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.

• of :: (
• 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.

• of :: (
• X : Type u

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

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

@[implicit_reducible]

instance SemilatSupCat.instCoeSortType : CoeSort SemilatSupCat (Type u_1)

theorem SemilatSupCat.coe_of (α : Type u_1) [SemilatticeSup α] [OrderBot α] : { X := α, isSemilatticeSup := inst✝, isOrderBot := inst✝¹ }.X = α

@[implicit_reducible]

instance SemilatSupCat.instInhabited : Inhabited SemilatSupCat

@[implicit_reducible]

instance SemilatSupCat.instLargeCategory : CategoryTheory.LargeCategory SemilatSupCat

@[implicit_reducible]

instance SemilatSupCat.instConcreteCategorySupBotHomX : CategoryTheory.ConcreteCategory SemilatSupCat fun (x1 x2 : SemilatSupCat) => SupBotHom x1.X x2.X

@[implicit_reducible]

instance SemilatSupCat.hasForgetToPartOrd : CategoryTheory.HasForget₂ SemilatSupCat PartOrd

@[simp]

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

@[implicit_reducible]

instance SemilatInfCat.instCoeSortType : CoeSort SemilatInfCat (Type u_1)

theorem SemilatInfCat.coe_of (α : Type u_1) [SemilatticeInf α] [OrderTop α] : { X := α, isSemilatticeInf := inst✝, isOrderTop := inst✝¹ }.X = α

@[implicit_reducible]

instance SemilatInfCat.instInhabited : Inhabited SemilatInfCat

@[implicit_reducible]

instance SemilatInfCat.instLargeCategory : CategoryTheory.LargeCategory SemilatInfCat

@[implicit_reducible]

instance SemilatInfCat.instConcreteCategoryInfTopHomX : CategoryTheory.ConcreteCategory SemilatInfCat fun (x1 x2 : SemilatInfCat) => InfTopHom x1.X x2.X

@[implicit_reducible]

instance SemilatInfCat.hasForgetToPartOrd : CategoryTheory.HasForget₂ SemilatInfCat PartOrd

@[simp]

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

Order dual

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

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

@[simp]

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

@[simp]

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

def SemilatSupCat.dual : CategoryTheory.Functor SemilatSupCat SemilatInfCat

OrderDual as a functor.

@[simp]

theorem SemilatSupCat.dual_map {x✝ x✝¹ : SemilatSupCat} (a : SupBotHom x✝.X x✝¹.X) : dual.map a = SupBotHom.dual a

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

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

@[simp]

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

@[simp]

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

def SemilatInfCat.dual : CategoryTheory.Functor SemilatInfCat SemilatSupCat

OrderDual as a functor.

@[simp]

theorem SemilatInfCat.dual_obj_X (X : SemilatInfCat) : (dual.obj X).X = X.Xᵒᵈ

@[simp]

theorem SemilatInfCat.dual_obj_isOrderBot (X : SemilatInfCat) : (dual.obj X).isOrderBot = OrderDual.instOrderBotOfOrderTop X.X

@[simp]

theorem SemilatInfCat.dual_map {x✝ x✝¹ : SemilatInfCat} (a : InfTopHom x✝.X x✝¹.X) : dual.map a = InfTopHom.dual a

@[simp]

theorem SemilatInfCat.dual_obj_isSemilatticeSup (X : SemilatInfCat) : (dual.obj X).isSemilatticeSup = OrderDual.instSemilatticeSup X.X

def SemilatSupCatEquivSemilatInfCat : SemilatSupCat ≌ SemilatInfCat

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

@[simp]

theorem SemilatSupCatEquivSemilatInfCat_functor : SemilatSupCatEquivSemilatInfCat.functor = SemilatSupCat.dual

@[simp]

theorem SemilatSupCatEquivSemilatInfCat_inverse : SemilatSupCatEquivSemilatInfCat.inverse = SemilatInfCat.dual

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

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