The category of bounded lattices #
This file defines BddLat
, the category of bounded lattices.
In literature, this is sometimes called Lat
, the category of lattices, because being a lattice is
understood to entail having a bottom and a top element.
The category of bounded lattices with bounded lattice morphisms.
- toLat : Lat
The underlying lattice of a bounded lattice.
- isBoundedOrder : BoundedOrder ↑self.toLat
Instances For
Equations
- BddLat.instCoeSortType = { coe := fun (X : BddLat) => ↑X.toLat }
Equations
- X.instLatticeαToLat = X.toLat.str
@[simp]
Equations
- BddLat.instInhabited = { default := BddLat.of PUnit.{?u.3 + 1} }
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.
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.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BddLat.coe_forget_to_bddOrd
(X : BddLat)
:
↑((CategoryTheory.forget₂ BddLat BddOrd).obj X).toPartOrd = ↑X.toLat
@[simp]
theorem
BddLat.coe_forget_to_lat
(X : BddLat)
:
↑((CategoryTheory.forget₂ BddLat Lat).obj X) = ↑X.toLat
@[simp]
theorem
BddLat.coe_forget_to_semilatSup
(X : BddLat)
:
((CategoryTheory.forget₂ BddLat SemilatSupCat).obj X).X = ↑X.toLat
@[simp]
theorem
BddLat.coe_forget_to_semilatInf
(X : BddLat)
:
((CategoryTheory.forget₂ BddLat SemilatInfCat).obj X).X = ↑X.toLat
@[simp]
theorem
BddLat.Iso.mk_hom_toLatticeHom_toSupHom_toFun
{α : BddLat}
{β : BddLat}
(e : ↑α.toLat ≃o ↑β.toLat)
(a : ↑α.toLat)
:
(BddLat.Iso.mk e).hom.toSupHom a = e a
@[simp]
theorem
BddLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun
{α : BddLat}
{β : BddLat}
(e : ↑α.toLat ≃o ↑β.toLat)
(a : ↑β.toLat)
:
(BddLat.Iso.mk e).inv.toSupHom a = e.symm a
@[simp]
theorem
BddLat.dual_map
{X : BddLat}
{Y : BddLat}
(a : BoundedLatticeHom ↑X.toLat ↑Y.toLat)
:
BddLat.dual.map a = BoundedLatticeHom.dual a
OrderDual
as a functor.
Equations
- BddLat.dual = { obj := fun (X : BddLat) => BddLat.of (↑X.toLat)ᵒᵈ, map := fun {X Y : BddLat} => ⇑BoundedLatticeHom.dual, map_id := BddLat.dual.proof_1, map_comp := @BddLat.dual.proof_2 }
Instances For
theorem
bddLat_dual_comp_forget_to_lat :
BddLat.dual.comp (CategoryTheory.forget₂ BddLat Lat) = (CategoryTheory.forget₂ BddLat Lat).comp Lat.dual
The functor that adds a bottom and a top element to a lattice. This is the free functor.
Equations
- latToBddLat = { obj := fun (X : Lat) => BddLat.of (WithTop (WithBot ↑X)), map := fun {X Y : Lat} => LatticeHom.withTopWithBot, map_id := latToBddLat.proof_1, map_comp := @latToBddLat.proof_2 }
Instances For
latToBddLat
is left adjoint to the forgetful functor, meaning it is the free
functor from Lat
to BddLat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
latToBddLatCompDualIsoDualCompLatToBddLat :
latToBddLat.comp BddLat.dual ≅ Lat.dual.comp latToBddLat
latToBddLat
and OrderDual
commute.
Equations
- latToBddLatCompDualIsoDualCompLatToBddLat = (latToBddLatForgetAdjunction.comp BddLat.dualEquiv.toAdjunction).leftAdjointUniq (Lat.dualEquiv.toAdjunction.comp latToBddLatForgetAdjunction)