The category of distributive lattices

This file defines DistLat, the category of distributive lattices.

Note that DistLat in the literature doesn't always correspond to DistLat as we don't require bottom or top elements. Instead, this DistLat corresponds to BddDistLat.

structure DistLat : Type (u_1 + 1)

The category of distributive lattices.

• carrier : Type u_1

  The underlying distributive lattice.

• str : DistribLattice ↑self

@[implicit_reducible]

instance DistLat.instCoeSortType : CoeSort DistLat (Type u)

@[reducible, inline]

abbrev DistLat.of (X : Type u_1) [DistribLattice X] : DistLat

Construct a bundled DistLat from the underlying type and typeclass.

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

The type of morphisms in DistLat R.

• hom' : LatticeHom ↑X ↑Y

  The underlying LatticeHom.

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[reducible, inline]

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

Turn a morphism in DistLat back into a LatticeHom.

@[reducible, inline]

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

Typecheck a LatticeHom as a morphism in DistLat.

def DistLat.Hom.Simps.hom (X Y : DistLat) (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 DistLat.coe_id {X : DistLat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

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

@[simp]

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

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

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

theorem DistLat.coe_of (X : Type u) [DistribLattice X] : ↑(of X) = X

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[implicit_reducible]

instance DistLat.hasForgetToLat : CategoryTheory.HasForget₂ DistLat Lat

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

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

@[simp]

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

@[simp]

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

def DistLat.dual : CategoryTheory.Functor DistLat DistLat

OrderDual as a functor.

@[simp]

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

def DistLat.dualEquiv : DistLat ≌ DistLat

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

@[simp]

theorem DistLat.dualEquiv_inverse : dualEquiv.inverse = dual

@[simp]

theorem DistLat.dualEquiv_functor : dualEquiv.functor = dual

theorem distLat_dual_comp_forget_to_Lat : DistLat.dual.comp (CategoryTheory.forget₂ DistLat Lat) = (CategoryTheory.forget₂ DistLat Lat).comp Lat.dual