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.instCoeSortType : CoeSort FinBddDistLat (Type u_1)

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

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 { α := α, str := inferInstance })

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 { α := α, str := inferInstance })

instance FinBddDistLat.instInhabited : Inhabited FinBddDistLat

Equations

• FinBddDistLat.instInhabited = { default := FinBddDistLat.of PUnit.{?u.3 + 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.

def FinBddDistLat.Iso.mk {α β : 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.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α β : 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} (e : ↑α.toBddDistLat.toDistLat ≃o ↑β.toBddDistLat.toDistLat) (a : ↑β.toBddDistLat.toDistLat) : (FinBddDistLat.Iso.mk e).inv.toSupHom a = e.symm a

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.dual_obj (X : FinBddDistLat) : FinBddDistLat.dual.obj X = FinBddDistLat.of (↑X.toBddDistLat.toDistLat)ᵒᵈ

@[simp]

theorem FinBddDistLat.dual_map {x✝ x✝¹ : FinBddDistLat} (a : BoundedLatticeHom ↑x✝.toBddDistLat.toBddLat.toLat ↑x✝¹.toBddDistLat.toBddLat.toLat) : FinBddDistLat.dual.map a = BoundedLatticeHom.dual a

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.

@[simp]

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

@[simp]

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

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