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 #
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
Instances For
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
Instances For
Equations
- SemilatSupCat.instCoeSortType = { coe := SemilatSupCat.X }
@[simp]
theorem
SemilatSupCat.coe_of
(α : Type u_1)
[SemilatticeSup α]
[OrderBot α]
:
(SemilatSupCat.of α).X = α
Equations
- SemilatSupCat.instInhabited = { default := SemilatSupCat.of PUnit.{?u.3 + 1} }
Equations
- X.instFunLike Y = inferInstance
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- SemilatInfCat.instCoeSortType = { coe := SemilatInfCat.X }
@[simp]
theorem
SemilatInfCat.coe_of
(α : Type u_1)
[SemilatticeInf α]
[OrderTop α]
:
(SemilatInfCat.of α).X = α
Equations
- SemilatInfCat.instInhabited = { default := SemilatInfCat.of PUnit.{?u.3 + 1} }
Equations
- X.instFunLike Y = inferInstance
Equations
- One or more equations did not get rendered due to their size.
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_inv_toSupHom_toFun
{α : SemilatSupCat}
{β : SemilatSupCat}
(e : α.X ≃o β.X)
(a : β.X)
:
(SemilatSupCat.Iso.mk e).inv.toSupHom a = e.symm a
@[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
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 := ⋯ }
Instances For
@[simp]
theorem
SemilatSupCat.dual_map :
∀ {x x_1 : SemilatSupCat} (a : SupBotHom x.X x_1.X), SemilatSupCat.dual.map a = SupBotHom.dual a
@[simp]
theorem
SemilatSupCat.dual_obj
(X : SemilatSupCat)
:
SemilatSupCat.dual.obj X = SemilatInfCat.of X.Xᵒᵈ
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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
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 := ⋯ }
Instances For
@[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ᵒᵈ
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
The equivalence between SemilatSupCat
and SemilatInfCat
induced by OrderDual
both ways.
Equations
- One or more equations did not get rendered due to their size.