The category of distributive lattices #
This file defines DistLat
, the category of distributive lattices.
Note that DistLat
in the literature doesn't always
correspond to DistLat
as we don't require bottom or top elements. Instead, this DistLat
corresponds to BddDistLat
.
The category of distributive lattices.
Equations
Instances For
Equations
- DistLat.instCoeSortType = CategoryTheory.Bundled.coeSort
Equations
- X.instDistribLatticeα = X.str
Construct a bundled DistLat
from a DistribLattice
underlying type and typeclass.
Equations
Instances For
Equations
- DistLat.instInhabited = { default := DistLat.of PUnit.{?u.3 + 1} }
@[simp]
theorem
DistLat.Iso.mk_hom_toSupHom_toFun
{α : DistLat}
{β : DistLat}
(e : ↑α ≃o ↑β)
(a : ↑α)
:
(DistLat.Iso.mk e).hom.toSupHom a = e a
@[simp]
theorem
DistLat.Iso.mk_inv_toSupHom_toFun
{α : DistLat}
{β : DistLat}
(e : ↑α ≃o ↑β)
(a : ↑β)
:
(DistLat.Iso.mk e).inv.toSupHom a = e.symm a
Constructs an equivalence between distributive lattices from an order isomorphism between them.
Equations
- DistLat.Iso.mk e = { hom := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }, inv := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
DistLat.dual_map :
∀ {X Y : DistLat} (a : LatticeHom ↑X ↑Y), DistLat.dual.map a = LatticeHom.dual a
OrderDual
as a functor.
Equations
- DistLat.dual = { obj := fun (X : DistLat) => DistLat.of (↑X)ᵒᵈ, map := fun {X Y : DistLat} => ⇑LatticeHom.dual, map_id := DistLat.dual.proof_1, map_comp := @DistLat.dual.proof_2 }
Instances For
theorem
distLat_dual_comp_forget_to_Lat :
DistLat.dual.comp (CategoryTheory.forget₂ DistLat Lat) = (CategoryTheory.forget₂ DistLat Lat).comp Lat.dual