The category of bounded lattices

This file defines BddLat, the category of bounded lattices.

In literature, this is sometimes called Lat, the category of lattices, because being a lattice is understood to entail having a bottom and a top element.

structure BddLat : Type (u_1 + 1)

The category of bounded lattices with bounded lattice morphisms.

• toLat : Lat

  The underlying lattice of a bounded lattice.

• isBoundedOrder : BoundedOrder ↑self.toLat

instance BddLat.instCoeSortBddLatType : CoeSort BddLat (Type u_1)

Equations

• BddLat.instCoeSortBddLatType = { coe := fun (X : BddLat) => ↑X.toLat }

instance BddLat.instLatticeαToLat (X : BddLat) : Lattice ↑X.toLat

Equations

• BddLat.instLatticeαToLat X = X.toLat.str

def BddLat.of (α : Type u_1) [Lattice α] [BoundedOrder α] : BddLat

Construct a bundled BddLat from Lattice + BoundedOrder.

Equations

• BddLat.of α = BddLat.mk (CategoryTheory.Bundled.mk α)

@[simp]

theorem BddLat.coe_of (α : Type u_1) [Lattice α] [BoundedOrder α] : ↑(BddLat.of α).toLat = α

instance BddLat.instInhabitedBddLat : Inhabited BddLat

Equations

• BddLat.instInhabitedBddLat = { default := BddLat.of PUnit.{u_1 + 1} }

instance BddLat.instLargeCategoryBddLat : CategoryTheory.LargeCategory BddLat

Equations

• BddLat.instLargeCategoryBddLat = CategoryTheory.Category.mk

instance BddLat.instFunLike (X : BddLat) (Y : BddLat) : FunLike (X ⟶ Y) ↑X.toLat ↑Y.toLat

Equations

• BddLat.instFunLike X Y = let_fun this := inferInstance; this

instance BddLat.instConcreteCategoryBddLatInstLargeCategoryBddLat : CategoryTheory.ConcreteCategory BddLat

Equations

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

instance BddLat.hasForgetToBddOrd : CategoryTheory.HasForget₂ BddLat BddOrd

Equations

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

instance BddLat.hasForgetToLat : CategoryTheory.HasForget₂ BddLat Lat

Equations

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

instance BddLat.hasForgetToSemilatSup : CategoryTheory.HasForget₂ BddLat SemilatSupCat

Equations

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

instance BddLat.hasForgetToSemilatInf : CategoryTheory.HasForget₂ BddLat SemilatInfCat

Equations

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

@[simp]

theorem BddLat.coe_forget_to_bddOrd (X : BddLat) : ↑((CategoryTheory.forget₂ BddLat BddOrd).toPrefunctor.obj X).toPartOrd = ↑X.toLat

@[simp]

theorem BddLat.coe_forget_to_lat (X : BddLat) : ↑((CategoryTheory.forget₂ BddLat Lat).toPrefunctor.obj X) = ↑X.toLat

@[simp]

theorem BddLat.coe_forget_to_semilatSup (X : BddLat) : ((CategoryTheory.forget₂ BddLat SemilatSupCat).toPrefunctor.obj X).X = ↑X.toLat

@[simp]

theorem BddLat.coe_forget_to_semilatInf (X : BddLat) : ((CategoryTheory.forget₂ BddLat SemilatInfCat).toPrefunctor.obj X).X = ↑X.toLat

theorem BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd : CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat Lat) (CategoryTheory.forget₂ Lat PartOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat BddOrd) (CategoryTheory.forget₂ BddOrd PartOrd)

theorem BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd : CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat SemilatSupCat) (CategoryTheory.forget₂ SemilatSupCat PartOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat BddOrd) (CategoryTheory.forget₂ BddOrd PartOrd)

theorem BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd : CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat SemilatInfCat) (CategoryTheory.forget₂ SemilatInfCat PartOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat BddOrd) (CategoryTheory.forget₂ BddOrd PartOrd)

@[simp]

theorem BddLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BddLat} {β : BddLat} (e : ↑α.toLat ≃o ↑β.toLat) (a : ↑β.toLat) : (BddLat.Iso.mk e).inv.toSupHom a = (OrderIso.symm e) a

@[simp]

theorem BddLat.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BddLat} {β : BddLat} (e : ↑α.toLat ≃o ↑β.toLat) (a : ↑α.toLat) : (BddLat.Iso.mk e).hom.toSupHom a = e a

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

Constructs an equivalence between bounded lattices from an order isomorphism between them.

Equations

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

@[simp]

theorem BddLat.dual_obj (X : BddLat) : BddLat.dual.toPrefunctor.obj X = BddLat.of (↑X.toLat)ᵒᵈ

@[simp]

theorem BddLat.dual_map {X : BddLat} {Y : BddLat} (a : BoundedLatticeHom ↑X.toLat ↑Y.toLat) : BddLat.dual.toPrefunctor.map a = BoundedLatticeHom.dual a

def BddLat.dual : CategoryTheory.Functor BddLat BddLat

OrderDual as a functor.

Equations

• BddLat.dual = CategoryTheory.Functor.mk { obj := fun (X : BddLat) => BddLat.of (↑X.toLat)ᵒᵈ, map := fun {X Y : BddLat} => ⇑BoundedLatticeHom.dual }

@[simp]

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

@[simp]

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

def BddLat.dualEquiv : BddLat ≌ BddLat

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

Equations

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

theorem bddLat_dual_comp_forget_to_bddOrd : CategoryTheory.Functor.comp BddLat.dual (CategoryTheory.forget₂ BddLat BddOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat BddOrd) BddOrd.dual

theorem bddLat_dual_comp_forget_to_lat : CategoryTheory.Functor.comp BddLat.dual (CategoryTheory.forget₂ BddLat Lat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat Lat) Lat.dual

theorem bddLat_dual_comp_forget_to_semilatSupCat : CategoryTheory.Functor.comp BddLat.dual (CategoryTheory.forget₂ BddLat SemilatSupCat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat SemilatInfCat) SemilatInfCat.dual

theorem bddLat_dual_comp_forget_to_semilatInfCat : CategoryTheory.Functor.comp BddLat.dual (CategoryTheory.forget₂ BddLat SemilatInfCat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ BddLat SemilatSupCat) SemilatSupCat.dual

def latToBddLat : CategoryTheory.Functor Lat BddLat

The functor that adds a bottom and a top element to a lattice. This is the free functor.

Equations

• latToBddLat = CategoryTheory.Functor.mk { obj := fun (X : Lat) => BddLat.of (WithTop (WithBot ↑X)), map := fun {X Y : Lat} => LatticeHom.withTopWithBot }

def latToBddLatForgetAdjunction : latToBddLat ⊣ CategoryTheory.forget₂ BddLat Lat

latToBddLat is left adjoint to the forgetful functor, meaning it is the free functor from Lat to BddLat.

Equations

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

def latToBddLatCompDualIsoDualCompLatToBddLat : CategoryTheory.Functor.comp latToBddLat BddLat.dual ≅ CategoryTheory.Functor.comp Lat.dual latToBddLat

latToBddLat and OrderDual commute.

Equations

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