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

instance DistLat.instCoeSortType : CoeSort DistLat (Type u)

Equations

• DistLat.instCoeSortType = { coe := DistLat.carrier }

@[reducible, inline]

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

Construct a bundled DistLat from the underlying type and typeclass.

Equations

• DistLat.of X = DistLat.mk X

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 {X Y : DistLat} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

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

Equations

• DistLat.instCategory = CategoryTheory.Category.mk @DistLat.instCategory.proof_1 @DistLat.instCategory.proof_2 @DistLat.instCategory.proof_3

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

Equations

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

@[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.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[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.

Equations

• DistLat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

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

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

Equations

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

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

@[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

instance DistLat.hasForgetToLat : CategoryTheory.HasForget₂ DistLat Lat

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def DistLat.dual : CategoryTheory.Functor DistLat DistLat

OrderDual as a functor.

Equations

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

@[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.

Equations

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

@[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