order.category.BddLat - mathlib docs

source

structure BddLat :

Type (u_1+1)

to_Lat : Lat
is_bounded_order : bounded_order ↥(self.to_Lat)

The category of bounded lattices with bounded lattice morphisms.

Instances for BddLat

source

@[protected, instance]

def BddLat.has_coe_to_sort :

has_coe_to_sort BddLat (Type u_1)

Equations

BddLat.has_coe_to_sort = {coe := λ (X : BddLat), ↥(X.to_Lat)}

source

@[protected, instance]

def BddLat.lattice (X : BddLat) :

lattice ↥X

Equations

X.lattice = X.to_Lat.str

source

def BddLat.of (α : Type u_1) [lattice α] [bounded_order α] :

BddLat

Construct a bundled BddLat from lattice + bounded_order.

Equations

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

source

@[simp]

theorem BddLat.coe_of (α : Type u_1) [lattice α] [bounded_order α] :

↥(BddLat.of α) = α

source

@[protected, instance]

def BddLat.inhabited :

inhabited BddLat

Equations

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

source

@[protected, instance]

def BddLat.category_theory.large_category :

category_theory.large_category BddLat

Equations

BddLat.category_theory.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : BddLat), bounded_lattice_hom ↥X ↥Y}, id := λ (X : BddLat), bounded_lattice_hom.id ↥X, comp := λ (X Y Z : BddLat) (f : X ⟶ Y) (g : Y ⟶ Z), bounded_lattice_hom.comp g f}, id_comp' := BddLat.category_theory.large_category._proof_1, comp_id' := BddLat.category_theory.large_category._proof_2, assoc' := BddLat.category_theory.large_category._proof_3}

source

@[protected, instance]

def BddLat.category_theory.concrete_category :

category_theory.concrete_category BddLat

Equations

BddLat.category_theory.concrete_category = category_theory.concrete_category.mk {obj := coe_sort BddLat.has_coe_to_sort, map := λ (X Y : BddLat), coe_fn, map_id' := BddLat.category_theory.concrete_category._proof_1, map_comp' := BddLat.category_theory.concrete_category._proof_2}

source

@[protected, instance]

def BddLat.has_forget_to_BddOrd :

category_theory.has_forget₂ BddLat BddOrd

Equations

BddLat.has_forget_to_BddOrd = {forget₂ := {obj := λ (X : BddLat), BddOrd.of ↥X, map := λ (X Y : BddLat), bounded_lattice_hom.to_bounded_order_hom, map_id' := BddLat.has_forget_to_BddOrd._proof_1, map_comp' := BddLat.has_forget_to_BddOrd._proof_2}, forget_comp := BddLat.has_forget_to_BddOrd._proof_3}

source

@[protected, instance]

def BddLat.has_forget_to_Lat :

category_theory.has_forget₂ BddLat Lat

Equations

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

source

@[protected, instance]

def BddLat.has_forget_to_SemilatSup :

category_theory.has_forget₂ BddLat SemilatSup

Equations

BddLat.has_forget_to_SemilatSup = {forget₂ := {obj := λ (X : BddLat), SemilatSup.mk ↥X, map := λ (X Y : BddLat), bounded_lattice_hom.to_sup_bot_hom, map_id' := BddLat.has_forget_to_SemilatSup._proof_1, map_comp' := BddLat.has_forget_to_SemilatSup._proof_2}, forget_comp := BddLat.has_forget_to_SemilatSup._proof_3}

source

@[protected, instance]

def BddLat.has_forget_to_SemilatInf :

category_theory.has_forget₂ BddLat SemilatInf

Equations

BddLat.has_forget_to_SemilatInf = {forget₂ := {obj := λ (X : BddLat), SemilatInf.mk ↥X, map := λ (X Y : BddLat), bounded_lattice_hom.to_inf_top_hom, map_id' := BddLat.has_forget_to_SemilatInf._proof_1, map_comp' := BddLat.has_forget_to_SemilatInf._proof_2}, forget_comp := BddLat.has_forget_to_SemilatInf._proof_3}

source

@[simp]

theorem BddLat.coe_forget_to_BddOrd (X : BddLat) :

↥((category_theory.forget₂ BddLat BddOrd).obj X) = ↥X

source

@[simp]

theorem BddLat.coe_forget_to_Lat (X : BddLat) :

↥((category_theory.forget₂ BddLat Lat).obj X) = ↥X

source

