The category of finite bounded distributive lattices #
This file defines FinBddDistLat
, the category of finite distributive lattices with
bounded lattice homomorphisms.
The category of finite distributive lattices with bounded lattice morphisms.
- toBddDistLat : BddDistLat
- isFintype : Fintype ↑self.toBddDistLat.toDistLat
Instances For
Equations
- FinBddDistLat.instCoeSortType = { coe := fun (X : FinBddDistLat) => ↑X.toBddDistLat.toDistLat }
instance
FinBddDistLat.instDistribLatticeαToDistLatToBddDistLat
(X : FinBddDistLat)
:
DistribLattice ↑X.toBddDistLat.toDistLat
Equations
- X.instDistribLatticeαToDistLatToBddDistLat = X.toBddDistLat.toDistLat.str
instance
FinBddDistLat.instBoundedOrderαDistribLatticeToDistLatToBddDistLat
(X : FinBddDistLat)
:
BoundedOrder ↑X.toBddDistLat.toDistLat
Equations
- X.instBoundedOrderαDistribLatticeToDistLatToBddDistLat = X.toBddDistLat.isBoundedOrder
Construct a bundled FinBddDistLat
from a Nonempty
BoundedOrder
DistribLattice
.
Equations
- FinBddDistLat.of α = FinBddDistLat.mk (BddDistLat.mk { α := α, str := inferInstance })
Instances For
Construct a bundled FinBddDistLat
from a Nonempty
BoundedOrder
DistribLattice
.
Equations
- FinBddDistLat.of' α = FinBddDistLat.mk (BddDistLat.mk { α := α, str := inferInstance })
Instances For
Equations
- FinBddDistLat.instInhabited = { default := FinBddDistLat.of PUnit.{?u.3 + 1} }
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
FinBddDistLat.Iso.mk_hom_toLatticeHom_toSupHom_toFun
{α : FinBddDistLat}
{β : FinBddDistLat}
(e : ↑α.toBddDistLat.toDistLat ≃o ↑β.toBddDistLat.toDistLat)
(a : ↑α.toBddDistLat.toDistLat)
:
(FinBddDistLat.Iso.mk e).hom.toSupHom a = e a
@[simp]
theorem
FinBddDistLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun
{α : FinBddDistLat}
{β : FinBddDistLat}
(e : ↑α.toBddDistLat.toDistLat ≃o ↑β.toBddDistLat.toDistLat)
(a : ↑β.toBddDistLat.toDistLat)
:
(FinBddDistLat.Iso.mk e).inv.toSupHom a = e.symm a
def
FinBddDistLat.Iso.mk
{α : FinBddDistLat}
{β : FinBddDistLat}
(e : ↑α.toBddDistLat.toDistLat ≃o ↑β.toBddDistLat.toDistLat)
:
α ≅ β
Constructs an equivalence between finite 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
FinBddDistLat.dual_obj
(X : FinBddDistLat)
:
FinBddDistLat.dual.obj X = FinBddDistLat.of (↑X.toBddDistLat.toDistLat)ᵒᵈ
@[simp]
theorem
FinBddDistLat.dual_map :
∀ {x x_1 : FinBddDistLat} (a : BoundedLatticeHom ↑x.toBddDistLat.toBddLat.toLat ↑x_1.toBddDistLat.toBddLat.toLat),
FinBddDistLat.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
@[simp]
@[simp]
The equivalence between FinBddDistLat
and itself induced by OrderDual
both ways.
Equations
- One or more equations did not get rendered due to their size.