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.

def DistLat : Type (u_1 + 1)

The category of distributive lattices.

Equations

• DistLat = CategoryTheory.Bundled DistribLattice

instance DistLat.instCoeSortType : CoeSort DistLat (Type u_1)

Equations

• DistLat.instCoeSortType = CategoryTheory.Bundled.coeSort

instance DistLat.instDistribLatticeα (X : DistLat) : DistribLattice ↑X

Equations

• X.instDistribLatticeα = X.str

def DistLat.of (α : Type u_1) [DistribLattice α] : DistLat

Construct a bundled DistLat from a DistribLattice underlying type and typeclass.

Equations

• DistLat.of α = CategoryTheory.Bundled.of α

@[simp]

theorem DistLat.coe_of (α : Type u_1) [DistribLattice α] : ↑(DistLat.of α) = α

instance DistLat.instInhabited : Inhabited DistLat

Equations

• DistLat.instInhabited = { default := DistLat.of PUnit.{?u.3 + 1} }

instance DistLat.instParentProjectionLatticeDistribLatticeToLattice : CategoryTheory.BundledHom.ParentProjection @DistribLattice.toLattice

instance instDistLatLargeCategory : CategoryTheory.LargeCategory DistLat

Equations

• instDistLatLargeCategory = CategoryTheory.BundledHom.category (CategoryTheory.BundledHom.MapHom LatticeHom @DistribLattice.toLattice)

instance DistLat.instConcreteCategory : CategoryTheory.ConcreteCategory DistLat

Equations

• DistLat.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory (CategoryTheory.BundledHom.MapHom LatticeHom @DistribLattice.toLattice)

instance DistLat.hasForgetToLat : CategoryTheory.HasForget₂ DistLat Lat

Equations

• DistLat.hasForgetToLat = CategoryTheory.BundledHom.forget₂ LatticeHom @DistribLattice.toLattice

def DistLat.Iso.mk {α β : DistLat} (e : ↑α ≃o ↑β) : α ≅ β

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 := ⋯ }

@[simp]

theorem DistLat.Iso.mk_hom_toSupHom_toFun {α β : DistLat} (e : ↑α ≃o ↑β) (a : ↑α) : (DistLat.Iso.mk e).hom.toSupHom a = e a

@[simp]

theorem DistLat.Iso.mk_inv_toSupHom_toFun {α β : DistLat} (e : ↑α ≃o ↑β) (a : ↑β) : (DistLat.Iso.mk e).inv.toSupHom a = e.symm a

def DistLat.dual : CategoryTheory.Functor DistLat DistLat

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 }

@[simp]

theorem DistLat.dual_obj (X : DistLat) : DistLat.dual.obj X = DistLat.of (↑X)ᵒᵈ

@[simp]

theorem DistLat.dual_map {X✝ Y✝ : DistLat} (a : LatticeHom ↑X✝ ↑Y✝) : DistLat.dual.map a = LatticeHom.dual a

def DistLat.dualEquiv : DistLat ≌ DistLat

The equivalence between DistLat and itself induced by OrderDual both ways.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DistLat.dualEquiv_functor : DistLat.dualEquiv.functor = DistLat.dual

@[simp]

theorem DistLat.dualEquiv_inverse : DistLat.dualEquiv.inverse = DistLat.dual

theorem distLat_dual_comp_forget_to_Lat : DistLat.dual.comp (CategoryTheory.forget₂ DistLat Lat) = (CategoryTheory.forget₂ DistLat Lat).comp Lat.dual