The category of bounded distributive lattices #
This defines BddDistLat
, the category of bounded distributive lattices.
Note that this category is sometimes called DistLat
when
being a lattice is understood to entail having a bottom and a top element.
The category of bounded distributive lattices with bounded lattice morphisms.
- toDistLat : DistLat
The underlying distrib lattice of a bounded distributive lattice.
- isBoundedOrder : BoundedOrder ↑self.toDistLat
Instances For
Equations
- BddDistLat.instCoeSortType = { coe := fun (X : BddDistLat) => ↑X.toDistLat }
Equations
- X.instDistribLatticeαToDistLat = X.toDistLat.str
Construct a bundled BddDistLat
from a BoundedOrder
DistribLattice
.
Equations
- BddDistLat.of α = BddDistLat.mk { α := α, str := inferInstance }
Instances For
@[simp]
theorem
BddDistLat.coe_of
(α : Type u_1)
[DistribLattice α]
[BoundedOrder α]
:
↑(BddDistLat.of α).toDistLat = α
Equations
- BddDistLat.instInhabited = { default := BddDistLat.of PUnit.{?u.3 + 1} }
Turn a BddDistLat
into a BddLat
by forgetting it is distributive.
Instances For
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
BddDistLat.Iso.mk_hom_toLatticeHom_toSupHom_toFun
{α : BddDistLat}
{β : BddDistLat}
(e : ↑α.toDistLat ≃o ↑β.toDistLat)
(a : ↑α.toDistLat)
:
(BddDistLat.Iso.mk e).hom.toSupHom a = e a
@[simp]
theorem
BddDistLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun
{α : BddDistLat}
{β : BddDistLat}
(e : ↑α.toDistLat ≃o ↑β.toDistLat)
(a : ↑β.toDistLat)
:
(BddDistLat.Iso.mk e).inv.toSupHom a = e.symm a
Constructs an equivalence between bounded distributive lattices from an order isomorphism between them.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
BddDistLat.dual_obj
(X : BddDistLat)
:
BddDistLat.dual.obj X = BddDistLat.of (↑X.toDistLat)ᵒᵈ
@[simp]
theorem
BddDistLat.dual_map
{X : BddDistLat}
{Y : BddDistLat}
(a : BoundedLatticeHom ↑X.toBddLat.toLat ↑Y.toBddLat.toLat)
:
BddDistLat.dual.map a = BoundedLatticeHom.dual a
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence between BddDistLat
and itself induced by OrderDual
both ways.
Equations
- One or more equations did not get rendered due to their size.