113 lines
4 KiB
Text
113 lines
4 KiB
Text
|
/-
|
||
|
|
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
|
||
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||
|
|
Author: Jeremy Avigad
|
||
|
|
-/
|
||
|
|
import .order
|
||
|
|
|
||
|
|
namespace algebra
|
||
|
|
|
||
|
|
variable {A : Type}
|
||
|
|
|
||
|
|
/- lattices (we could split this to upper- and lower-semilattices, if needed) -/
|
||
|
|
|
||
|
|
structure lattice [class] (A : Type) extends weak_order A :=
|
||
|
|
(inf : A → A → A)
|
||
|
|
(sup : A → A → A)
|
||
|
|
(inf_le_left : ∀ a b, le (inf a b) a)
|
||
|
|
(inf_le_right : ∀ a b, le (inf a b) b)
|
||
|
|
(le_inf : ∀a b c, le c a → le c b → le c (inf a b))
|
||
|
|
(le_sup_left : ∀ a b, le a (sup a b))
|
||
|
|
(le_sup_right : ∀ a b, le b (sup a b))
|
||
|
|
(sup_le : ∀ a b c, le a c → le b c → le (sup a b) c)
|
||
|
|
|
||
|
|
definition inf := @lattice.inf
|
||
|
|
definition sup := @lattice.sup
|
||
|
|
infix `⊓`:70 := inf
|
||
|
|
infix `⊔`:65 := sup
|
||
|
|
|
||
|
|
section
|
||
|
|
variable [s : lattice A]
|
||
|
|
include s
|
||
|
|
|
||
|
|
theorem inf_le_left (a b : A) : a ⊓ b ≤ a := !lattice.inf_le_left
|
||
|
|
|
||
|
|
theorem inf_le_right (a b : A) : a ⊓ b ≤ b := !lattice.inf_le_right
|
||
|
|
|
||
|
|
theorem le_inf {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) : c ≤ a ⊓ b := !lattice.le_inf H₁ H₂
|
||
|
|
|
||
|
|
theorem le_sup_left (a b : A) : a ≤ a ⊔ b := !lattice.le_sup_left
|
||
|
|
|
||
|
|
theorem le_sup_right (a b : A) : b ≤ a ⊔ b := !lattice.le_sup_right
|
||
|
|
|
||
|
|
theorem sup_le {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) : a ⊔ b ≤ c := !lattice.sup_le H₁ H₂
|
||
|
|
|
||
|
|
/- inf -/
|
||
|
|
|
||
|
|
theorem eq_inf {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) (H₃ : ∀{d}, d ≤ a → d ≤ b → d ≤ c) :
|
||
|
|
c = a ⊓ b :=
|
||
|
|
le.antisymm (le_inf H₁ H₂) (H₃ !inf_le_left !inf_le_right)
|
||
|
|
|
||
|
|
theorem inf.comm (a b : A) : a ⊓ b = b ⊓ a :=
|
||
|
|
eq_inf !inf_le_right !inf_le_left (λ c H₁ H₂, le_inf H₂ H₁)
|
||
|
|
|
||
|
|
theorem inf.assoc (a b c : A) : (a ⊓ b) ⊓ c = a ⊓ (b ⊓ c) :=
|
||
|
|
begin
|
||
|
|
apply eq_inf,
|
||
|
|
{ apply le.trans, apply inf_le_left, apply inf_le_left },
|
||
|
|
{ apply le_inf, apply le.trans, apply inf_le_left, apply inf_le_right, apply inf_le_right },
|
||
|
|
{ intros [d, H₁, H₂], apply le_inf, apply le_inf H₁, apply le.trans H₂, apply inf_le_left,
|
||
|
|
apply le.trans H₂, apply inf_le_right }
|
||
|
|
end
|
||
|
|
|
||
|
|
theorem inf.left_comm (a b c : A) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c) :=
|
||
|
|
binary.left_comm (@inf.comm A s) (@inf.assoc A s) a b c
|
||
|
|
|
||
|
|
theorem inf.right_comm (a b c : A) : (a ⊓ b) ⊓ c = (a ⊓ c) ⊓ b :=
|
||
|
|
binary.right_comm (@inf.comm A s) (@inf.assoc A s) a b c
|
||
|
|
|
||
|
|
theorem inf_self (a : A) : a ⊓ a = a :=
|
||
|
|
by apply eq.symm; apply eq_inf (le.refl a) !le.refl; intros; assumption
|
||
|
|
|
||
|
|
theorem inf_eq_left {a b : A} (H : a ≤ b) : a ⊓ b = a :=
|
||
|
|
by apply eq.symm; apply eq_inf !le.refl H; intros; assumption
|
||
|
|
|
||
|
|
theorem inf_eq_right {a b : A} (H : b ≤ a) : a ⊓ b = b :=
|
||
|
|
eq.subst !inf.comm (inf_eq_left H)
|
||
|
|
|
||
|
|
/- sup -/
|
||
|
|
|
||
|
|
theorem eq_sup {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) (H₃ : ∀{d}, a ≤ d → b ≤ d → c ≤ d) :
|
||
|
|
c = a ⊔ b :=
|
||
|
|
le.antisymm (H₃ !le_sup_left !le_sup_right) (sup_le H₁ H₂)
|
||
|
|
|
||
|
|
theorem sup.comm (a b : A) : a ⊔ b = b ⊔ a :=
|
||
|
|
eq_sup !le_sup_right !le_sup_left (λ c H₁ H₂, sup_le H₂ H₁)
|
||
|
|
|
||
|
|
theorem sup.assoc (a b c : A) : (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c) :=
|
||
|
|
begin
|
||
|
|
apply eq_sup,
|
||
|
|
{ apply le.trans, apply le_sup_left a b, apply le_sup_left },
|
||
|
|
{ apply sup_le, apply le.trans, apply le_sup_right a b, apply le_sup_left, apply le_sup_right },
|
||
|
|
{ intros [d, H₁, H₂], apply sup_le, apply sup_le H₁, apply le.trans !le_sup_left H₂,
|
||
|
|
apply le.trans !le_sup_right H₂}
|
||
|
|
end
|
||
|
|
|
||
|
|
theorem sup.left_comm (a b c : A) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c) :=
|
||
|
|
binary.left_comm (@sup.comm A s) (@sup.assoc A s) a b c
|
||
|
|
|
||
|
|
theorem sup.right_comm (a b c : A) : (a ⊔ b) ⊔ c = (a ⊔ c) ⊔ b :=
|
||
|
|
binary.right_comm (@sup.comm A s) (@sup.assoc A s) a b c
|
||
|
|
|
||
|
|
theorem sup_self (a : A) : a ⊔ a = a :=
|
||
|
|
by apply eq.symm; apply eq_sup (le.refl a) !le.refl; intros; assumption
|
||
|
|
|
||
|
|
theorem sup_eq_left {a b : A} (H : b ≤ a) : a ⊔ b = a :=
|
||
|
|
by apply eq.symm; apply eq_sup !le.refl H; intros; assumption
|
||
|
|
|
||
|
|
theorem sup_eq_right {a b : A} (H : a ≤ b) : a ⊔ b = b :=
|
||
|
|
eq.subst !sup.comm (sup_eq_left H)
|
||
|
|
end
|
||
|
|
|
||
|
|
end algebra
|