The category of finite bounded distributive lattices

This file defines FinBddDistLat, the category of finite distributive lattices with bounded lattice homomorphisms.

structure FinBddDistLatextends BddDistLat : Type (u_1 + 1)

The category of finite distributive lattices with bounded lattice morphisms.

• carrier : Type u_1
• str : DistribLattice ↑self.toDistLat
• isBoundedOrder : BoundedOrder ↑self.toDistLat
• isFintype : Fintype ↑self.toDistLat

instance FinBddDistLat.instCoeSortType : CoeSort FinBddDistLat (Type u_1)

instance FinBddDistLat.instDistribLatticeCarrier (X : FinBddDistLat) : DistribLattice ↑X.toDistLat

instance FinBddDistLat.instBoundedOrderCarrier (X : FinBddDistLat) : BoundedOrder ↑X.toDistLat

@[reducible, inline]

abbrev FinBddDistLat.of (α : Type u_1) [DistribLattice α] [BoundedOrder α] [Fintype α] : FinBddDistLat

Construct a bundled FinBddDistLat from a Fintype BoundedOrder DistribLattice.

@[reducible, inline]

abbrev FinBddDistLat.of' (α : Type u_1) [DistribLattice α] [Fintype α] [Nonempty α] : FinBddDistLat

Construct a bundled FinBddDistLat from a Nonempty Fintype DistribLattice.

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

The type of morphisms in FinBddDistLat R.

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

  The underlying BoundedLatticeHom.

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

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

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

instance FinBddDistLat.instConcreteCategoryBoundedLatticeHomCarrier : CategoryTheory.ConcreteCategory FinBddDistLat fun (x1 x2 : FinBddDistLat) => BoundedLatticeHom ↑x1.toDistLat ↑x2.toDistLat

@[reducible, inline]

abbrev FinBddDistLat.Hom.hom {X Y : FinBddDistLat} (f : X.Hom Y) : BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat

Turn a morphism in FinBddDistLat back into a BoundedLatticeHom.

@[reducible, inline]

abbrev FinBddDistLat.ofHom {X Y : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] [DistribLattice Y] [BoundedOrder Y] [Fintype Y] (f : BoundedLatticeHom X Y) : of X ⟶ of Y

Typecheck a BoundedLatticeHom as a morphism in FinBddDistLat.

def FinBddDistLat.Hom.Simps.hom (X Y : FinBddDistLat) (f : X.Hom Y) : BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat

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 FinBddDistLat.coe_id {X : FinBddDistLat} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem FinBddDistLat.hom_id {X : FinBddDistLat} : Hom.hom (CategoryTheory.CategoryStruct.id X) = BoundedLatticeHom.id ↑X.toDistLat

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

@[simp]

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

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

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

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

@[simp]

theorem FinBddDistLat.hom_ofHom {X Y : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] [DistribLattice Y] [BoundedOrder Y] [Fintype Y] (f : BoundedLatticeHom X Y) : Hom.hom (ofHom f) = f

@[simp]

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

@[simp]

theorem FinBddDistLat.ofHom_id {X : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] : ofHom (BoundedLatticeHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem FinBddDistLat.ofHom_comp {X Y Z : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] [DistribLattice Y] [BoundedOrder Y] [Fintype Y] [DistribLattice Z] [BoundedOrder Z] [Fintype Z] (f : BoundedLatticeHom X Y) (g : BoundedLatticeHom Y Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem FinBddDistLat.ofHom_apply {X Y : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] [DistribLattice Y] [BoundedOrder Y] [Fintype Y] (f : BoundedLatticeHom X Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

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

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

instance FinBddDistLat.instInhabited : Inhabited FinBddDistLat

instance FinBddDistLat.hasForgetToBddDistLat : CategoryTheory.HasForget₂ FinBddDistLat BddDistLat

instance FinBddDistLat.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ FinBddDistLat FinPartOrd

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

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

@[simp]

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

@[simp]

theorem FinBddDistLat.Iso.mk_inv {α β : FinBddDistLat} (e : ↑α.toDistLat ≃o ↑β.toDistLat) : (mk e).inv = ofHom (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })

def FinBddDistLat.dual : CategoryTheory.Functor FinBddDistLat FinBddDistLat

OrderDual as a functor.

@[simp]

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

def FinBddDistLat.dualEquiv : FinBddDistLat ≌ FinBddDistLat

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

@[simp]

theorem FinBddDistLat.dualEquiv_functor : dualEquiv.functor = dual

@[simp]

theorem FinBddDistLat.dualEquiv_inverse : dualEquiv.inverse = dual

theorem finBddDistLat_dual_comp_forget_to_bddDistLat : FinBddDistLat.dual.comp (CategoryTheory.forget₂ FinBddDistLat BddDistLat) = (CategoryTheory.forget₂ FinBddDistLat BddDistLat).comp BddDistLat.dual