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.instCoeSortType : CoeSort SemilatSupCat (Type u_1)

Equations

• SemilatSupCat.instCoeSortType = { 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.instInhabited : Inhabited SemilatSupCat

Equations

• SemilatSupCat.instInhabited = { default := SemilatSupCat.of PUnit.{?u.3 + 1} }

instance SemilatSupCat.instLargeCategory : CategoryTheory.LargeCategory SemilatSupCat

Equations

• SemilatSupCat.instLargeCategory = CategoryTheory.Category.mk @SemilatSupCat.instLargeCategory.proof_1 @SemilatSupCat.instLargeCategory.proof_2 @SemilatSupCat.instLargeCategory.proof_3

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

Equations

• X.instFunLike Y = inferInstance

instance SemilatSupCat.instConcreteCategory : 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.instCoeSortType : CoeSort SemilatInfCat (Type u_1)

Equations

• SemilatInfCat.instCoeSortType = { 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.instInhabited : Inhabited SemilatInfCat

Equations

• SemilatInfCat.instInhabited = { default := SemilatInfCat.of PUnit.{?u.3 + 1} }

instance SemilatInfCat.instLargeCategory : CategoryTheory.LargeCategory SemilatInfCat

Equations

• SemilatInfCat.instLargeCategory = CategoryTheory.Category.mk @SemilatInfCat.instLargeCategory.proof_1 @SemilatInfCat.instLargeCategory.proof_2 @SemilatInfCat.instLargeCategory.proof_3

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

Equations

• X.instFunLike Y = inferInstance

instance SemilatInfCat.instConcreteCategory : 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

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

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

Equations

• SemilatSupCat.Iso.mk e = { hom := { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ }, inv := { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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 = e.symm a

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 SemilatSupCat.dual_obj (X : SemilatSupCat) : SemilatSupCat.dual.obj X = SemilatInfCat.of X.Xᵒᵈ

@[simp]

theorem SemilatSupCat.dual_map : ∀ {x x_1 : SemilatSupCat} (a : SupBotHom x.X x_1.X), SemilatSupCat.dual.map a = SupBotHom.dual a

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

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

Equations

• SemilatInfCat.Iso.mk e = { hom := { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ }, inv := { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[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

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 SemilatInfCat.dual_map : ∀ {x x_1 : SemilatInfCat} (a : InfTopHom x.X x_1.X), SemilatInfCat.dual.map a = InfTopHom.dual a

@[simp]

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

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.

@[simp]

theorem SemilatSupCatEquivSemilatInfCat_inverse : SemilatSupCatEquivSemilatInfCat.inverse = SemilatInfCat.dual

@[simp]

theorem SemilatSupCatEquivSemilatInfCat_functor : SemilatSupCatEquivSemilatInfCat.functor = SemilatSupCat.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