The categories of semilattices

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

References

• nLab, semilattice

structure SemilatSupCat : Type (u + 1)

The category of sup-semilattices with a bottom element.

• X : Type u

  The underlying type of a sup-semilattice with a bottom element.

• isSemilatticeSup : SemilatticeSup self.X
• isOrderBot : OrderBot self.X

structure SemilatInfCat : Type (u + 1)

The category of inf-semilattices with a top element.

• X : Type u

  The underlying type of an inf-semilattice with a top element.

• isSemilatticeInf : SemilatticeInf self.X
• isOrderTop : OrderTop self.X

instance SemilatSupCat.instCoeSortSemilatSupCatType : CoeSort SemilatSupCat (Type u_1)

Equations

• SemilatSupCat.instCoeSortSemilatSupCatType = { coe := SemilatSupCat.X }

def SemilatSupCat.of (α : Type u_1) [SemilatticeSup α] [OrderBot α] : SemilatSupCat

Construct a bundled SemilatSupCat from a SemilatticeSup.

Equations

• SemilatSupCat.of α = SemilatSupCat.mk α

@[simp]

theorem SemilatSupCat.coe_of (α : Type u_1) [SemilatticeSup α] [OrderBot α] : (SemilatSupCat.of α).X = α

instance SemilatSupCat.instInhabitedSemilatSupCat : Inhabited SemilatSupCat

Equations

• SemilatSupCat.instInhabitedSemilatSupCat = { default := SemilatSupCat.of PUnit.{u_1 + 1} }

instance SemilatSupCat.instLargeCategorySemilatSupCat : CategoryTheory.LargeCategory SemilatSupCat

Equations

• One or more equations did not get rendered due to their size.

instance SemilatSupCat.instFunLike (X : SemilatSupCat) (Y : SemilatSupCat) : FunLike (X ⟶ Y) X.X Y.X

Equations

• SemilatSupCat.instFunLike X Y = let_fun this := inferInstance; this

instance SemilatSupCat.instConcreteCategorySemilatSupCatInstLargeCategorySemilatSupCat : CategoryTheory.ConcreteCategory SemilatSupCat

Equations

• One or more equations did not get rendered due to their size.

instance SemilatSupCat.hasForgetToPartOrd : CategoryTheory.HasForget₂ SemilatSupCat PartOrd

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SemilatSupCat.coe_forget_to_partOrd (X : SemilatSupCat) : ↑((CategoryTheory.forget₂ SemilatSupCat PartOrd).obj X) = X.X

instance SemilatInfCat.instCoeSortSemilatInfCatType : CoeSort SemilatInfCat (Type u_1)

Equations

• SemilatInfCat.instCoeSortSemilatInfCatType = { coe := SemilatInfCat.X }

def SemilatInfCat.of (α : Type u_1) [SemilatticeInf α] [OrderTop α] : SemilatInfCat

Construct a bundled SemilatInfCat from a SemilatticeInf.

Equations

• SemilatInfCat.of α = SemilatInfCat.mk α

@[simp]

theorem SemilatInfCat.coe_of (α : Type u_1) [SemilatticeInf α] [OrderTop α] : (SemilatInfCat.of α).X = α

instance SemilatInfCat.instInhabitedSemilatInfCat : Inhabited SemilatInfCat

Equations

• SemilatInfCat.instInhabitedSemilatInfCat = { default := SemilatInfCat.of PUnit.{u_1 + 1} }

instance SemilatInfCat.instLargeCategorySemilatInfCat : CategoryTheory.LargeCategory SemilatInfCat

Equations

• One or more equations did not get rendered due to their size.

instance SemilatInfCat.instFunLike (X : SemilatInfCat) (Y : SemilatInfCat) : FunLike (X ⟶ Y) X.X Y.X

Equations

• SemilatInfCat.instFunLike X Y = let_fun this := inferInstance; this

instance SemilatInfCat.instConcreteCategorySemilatInfCatInstLargeCategorySemilatInfCat : CategoryTheory.ConcreteCategory SemilatInfCat

