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

Equations

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

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

Equations

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

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

Construct a bundled BddLat from Lattice + BoundedOrder.

Equations

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

@[simp]

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

instance BddLat.instInhabited : Inhabited BddLat

Equations

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

instance BddLat.instLargeCategory : CategoryTheory.LargeCategory BddLat

Equations

• BddLat.instLargeCategory = CategoryTheory.Category.mk @BddLat.instLargeCategory.proof_1 @BddLat.instLargeCategory.proof_2 @BddLat.instLargeCategory.proof_3

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

Equations

• X.instFunLike Y = inferInstance

instance BddLat.instConcreteCategory : 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).obj X).toPartOrd = ↑X.toLat

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BddLat} {β : BddLat} (e : ↑α.toLat ≃o ↑β.toLat) (a : ↑α.toLat) : (BddLat.Iso.mk e).hom.toSupHom a = e a

@[simp]

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

def BddLat.dual : CategoryTheory.Functor BddLat BddLat

OrderDual as a functor.

Equations

• BddLat.dual = { obj := fun (X : BddLat) => BddLat.of (↑X.toLat)ᵒᵈ, map := fun {x x_1 : BddLat} => ⇑BoundedLatticeHom.dual, map_id := BddLat.dual.proof_1, map_comp := @BddLat.dual.proof_2 }

@[simp]

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

@[simp]

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

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.

@[simp]

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

@[simp]

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

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

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

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

theorem bddLat_dual_comp_forget_to_semilatInfCat : BddLat.dual.comp (CategoryTheory.forget₂ BddLat SemilatInfCat) = (CategoryTheory.forget₂ BddLat SemilatSupCat).comp 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 = { obj := fun (X : Lat) => BddLat.of (WithTop (WithBot ↑X)), map := fun {X Y : Lat} => LatticeHom.withTopWithBot, map_id := latToBddLat.proof_1, map_comp := @latToBddLat.proof_2 }

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 : latToBddLat.comp BddLat.dual ≅ Lat.dual.comp latToBddLat

latToBddLat and OrderDual commute.

Equations

• latToBddLatCompDualIsoDualCompLatToBddLat = (latToBddLatForgetAdjunction.comp BddLat.dualEquiv.toAdjunction).leftAdjointUniq (Lat.dualEquiv.toAdjunction.comp latToBddLatForgetAdjunction)