@[simp]

theorem BddLat.coe_forget_to_SemilatSup (X : BddLat) :

↥((category_theory.forget₂ BddLat SemilatSup).obj X) = ↥X

source

@[simp]

theorem BddLat.coe_forget_to_SemilatInf (X : BddLat) :

↥((category_theory.forget₂ BddLat SemilatInf).obj X) = ↥X

source

theorem BddLat.forget_Lat_PartOrd_eq_forget_BddOrd_PartOrd :

category_theory.forget₂ BddLat Lat ⋙ category_theory.forget₂ Lat PartOrd = category_theory.forget₂ BddLat BddOrd ⋙ category_theory.forget₂ BddOrd PartOrd

source

theorem BddLat.forget_SemilatSup_PartOrd_eq_forget_BddOrd_PartOrd :

category_theory.forget₂ BddLat SemilatSup ⋙ category_theory.forget₂ SemilatSup PartOrd = category_theory.forget₂ BddLat BddOrd ⋙ category_theory.forget₂ BddOrd PartOrd

source

theorem BddLat.forget_SemilatInf_PartOrd_eq_forget_BddOrd_PartOrd :

category_theory.forget₂ BddLat SemilatInf ⋙ category_theory.forget₂ SemilatInf PartOrd = category_theory.forget₂ BddLat BddOrd ⋙ category_theory.forget₂ BddOrd PartOrd

source

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

α ≅ β

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

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem BddLat.dual_obj (X : BddLat) :

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

source

@[simp]

theorem BddLat.dual_map (X Y : BddLat) (ᾰ : bounded_lattice_hom ↥X ↥Y) :

BddLat.dual.map ᾰ = ⇑bounded_lattice_hom.dual ᾰ

source

def BddLat.dual :

BddLat ⥤ BddLat

order_dual as a functor.

Equations

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

source

def BddLat.dual_equiv :

BddLat ≌ BddLat

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

Equations

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

source

@[simp]

theorem BddLat.dual_equiv_functor :

BddLat.dual_equiv.functor = BddLat.dual

source

@[simp]

theorem BddLat.dual_equiv_inverse :

BddLat.dual_equiv.inverse = BddLat.dual

source

theorem BddLat_dual_comp_forget_to_BddOrd :

BddLat.dual ⋙ category_theory.forget₂ BddLat BddOrd = category_theory.forget₂ BddLat BddOrd ⋙ BddOrd.dual

source

theorem BddLat_dual_comp_forget_to_Lat :

BddLat.dual ⋙ category_theory.forget₂ BddLat Lat = category_theory.forget₂ BddLat Lat ⋙ Lat.dual

source

theorem BddLat_dual_comp_forget_to_SemilatSup :

BddLat.dual ⋙ category_theory.forget₂ BddLat SemilatSup = category_theory.forget₂ BddLat SemilatInf ⋙ SemilatInf.dual

source

theorem BddLat_dual_comp_forget_to_SemilatInf :

BddLat.dual ⋙ category_theory.forget₂ BddLat SemilatInf = category_theory.forget₂ BddLat SemilatSup ⋙ SemilatSup.dual

source

def Lat_to_BddLat :

Lat ⥤ BddLat

The functor that adds a bottom and a top element to a lattice. This is the free functor.

Equations

Lat_to_BddLat = {obj := λ (X : Lat), BddLat.of (with_top (with_bot ↥X)), map := λ (X Y : Lat), lattice_hom.with_top_with_bot, map_id' := Lat_to_BddLat._proof_1, map_comp' := Lat_to_BddLat._proof_2}

source

def Lat_to_BddLat_forget_adjunction :

Lat_to_BddLat ⊣ category_theory.forget₂ BddLat Lat

Lat_to_BddLat is left adjoint to the forgetful functor, meaning it is the free functor from Lat to BddLat.

Equations

Lat_to_BddLat_forget_adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Lat) (Y : BddLat), {to_fun := λ (f : Lat_to_BddLat.obj X ⟶ Y), {to_sup_hom := {to_fun := ⇑f ∘ option.some ∘ option.some, map_sup' := _}, map_inf' := _}, inv_fun := lattice_hom.with_top_with_bot' Y.is_bounded_order, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := Lat_to_BddLat_forget_adjunction._proof_5, hom_equiv_naturality_right' := Lat_to_BddLat_forget_adjunction._proof_6}

mathlib documentation

The category of bounded lattices #