Join-semilattice congruences

SupCon α is an equivalence relation compatible with ⊔, the join-only sibling of mathlib's LatticeCon. The kernel of a sup-homomorphism is one. Conversely, a congruence of a join-semilattice is cut out by the sup-homomorphisms to Prop whose kernels contain it: for each y, the elements whose join with y stays in the class of y form an ideal, and its complement is such a homomorphism separating y from everything outside that ideal. In a finite join-semilattice the ideal is principal, so a congruence is cut out by the down-sets Iic a that are unions of its classes.

Main definitions

• SupCon: a congruence for ⊔.
• SupCon.ker: the kernel of a sup-homomorphism.
• SupCon.sepHom: the sup-homomorphism to Prop separating y from the elements whose join with y leaves its class.

Main statements

• SupCon.r_iff_forall_le: in a finite join-semilattice, two elements are congruent iff they lie in the same down-sets Iic a among those that are unions of classes.

[UPSTREAM] candidate beside Mathlib/Order/Lattice/Congruence.lean.

structure SupCon (α : Type u_2) [Max α] extends Setoid α : Type u_2

An equivalence relation is a congruence for ⊔ if it is compatible with it.

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

def SupCon.ker {F : Type u_1} {α : Type u_2} {β : Type u_3} [Max α] [Max β] [FunLike F α β] [SupHomClass F α β] (f : F) : SupCon α

The kernel of a sup-homomorphism as a congruence.

Equations

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

@[simp]

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

theorem SupCon.r_sup_sup_iff {α : Type u_2} [SemilatticeSup α] (c : SupCon α) {y z w : α} : c.toSetoid (z ⊔ w ⊔ y) y ↔ c.toSetoid (z ⊔ y) y ∧ c.toSetoid (w ⊔ y) y

An element joins into the class of y with the join of two elements iff it does so with each.

def SupCon.sepHom {α : Type u_2} [SemilatticeSup α] (c : SupCon α) (y : α) : SupHom α Prop

The elements whose join with y leaves the class of y: the complement of an ideal, so a sup-homomorphism to Prop.

Equations

• c.sepHom y = { toFun := fun (z : α) => ¬c.toSetoid (z ⊔ y) y, map_sup' := ⋯ }

@[simp]

theorem SupCon.sepHom_apply {α : Type u_2} [SemilatticeSup α] (c : SupCon α) (y z : α) : (c.sepHom y) z ↔ ¬c.toSetoid (z ⊔ y) y

theorem SupCon.le_ker_sepHom {α : Type u_2} [SemilatticeSup α] (c : SupCon α) (y : α) : c.toSetoid ≤ Setoid.ker ⇑(c.sepHom y)

The congruence is contained in the kernel of each separating homomorphism.

theorem SupCon.exists_iff_le {α : Type u_2} [SemilatticeSup α] (c : SupCon α) [Finite α] (y : α) : ∃ (a : α), ∀ (z : α), z ≤ a ↔ c.toSetoid (z ⊔ y) y

In a finite join-semilattice, the elements whose join with y stays in the class of y are the down-set of some element.

theorem SupCon.r_iff_forall_le {α : Type u_2} [SemilatticeSup α] (c : SupCon α) {x y : α} [Finite α] : c.toSetoid x y ↔ ∀ (a : α), (∀ (z w : α), c.toSetoid z w → (z ≤ a ↔ w ≤ a)) → (x ≤ a ↔ y ≤ a)

In a finite join-semilattice, two elements are congruent iff they lie in the same down-sets Iic a among those that are unions of classes.