# mathlibdocumentation

order.category.Semilattice

# The categories of semilattices #

This defines SemilatticeSup and SemilatticeInf, the categories of sup-semilattices with a bottom element and inf-semilattices with a top element.

## References #

structure SemilatticeSup  :
Type (u+1)

The category of sup-semilattices with a bottom element.

Instances for SemilatticeSup
structure SemilatticeInf  :
Type (u+1)

The category of inf-semilattices with a top element.

Instances for SemilatticeInf
@[protected, instance]
def SemilatticeSup.has_coe_to_sort  :
(Type u_1)
Equations
def SemilatticeSup.of (α : Type u_1) [order_bot α] :

Construct a bundled SemilatticeSup from a semilattice_sup.

Equations
@[simp]
theorem SemilatticeSup.coe_of (α : Type u_1) [order_bot α] :
= α
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[protected, instance]
def SemilatticeInf.has_coe_to_sort  :
(Type u_1)
Equations
def SemilatticeInf.of (α : Type u_1) [order_top α] :

Construct a bundled SemilatticeInf from a semilattice_inf.

Equations
@[simp]
theorem SemilatticeInf.coe_of (α : Type u_1) [order_top α] :
= α
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]

### Order dual #

def SemilatticeSup.iso.mk {α β : SemilatticeSup} (e : α ≃o β) :
α β

Constructs an isomorphism of lattices from an order isomorphism between them.

Equations
@[simp]
theorem SemilatticeSup.iso.mk_inv {α β : SemilatticeSup} (e : α ≃o β) :
= (e.symm)
@[simp]
theorem SemilatticeSup.iso.mk_hom {α β : SemilatticeSup} (e : α ≃o β) :

order_dual as a functor.

Equations
@[simp]
@[simp]
theorem SemilatticeSup.dual_map (X Y : SemilatticeSup) (ᾰ : Y) :
@[simp]
theorem SemilatticeInf.iso.mk_inv {α β : SemilatticeInf} (e : α ≃o β) :
= (e.symm)
@[simp]
theorem SemilatticeInf.iso.mk_hom {α β : SemilatticeInf} (e : α ≃o β) :
def SemilatticeInf.iso.mk {α β : SemilatticeInf} (e : α ≃o β) :
α β

Constructs an isomorphism of lattices from an order isomorphism between them.

Equations

order_dual as a functor.

Equations
@[simp]
@[simp]
theorem SemilatticeInf.dual_map (X Y : SemilatticeInf) (ᾰ : Y) :

The equivalence between SemilatticeSup and SemilatticeInf induced by order_dual both ways.

Equations