The category of complete lattices #
This file defines CompleteLat
, the category of complete lattices.
The category of complete lattices.
Instances For
Equations
- CompleteLat.instCoeSortType = CategoryTheory.Bundled.coeSort
Equations
- X.instCompleteLatticeα = X.str
@[simp]
Equations
- CompleteLat.instInhabited = { default := CompleteLat.of PUnit.{?u.3 + 1} }
Equations
- One or more equations did not get rendered due to their size.
Equations
- CompleteLat.instConcreteCategory = id inferInstance
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CompleteLat.Iso.mk_inv_toFun
{α : CompleteLat}
{β : CompleteLat}
(e : ↑α ≃o ↑β)
(a : ↑β)
:
(CompleteLat.Iso.mk e).inv.toFun a = e.symm a
@[simp]
theorem
CompleteLat.Iso.mk_hom_toFun
{α : CompleteLat}
{β : CompleteLat}
(e : ↑α ≃o ↑β)
(a : ↑α)
:
(CompleteLat.Iso.mk e).hom.toFun a = e a
Constructs an isomorphism of complete lattices from an order isomorphism between them.
Equations
- CompleteLat.Iso.mk e = { hom := { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }, inv := { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CompleteLat.dual_map
{X : CompleteLat}
{Y : CompleteLat}
(a : CompleteLatticeHom ↑X ↑Y)
:
CompleteLat.dual.map a = CompleteLatticeHom.dual a
@[simp]
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
The equivalence between CompleteLat
and itself induced by OrderDual
both ways.
Equations
- One or more equations did not get rendered due to their size.