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 BddLatextends Lat : Type (u_1 + 1)

The category of bounded lattices with bounded lattice morphisms.

• carrier : Type u_1
• str : Lattice ↑self.toLat
• isBoundedOrder : BoundedOrder ↑self.toLat

instance BddLat.instCoeSortType : CoeSort BddLat (Type u_1)

Equations

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

@[reducible, inline]

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

Construct a bundled BddLat from Lattice + BoundedOrder.

Equations

• BddLat.of α = BddLat.mk (Lat.mk α)

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

structure BddLat.Hom (X Y : BddLat) : Type u

The type of morphisms in BddLat.

• hom' : BoundedLatticeHom ↑X.toLat ↑Y.toLat

  The underlying BoundedLatticeHom.

theorem BddLat.Hom.ext {X Y : BddLat} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

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.instConcreteCategoryBoundedLatticeHomCarrier : CategoryTheory.ConcreteCategory BddLat fun (x1 x2 : BddLat) => BoundedLatticeHom ↑x1.toLat ↑x2.toLat

Equations

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

@[reducible, inline]

abbrev BddLat.Hom.hom {X Y : BddLat} (f : X.Hom Y) : BoundedLatticeHom ↑X.toLat ↑Y.toLat

Turn a morphism in BddLat back into a BoundedLatticeHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev BddLat.ofHom {X Y : Type u} [Lattice X] [BoundedOrder X] [Lattice Y] [BoundedOrder Y] (f : BoundedLatticeHom X Y) : of X ⟶ of Y

Typecheck a BoundedLatticeHom as a morphism in BddLat.

Equations

• BddLat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def BddLat.Hom.Simps.hom (X Y : BddLat) (f : X.Hom Y) : BoundedLatticeHom ↑X.toLat ↑Y.toLat

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• BddLat.Hom.Simps.hom X Y f = f.hom

@[simp]

theorem BddLat.hom_id {X : Lat} : Lat.Hom.hom (CategoryTheory.CategoryStruct.id X) = LatticeHom.id ↑X

theorem BddLat.id_apply (X : Lat) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem BddLat.hom_comp {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) : Lat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Lat.Hom.hom g).comp (Lat.Hom.hom f)

theorem BddLat.comp_apply {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem BddLat.ext {X Y : BddLat} {f g : X ⟶ Y} (w : ∀ (x : ↑X.toLat), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem BddLat.hom_ext {X Y : BddLat} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

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} (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_inv {α β : BddLat} (e : ↑α.toLat ≃o ↑β.toLat) : (mk e).inv = ofHom (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })

@[simp]

theorem BddLat.Iso.mk_hom {α β : BddLat} (e : ↑α.toLat ≃o ↑β.toLat) : (mk e).hom = ofHom (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })

def BddLat.dual : CategoryTheory.Functor BddLat BddLat

OrderDual as a functor.

Equations

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

@[simp]

theorem BddLat.dual_map {X✝ Y✝ : BddLat} (f : X✝ ⟶ Y✝) : dual.map f = ofHom (BoundedLatticeHom.dual (Hom.hom f))

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_functor : dualEquiv.functor = dual

@[simp]

theorem BddLat.dualEquiv_inverse : dualEquiv.inverse = 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

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

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)