The category of bounded distributive lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines BddDistLat, the category of bounded distributive lattices.

Note that this category is sometimes called DistLat when being a lattice is understood to entail having a bottom and a top element.

source

structure BddDistLat :

Type (u_1+1)

to_DistLat : DistLat
is_bounded_order : bounded_order ↥(self.to_DistLat)

The category of bounded distributive lattices with bounded lattice morphisms.

Instances for BddDistLat

source

@[protected, instance]

def BddDistLat.has_coe_to_sort :

has_coe_to_sort BddDistLat (Type u_1)

Equations

BddDistLat.has_coe_to_sort = {coe := λ (X : BddDistLat), ↥(X.to_DistLat)}

source

@[protected, instance]

def BddDistLat.distrib_lattice (X : BddDistLat) :

distrib_lattice ↥X

Equations

X.distrib_lattice = X.to_DistLat.str

source

def BddDistLat.of (α : Type u_1) [distrib_lattice α] [bounded_order α] :

BddDistLat

Construct a bundled BddDistLat from a bounded_order distrib_lattice.

Equations

BddDistLat.of α = BddDistLat.mk {α := α, str := _inst_1}

source

@[simp]

theorem BddDistLat.coe_of (α : Type u_1) [distrib_lattice α] [bounded_order α] :

↥(BddDistLat.of α) = α

source

@[protected, instance]

def BddDistLat.inhabited :

inhabited BddDistLat

Equations

BddDistLat.inhabited = {default := BddDistLat.of punit boolean_algebra.to_bounded_order}

source

def BddDistLat.to_BddLat (X : BddDistLat) :

BddLat

Turn a BddDistLat into a BddLat by forgetting it is distributive.

Equations

X.to_BddLat = BddLat.of ↥X

source

@[simp]

theorem BddDistLat.coe_to_BddLat (X : BddDistLat) :

↥(X.to_BddLat) = ↥X

source

@[protected, instance]

def BddDistLat.category_theory.large_category :

category_theory.large_category BddDistLat

Equations

BddDistLat.category_theory.large_category = category_theory.induced_category.category BddDistLat.to_BddLat

source

@[protected, instance]

def BddDistLat.category_theory.concrete_category :

category_theory.concrete_category BddDistLat

Equations

BddDistLat.category_theory.concrete_category = category_theory.induced_category.concrete_category BddDistLat.to_BddLat

source

@[protected, instance]

def BddDistLat.has_forget_to_DistLat :

category_theory.has_forget₂ BddDistLat DistLat

Equations

BddDistLat.has_forget_to_DistLat = {forget₂ := {obj := λ (X : BddDistLat), {α := ↥X, str := X.distrib_lattice}, map := λ (X Y : BddDistLat), bounded_lattice_hom.to_lattice_hom, map_id' := BddDistLat.has_forget_to_DistLat._proof_1, map_comp' := BddDistLat.has_forget_to_DistLat._proof_2}, forget_comp := BddDistLat.has_forget_to_DistLat._proof_3}

source

@[protected, instance]

def BddDistLat.has_forget_to_BddLat :

category_theory.has_forget₂ BddDistLat BddLat

Equations

BddDistLat.has_forget_to_BddLat = category_theory.induced_category.has_forget₂ BddDistLat.to_BddLat

source

theorem BddDistLat.forget_BddLat_Lat_eq_forget_DistLat_Lat :

category_theory.forget₂ BddDistLat BddLat ⋙ category_theory.forget₂ BddLat Lat = category_theory.forget₂ BddDistLat DistLat ⋙ category_theory.forget₂ DistLat Lat

source

@[simp]

theorem BddDistLat.iso.mk_hom {α β : BddDistLat} (e : ↥α ≃o ↥β) :

(BddDistLat.iso.mk e).hom = ↑e

source

def BddDistLat.iso.mk {α β : BddDistLat} (e : ↥α ≃o ↥β) :

α ≅ β

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

Equations

BddDistLat.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem BddDistLat.iso.mk_inv {α β : BddDistLat} (e : ↥α ≃o ↥β) :

(BddDistLat.iso.mk e).inv = ↑(e.symm)

source

@[simp]

theorem BddDistLat.dual_obj (X : BddDistLat) :

BddDistLat.dual.obj X = BddDistLat.of (↥X)ᵒᵈ

source

@[simp]

theorem BddDistLat.dual_map (X Y : BddDistLat) (ᾰ : bounded_lattice_hom ↥(X.to_BddLat) ↥(Y.to_BddLat)) :

BddDistLat.dual.map ᾰ = ⇑bounded_lattice_hom.dual ᾰ

source

def BddDistLat.dual :

BddDistLat ⥤ BddDistLat

order_dual as a functor.

Equations

BddDistLat.dual = {obj := λ (X : BddDistLat), BddDistLat.of (↥X)ᵒᵈ, map := λ (X Y : BddDistLat), ⇑bounded_lattice_hom.dual, map_id' := BddDistLat.dual._proof_1, map_comp' := BddDistLat.dual._proof_2}

source

@[simp]

theorem BddDistLat.dual_equiv_inverse :

BddDistLat.dual_equiv.inverse = BddDistLat.dual

source

def BddDistLat.dual_equiv :

BddDistLat ≌ BddDistLat

The equivalence between BddDistLat and itself induced by order_dual both ways.

Equations

BddDistLat.dual_equiv = category_theory.equivalence.mk BddDistLat.dual BddDistLat.dual (category_theory.nat_iso.of_components (λ (X : BddDistLat), BddDistLat.iso.mk (order_iso.dual_dual ↥X)) BddDistLat.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : BddDistLat), BddDistLat.iso.mk (order_iso.dual_dual ↥X)) BddDistLat.dual_equiv._proof_2)

source

@[simp]

theorem BddDistLat.dual_equiv_functor :

BddDistLat.dual_equiv.functor = BddDistLat.dual

source

theorem BddDistLat_dual_comp_forget_to_DistLat :

BddDistLat.dual ⋙ category_theory.forget₂ BddDistLat DistLat = category_theory.forget₂ BddDistLat DistLat ⋙ DistLat.dual