order.category.Semilat - mathlib3 docs

source

structure SemilatSup :

Type (u+1)

X : Type ?
is_semilattice_sup : semilattice_sup self.X
is_order_bot : order_bot self.X

The category of sup-semilattices with a bottom element.

Instances for SemilatSup

SemilatSup.has_sizeof_inst
SemilatSup.has_coe_to_sort
SemilatSup.inhabited
SemilatSup.category_theory.large_category
SemilatSup.category_theory.concrete_category
SemilatSup.has_forget_to_PartOrd
BddLat.has_forget_to_SemilatSup

source

structure SemilatInf :

Type (u+1)

X : Type ?
is_semilattice_inf : semilattice_inf self.X
is_order_top : order_top self.X

The category of inf-semilattices with a top element.

Instances for SemilatInf

SemilatInf.has_sizeof_inst
SemilatInf.has_coe_to_sort
SemilatInf.inhabited
SemilatInf.category_theory.large_category
SemilatInf.category_theory.concrete_category
SemilatInf.has_forget_to_PartOrd
BddLat.has_forget_to_SemilatInf

source

@[protected, instance]

def SemilatSup.has_coe_to_sort :

has_coe_to_sort SemilatSup (Type u_1)

Equations

SemilatSup.has_coe_to_sort = {coe := SemilatSup.X}

source

def SemilatSup.of (α : Type u_1) [semilattice_sup α] [order_bot α] :

SemilatSup

Construct a bundled SemilatSup from a semilattice_sup.

Equations

SemilatSup.of α = SemilatSup.mk α

source

@[simp]

theorem SemilatSup.coe_of (α : Type u_1) [semilattice_sup α] [order_bot α] :

↥(SemilatSup.of α) = α

source

@[protected, instance]

def SemilatSup.inhabited :

inhabited SemilatSup

Equations

SemilatSup.inhabited = {default := SemilatSup.of punit generalized_boolean_algebra.to_order_bot}

source

@[protected, instance]

def SemilatSup.category_theory.large_category :

category_theory.large_category SemilatSup

Equations

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

source

@[protected, instance]

def SemilatSup.category_theory.concrete_category :

category_theory.concrete_category SemilatSup

Equations

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

source

@[protected, instance]

def SemilatSup.has_forget_to_PartOrd :

category_theory.has_forget₂ SemilatSup PartOrd

Equations

SemilatSup.has_forget_to_PartOrd = {forget₂ := {obj := λ (X : SemilatSup), {α := ↥X, str := semilattice_sup.to_partial_order ↥X X.is_semilattice_sup}, map := λ (X Y : SemilatSup) (f : X ⟶ Y), ↑f, map_id' := SemilatSup.has_forget_to_PartOrd._proof_1, map_comp' := SemilatSup.has_forget_to_PartOrd._proof_2}, forget_comp := SemilatSup.has_forget_to_PartOrd._proof_3}

source

@[simp]

theorem SemilatSup.coe_forget_to_PartOrd (X : SemilatSup) :

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

source

@[protected, instance]

def SemilatInf.has_coe_to_sort :

has_coe_to_sort SemilatInf (Type u_1)

Equations

SemilatInf.has_coe_to_sort = {coe := SemilatInf.X}

source

def SemilatInf.of (α : Type u_1) [semilattice_inf α] [order_top α] :

SemilatInf

Construct a bundled SemilatInf from a semilattice_inf.

Equations

SemilatInf.of α = SemilatInf.mk α

source

@[simp]

theorem SemilatInf.coe_of (α : Type u_1) [semilattice_inf α] [order_top α] :

↥(SemilatInf.of α) = α

source

@[protected, instance]

def SemilatInf.inhabited :

inhabited SemilatInf

Equations

SemilatInf.inhabited = {default := SemilatInf.of punit generalized_heyting_algebra.to_order_top}

source

@[protected, instance]

def SemilatInf.category_theory.large_category :

category_theory.large_category SemilatInf

Equations

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

source

@[protected, instance]

def SemilatInf.category_theory.concrete_category :

category_theory.concrete_category SemilatInf

Equations

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

source

@[protected, instance]

def SemilatInf.has_forget_to_PartOrd :

category_theory.has_forget₂ SemilatInf PartOrd

Equations

SemilatInf.has_forget_to_PartOrd = {forget₂ := {obj := λ (X : SemilatInf), {α := ↥X, str := semilattice_inf.to_partial_order ↥X X.is_semilattice_inf}, map := λ (X Y : SemilatInf) (f : X ⟶ Y), ↑f, map_id' := SemilatInf.has_forget_to_PartOrd._proof_1, map_comp' := SemilatInf.has_forget_to_PartOrd._proof_2}, forget_comp := SemilatInf.has_forget_to_PartOrd._proof_3}

source

@[simp]

theorem SemilatInf.coe_forget_to_PartOrd (X : SemilatInf) :

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

source

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

α ≅ β

Constructs an isomorphism of lattices from an order isomorphism between them.

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

def SemilatSup.dual :

SemilatSup ⥤ SemilatInf

order_dual as a functor.

Equations

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

source

@[simp]

theorem SemilatSup.dual_obj (X : SemilatSup) :

SemilatSup.dual.obj X = SemilatInf.of (↥X)ᵒᵈ

source

@[simp]

theorem SemilatSup.dual_map (X Y : SemilatSup) (ᾰ : sup_bot_hom ↥X ↥Y) :

SemilatSup.dual.map ᾰ = ⇑sup_bot_hom.dual ᾰ

source

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

α ≅ β

Constructs an isomorphism of lattices from an order isomorphism between them.

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem SemilatInf.dual_map (X Y : SemilatInf) (ᾰ : inf_top_hom ↥X ↥Y) :

SemilatInf.dual.map ᾰ = ⇑inf_top_hom.dual ᾰ

source

def SemilatInf.dual :

SemilatInf ⥤ SemilatSup

order_dual as a functor.

Equations

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

source

@[simp]

theorem SemilatInf.dual_obj (X : SemilatInf) :

SemilatInf.dual.obj X = SemilatSup.of (↥X)ᵒᵈ

source

@[simp]

theorem SemilatSup_equiv_SemilatInf_inverse :

SemilatSup_equiv_SemilatInf.inverse = SemilatInf.dual

source

@[simp]

theorem SemilatSup_equiv_SemilatInf_functor :

SemilatSup_equiv_SemilatInf.functor = SemilatSup.dual

source

def SemilatSup_equiv_SemilatInf :

SemilatSup ≌ SemilatInf

The equivalence between SemilatSup and SemilatInf induced by order_dual both ways.

Equations

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

source

theorem SemilatSup_dual_comp_forget_to_PartOrd :

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

source

theorem SemilatInf_dual_comp_forget_to_PartOrd :

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

mathlib3 documentation

The categories of semilattices #

References #

Order dual #