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.

structure BddDistLat : Type (u_1 + 1)

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

instance BddDistLat.instCoeSortType : CoeSort BddDistLat (Type u_1)

Equations

• BddDistLat.instCoeSortType = { coe := fun (X : BddDistLat) => ↑X.toDistLat }

instance BddDistLat.instDistribLatticeαToDistLat (X : BddDistLat) : DistribLattice ↑X.toDistLat

Equations

• X.instDistribLatticeαToDistLat = X.toDistLat.str

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

Construct a bundled BddDistLat from a BoundedOrder DistribLattice.

Equations

• BddDistLat.of α = BddDistLat.mk { α := α, str := inferInstance }

@[simp]

theorem BddDistLat.coe_of (α : Type u_1) [DistribLattice α] [BoundedOrder α] : ↑(BddDistLat.of α).toDistLat = α

instance BddDistLat.instInhabited : Inhabited BddDistLat

Equations

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

def BddDistLat.toBddLat (X : BddDistLat) : BddLat

Turn a BddDistLat into a BddLat by forgetting it is distributive.

Equations

• X.toBddLat = BddLat.of ↑X.toDistLat

@[simp]

theorem BddDistLat.coe_toBddLat (X : BddDistLat) : ↑X.toBddLat.toLat = ↑X.toDistLat

instance BddDistLat.instLargeCategory : CategoryTheory.LargeCategory BddDistLat

Equations

• BddDistLat.instLargeCategory = CategoryTheory.InducedCategory.category BddDistLat.toBddLat

instance BddDistLat.instConcreteCategory : CategoryTheory.ConcreteCategory BddDistLat

Equations

• BddDistLat.instConcreteCategory = CategoryTheory.InducedCategory.concreteCategory BddDistLat.toBddLat

instance BddDistLat.hasForgetToDistLat : CategoryTheory.HasForget₂ BddDistLat DistLat

Equations

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

instance BddDistLat.hasForgetToBddLat : CategoryTheory.HasForget₂ BddDistLat BddLat

Equations

• BddDistLat.hasForgetToBddLat = CategoryTheory.InducedCategory.hasForget₂ BddDistLat.toBddLat

theorem BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat : (CategoryTheory.forget₂ BddDistLat BddLat).comp (CategoryTheory.forget₂ BddLat Lat) = (CategoryTheory.forget₂ BddDistLat DistLat).comp (CategoryTheory.forget₂ DistLat Lat)

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

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.

@[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

def BddDistLat.dual : CategoryTheory.Functor BddDistLat BddDistLat

OrderDual as a functor.

Equations

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

@[simp]

theorem BddDistLat.dual_map : ∀ {x x_1 : BddDistLat} (a : BoundedLatticeHom ↑x.toBddLat.toLat ↑x_1.toBddLat.toLat), BddDistLat.dual.map a = BoundedLatticeHom.dual a

@[simp]

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

def BddDistLat.dualEquiv : BddDistLat ≌ BddDistLat

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

Equations

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

@[simp]

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

@[simp]

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

theorem bddDistLat_dual_comp_forget_to_distLat : BddDistLat.dual.comp (CategoryTheory.forget₂ BddDistLat DistLat) = (CategoryTheory.forget₂ BddDistLat DistLat).comp DistLat.dual