Equations

• One or more equations did not get rendered due to their size.

instance SemilatInfCat.hasForgetToPartOrd : CategoryTheory.HasForget₂ SemilatInfCat PartOrd

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SemilatInfCat.coe_forget_to_partOrd (X : SemilatInfCat) : ↑((CategoryTheory.forget₂ SemilatInfCat PartOrd).obj X) = X.X

Order dual

@[simp]

theorem SemilatSupCat.Iso.mk_hom_toSupHom_toFun {α : SemilatSupCat} {β : SemilatSupCat} (e : α.X ≃o β.X) (a : α.X) : (SemilatSupCat.Iso.mk e).hom.toSupHom a = e a

@[simp]

theorem SemilatSupCat.Iso.mk_inv_toSupHom_toFun {α : SemilatSupCat} {β : SemilatSupCat} (e : α.X ≃o β.X) (a : β.X) : (SemilatSupCat.Iso.mk e).inv.toSupHom a = (OrderIso.symm e) a

def SemilatSupCat.Iso.mk {α : SemilatSupCat} {β : SemilatSupCat} (e : α.X ≃o β.X) : α ≅ β

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SemilatSupCat.dual_map {X : SemilatSupCat} {Y : SemilatSupCat} (a : SupBotHom X.X Y.X) : SemilatSupCat.dual.map a = SupBotHom.dual a

@[simp]

theorem SemilatSupCat.dual_obj (X : SemilatSupCat) : SemilatSupCat.dual.obj X = SemilatInfCat.of X.Xᵒᵈ

def SemilatSupCat.dual : CategoryTheory.Functor SemilatSupCat SemilatInfCat

OrderDual as a functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SemilatInfCat.Iso.mk_hom_toInfHom_toFun {α : SemilatInfCat} {β : SemilatInfCat} (e : α.X ≃o β.X) (a : α.X) : (SemilatInfCat.Iso.mk e).hom.toInfHom a = e a

@[simp]

theorem SemilatInfCat.Iso.mk_inv_toInfHom_toFun {α : SemilatInfCat} {β : SemilatInfCat} (e : α.X ≃o β.X) (a : β.X) : (SemilatInfCat.Iso.mk e).inv.toInfHom a = (OrderIso.symm e) a

def SemilatInfCat.Iso.mk {α : SemilatInfCat} {β : SemilatInfCat} (e : α.X ≃o β.X) : α ≅ β

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SemilatInfCat.dual_map {X : SemilatInfCat} {Y : SemilatInfCat} (a : InfTopHom X.X Y.X) : SemilatInfCat.dual.map a = InfTopHom.dual a

@[simp]

theorem SemilatInfCat.dual_obj (X : SemilatInfCat) : SemilatInfCat.dual.obj X = SemilatSupCat.of X.Xᵒᵈ

def SemilatInfCat.dual : CategoryTheory.Functor SemilatInfCat SemilatSupCat

OrderDual as a functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SemilatSupCatEquivSemilatInfCat_inverse : SemilatSupCatEquivSemilatInfCat.inverse = SemilatInfCat.dual

@[simp]

theorem SemilatSupCatEquivSemilatInfCat_functor : SemilatSupCatEquivSemilatInfCat.functor = SemilatSupCat.dual

def SemilatSupCatEquivSemilatInfCat : SemilatSupCat ≌ SemilatInfCat

The equivalence between SemilatSupCat and SemilatInfCat induced by OrderDual both ways.

Equations

• One or more equations did not get rendered due to their size.

theorem SemilatSupCat_dual_comp_forget_to_partOrd : CategoryTheory.Functor.comp SemilatSupCat.dual (CategoryTheory.forget₂ SemilatInfCat PartOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ SemilatSupCat PartOrd) PartOrd.dual

theorem SemilatInfCat_dual_comp_forget_to_partOrd : CategoryTheory.Functor.comp SemilatInfCat.dual (CategoryTheory.forget₂ SemilatSupCat PartOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ SemilatInfCat PartOrd) PartOrd.dual