Lattice Congruences

Main definitions

• LatticeCon: An equivalence relation is a congruence relation for the lattice structure if it is compatible with the inf and sup operations.
• LatticeCon.ker: The kernel of a lattice homomorphism as a lattice congruence.

Main statements

• LatticeCon.mk': Alternative conditions for a relation to be a lattice congruence.

References

• Grätzer et al, General lattice theory

Tags

Lattice, Congruence

structure LatticeCon (α : Type u_2) [Lattice α] extends Setoid α : Type u_2

An equivalence relation is a congruence relation for the latice structure if it is compatible with the inf and sup operations.

• r : α → α → Prop
• iseqv : Equivalence ⇑self.toSetoid
• inf {w x y z : α} : self.toSetoid w x → self.toSetoid y z → self.toSetoid (w ⊓ y) (x ⊓ z)
• sup {w x y z : α} : self.toSetoid w x → self.toSetoid y z → self.toSetoid (w ⊔ y) (x ⊔ z)

@[simp]

theorem LatticeCon.r_inf_sup_iff {α : Type u_2} [Lattice α] (c : LatticeCon α) {x y : α} : c.toSetoid (x ⊓ y) (x ⊔ y) ↔ c.toSetoid x y

def LatticeCon.mk' {α : Type u_2} [Lattice α] (r : α → α → Prop) [h₁ : IsRefl α r] (h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)) (h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z) (h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)) : LatticeCon α

Alternative conditions for a lattice congruence.

Equations

• LatticeCon.mk' r h₂ h₃ h₄ = { r := r, iseqv := ⋯, inf := ⋯, sup := ⋯ }

def LatticeCon.ker {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Lattice α] [Lattice β] [LatticeHomClass F α β] (f : F) : LatticeCon α

The kernel of a lattice homomorphism as a lattice congruence.

Equations

• LatticeCon.ker f = { toSetoid := Setoid.ker ⇑f, inf := ⋯, sup := ⋯ }

@[simp]

theorem LatticeCon.ker_r {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Lattice α] [Lattice β] [LatticeHomClass F α β] (f : F) (a✝ a✝¹ : α) : (ker f).toSetoid a✝ a✝¹ = Function.onFun (fun (x1 x2 : β) => x1 = x2) (⇑f) a✝ a✝¹