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).

structure Lat : Type (u_1 + 1)

The category of lattices.

• carrier : Type u_1

  The underlying lattices.

• str : Lattice ↑self

@[implicit_reducible]

instance Lat.instCoeSortType : CoeSort Lat (Type u_1)

@[reducible, inline]

abbrev Lat.of (X : Type u_1) [Lattice X] : Lat

Construct a bundled Lat from the underlying type and typeclass.

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

The type of morphisms in Lat R.

• hom' : LatticeHom ↑X ↑Y

  The underlying LatticeHom.

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

theorem Lat.Hom.ext_iff {X Y : Lat} {x y : X.Hom Y} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

instance Lat.instCategory : CategoryTheory.Category.{u, u + 1} Lat

@[implicit_reducible]

instance Lat.instConcreteCategoryLatticeHomCarrier : CategoryTheory.ConcreteCategory Lat fun (x1 x2 : Lat) => LatticeHom ↑x1 ↑x2

@[reducible, inline]

abbrev Lat.Hom.hom {X Y : Lat} (f : X.Hom Y) : LatticeHom ↑X ↑Y

Turn a morphism in Lat back into a LatticeHom.

@[reducible, inline]

abbrev Lat.ofHom {X Y : Type u} [Lattice X] [Lattice Y] (f : LatticeHom X Y) : of X ⟶ of Y

Typecheck a LatticeHom as a morphism in Lat.

def Lat.Hom.Simps.hom (X Y : Lat) (f : X.Hom Y) : LatticeHom ↑X ↑Y

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

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem Lat.coe_id {X : Lat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem Lat.coe_comp {X Y Z : Lat} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem Lat.forget_map {X Y : Lat} (f : X ⟶ Y) : (CategoryTheory.forget Lat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

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

theorem Lat.ext_iff {X Y : Lat} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem Lat.coe_of (X : Type u) [Lattice X] : ↑(of X) = X

@[simp]

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

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

@[simp]

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

theorem Lat.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 Lat.hom_ext {X Y : Lat} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem Lat.hom_ext_iff {X Y : Lat} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem Lat.hom_ofHom {X Y : Type u} [Lattice X] [Lattice Y] (f : LatticeHom X Y) : Hom.hom (ofHom f) = f

@[simp]

theorem Lat.ofHom_hom {X Y : Lat} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem Lat.ofHom_id {X : Type u} [Lattice X] : ofHom (LatticeHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem Lat.ofHom_comp {X Y Z : Type u} [Lattice X] [Lattice Y] [Lattice Z] (f : LatticeHom X Y) (g : LatticeHom Y Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem Lat.ofHom_apply {X Y : Type u} [Lattice X] [Lattice Y] (f : LatticeHom X Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem Lat.inv_hom_apply {X Y : Lat} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem Lat.hom_inv_apply {X Y : Lat} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

@[implicit_reducible]

instance Lat.hasForgetToPartOrd : CategoryTheory.HasForget₂ Lat PartOrd

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

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

@[simp]

theorem Lat.Iso.mk_hom {α β : Lat} (e : ↑α ≃o ↑β) : (mk e).hom = ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem Lat.Iso.mk_inv {α β : Lat} (e : ↑α ≃o ↑β) : (mk e).inv = ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }

def Lat.dual : CategoryTheory.Functor Lat Lat

OrderDual as a functor.

@[simp]

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

def Lat.dualEquiv : Lat ≌ Lat

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

@[simp]

theorem Lat.dualEquiv_functor : dualEquiv.functor = dual

@[simp]

theorem Lat.dualEquiv_inverse : dualEquiv.inverse = dual

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