The category of finite bounded distributive lattices

This file defines FinBddDistLat, the category of finite distributive lattices with bounded lattice homomorphisms.

structure FinBddDistLat : Type (u_1 + 1)

The category of finite distributive lattices with bounded lattice morphisms.

• toBddDistLat : BddDistLat
• isFintype : Fintype ↑self.toBddDistLat.toDistLat

instance FinBddDistLat.instCoeSortFinBddDistLatType : CoeSort FinBddDistLat (Type u_1)

Equations

• FinBddDistLat.instCoeSortFinBddDistLatType = { coe := fun (X : FinBddDistLat) => ↑X.toBddDistLat.toDistLat }

instance FinBddDistLat.instDistribLatticeαToDistLatToBddDistLat (X : FinBddDistLat) : DistribLattice ↑X.toBddDistLat.toDistLat

Equations

• FinBddDistLat.instDistribLatticeαToDistLatToBddDistLat X = X.toBddDistLat.toDistLat.str

instance FinBddDistLat.instBoundedOrderαDistribLatticeToDistLatToBddDistLatToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeαToDistLatToBddDistLat (X : FinBddDistLat) : BoundedOrder ↑X.toBddDistLat.toDistLat

Equations

• FinBddDistLat.instBoundedOrderαDistribLatticeToDistLatToBddDistLatToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeαToDistLatToBddDistLat X = X.toBddDistLat.isBoundedOrder

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

Construct a bundled FinBddDistLat from a Nonempty BoundedOrder DistribLattice.

Equations

• FinBddDistLat.of α = FinBddDistLat.mk (BddDistLat.mk (CategoryTheory.Bundled.mk α))

def FinBddDistLat.of' (α : Type u_1) [DistribLattice α] [Fintype α] [Nonempty α] : FinBddDistLat

Construct a bundled FinBddDistLat from a Nonempty BoundedOrder DistribLattice.

Equations

• FinBddDistLat.of' α = FinBddDistLat.mk (BddDistLat.mk (CategoryTheory.Bundled.mk α))

instance FinBddDistLat.instInhabitedFinBddDistLat : Inhabited FinBddDistLat

Equations

• FinBddDistLat.instInhabitedFinBddDistLat = { default := FinBddDistLat.of PUnit.{u_1 + 1} }

instance FinBddDistLat.largeCategory : CategoryTheory.LargeCategory FinBddDistLat

Equations

• FinBddDistLat.largeCategory = CategoryTheory.InducedCategory.category FinBddDistLat.toBddDistLat

instance FinBddDistLat.concreteCategory : CategoryTheory.ConcreteCategory FinBddDistLat

Equations

• FinBddDistLat.concreteCategory = CategoryTheory.InducedCategory.concreteCategory FinBddDistLat.toBddDistLat

instance FinBddDistLat.hasForgetToBddDistLat : CategoryTheory.HasForget₂ FinBddDistLat BddDistLat

Equations

• FinBddDistLat.hasForgetToBddDistLat = CategoryTheory.InducedCategory.hasForget₂ FinBddDistLat.toBddDistLat

instance FinBddDistLat.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ FinBddDistLat FinPartOrd

Equations

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

@[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 = (OrderIso.symm e) a

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

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.

@[simp]

theorem FinBddDistLat.dual_map {X : FinBddDistLat} {Y : FinBddDistLat} (a : BoundedLatticeHom ↑(BddDistLat.toBddLat X.toBddDistLat).toLat ↑(BddDistLat.toBddLat Y.toBddDistLat).toLat) : FinBddDistLat.dual.toPrefunctor.map a = BoundedLatticeHom.dual a

@[simp]

theorem FinBddDistLat.dual_obj (X : FinBddDistLat) : FinBddDistLat.dual.toPrefunctor.obj X = FinBddDistLat.of (↑X.toBddDistLat.toDistLat)ᵒᵈ

def FinBddDistLat.dual : CategoryTheory.Functor FinBddDistLat FinBddDistLat

OrderDual as a functor.

Equations

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

@[simp]

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

@[simp]

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

def FinBddDistLat.dualEquiv : FinBddDistLat ≌ FinBddDistLat

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

Equations

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

theorem finBddDistLat_dual_comp_forget_to_bddDistLat : CategoryTheory.Functor.comp FinBddDistLat.dual (CategoryTheory.forget₂ FinBddDistLat BddDistLat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ FinBddDistLat BddDistLat) BddDistLat.dual