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 }
@[simp]
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.
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
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
BddDistLat.dual_map
{x✝ x✝¹ : BddDistLat}
(a : BoundedLatticeHom ↑x✝.toBddLat.toLat ↑x✝¹.toBddLat.toLat)
:
The equivalence between BddDistLat
and itself induced by OrderDual
both ways.
Equations
- One or more equations did not get rendered due to their size.