The category of lattices

This defines Lat, the category of lattices.

Note that Lat doesn't correspond to the literature definition of [Lat] (https://ncatlab.org/nlab/show/Lat) as we don't require bottom or top elements. Instead, Lat corresponds to BddLat.

TODO

The free functor from Lat to BddLat is X → WithTop (WithBot X).

def Lat : Type (u_1 + 1)

The category of lattices.

Equations

• Lat = CategoryTheory.Bundled Lattice

instance Lat.instCoeSortType : CoeSort Lat (Type u_1)

Equations

• Lat.instCoeSortType = CategoryTheory.Bundled.coeSort

instance Lat.instLatticeα (X : Lat) : Lattice ↑X

Equations

• X.instLatticeα = X.str

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

Construct a bundled Lat from a Lattice.

Equations

• Lat.of α = CategoryTheory.Bundled.of α

@[simp]

theorem Lat.coe_of (α : Type u_1) [Lattice α] : ↑(Lat.of α) = α

instance Lat.instInhabited : Inhabited Lat

Equations

• Lat.instInhabited = { default := Lat.of Bool }

instance Lat.instBundledHomLatticeLatticeHom : CategoryTheory.BundledHom LatticeHom

Equations

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

instance Lat.instLargeCategory : CategoryTheory.LargeCategory Lat

Equations

• Lat.instLargeCategory = CategoryTheory.BundledHom.category LatticeHom

instance Lat.instConcreteCategory : CategoryTheory.ConcreteCategory Lat

Equations

• Lat.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory LatticeHom

instance Lat.hasForgetToPartOrd : CategoryTheory.HasForget₂ Lat PartOrd

Equations

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

@[simp]

theorem Lat.Iso.mk_hom_toSupHom_toFun {α : Lat} {β : Lat} (e : ↑α ≃o ↑β) (a : ↑α) : (Lat.Iso.mk e).hom.toSupHom a = e a

@[simp]

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

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

Constructs an isomorphism of lattices from an order isomorphism between them.

Equations

• Lat.Iso.mk e = { hom := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }, inv := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Lat.dual_map : ∀ {X Y : Lat} (a : LatticeHom ↑X ↑Y), Lat.dual.map a = LatticeHom.dual a

@[simp]

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

def Lat.dual : CategoryTheory.Functor Lat Lat

OrderDual as a functor.

Equations

• Lat.dual = { obj := fun (X : Lat) => Lat.of (↑X)ᵒᵈ, map := fun {X Y : Lat} => ⇑LatticeHom.dual, map_id := Lat.dual.proof_1, map_comp := @Lat.dual.proof_2 }

@[simp]

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

@[simp]

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

def Lat.dualEquiv : Lat ≌ Lat

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

Equations

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

theorem Lat_dual_comp_forget_to_partOrd : Lat.dual.comp (CategoryTheory.forget₂ Lat PartOrd) = (CategoryTheory.forget₂ Lat PartOrd).comp PartOrd.dual