order.category.PartOrd - mathlib3 docs

source

def PartOrd :

Type (u_1+1)

The category of partially ordered types.

Equations

PartOrd = category_theory.bundled partial_order

Instances for PartOrd

source

@[protected, instance]

def PartOrd.partial_order.to_preorder.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection partial_order.to_preorder

Equations

PartOrd.partial_order.to_preorder.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def PartOrd.large_category :

category_theory.large_category PartOrd

source

@[protected, instance]

def PartOrd.concrete_category :

category_theory.concrete_category PartOrd

source

@[protected, instance]

def PartOrd.has_coe_to_sort :

has_coe_to_sort PartOrd (Type u_1)

Equations

PartOrd.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

def PartOrd.of (α : Type u_1) [partial_order α] :

PartOrd

Construct a bundled PartOrd from the underlying type and typeclass.

Equations

PartOrd.of α = category_theory.bundled.of α

source

@[simp]

theorem PartOrd.coe_of (α : Type u_1) [partial_order α] :

↥(PartOrd.of α) = α

source

@[protected, instance]

def PartOrd.inhabited :

inhabited PartOrd

Equations

PartOrd.inhabited = {default := PartOrd.of punit (semilattice_inf.to_partial_order punit)}

source

@[protected, instance]

def PartOrd.partial_order (α : PartOrd) :

partial_order ↥α

Equations

α.partial_order = α.str

source

@[protected, instance]

def PartOrd.has_forget_to_Preord :

category_theory.has_forget₂ PartOrd Preord

Equations

PartOrd.has_forget_to_Preord = category_theory.bundled_hom.forget₂ order_hom partial_order.to_preorder

source

@[simp]

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

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

source

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

α ≅ β

Constructs an equivalence between partial orders from an order isomorphism between them.

Equations

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

source

@[simp]

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

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

source

def PartOrd.dual :

PartOrd ⥤ PartOrd

order_dual as a functor.

Equations

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

source

@[simp]

theorem PartOrd.dual_obj (X : PartOrd) :

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

source

@[simp]

theorem PartOrd.dual_map (X Y : PartOrd) (ᾰ : ↥X →o ↥Y) :

PartOrd.dual.map ᾰ = ⇑order_hom.dual ᾰ

source

@[simp]

theorem PartOrd.dual_equiv_inverse :

PartOrd.dual_equiv.inverse = PartOrd.dual

source

@[simp]

theorem PartOrd.dual_equiv_functor :

PartOrd.dual_equiv.functor = PartOrd.dual

source

def PartOrd.dual_equiv :

PartOrd ≌ PartOrd

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

Equations

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

source

theorem PartOrd_dual_comp_forget_to_Preord :

PartOrd.dual ⋙ category_theory.forget₂ PartOrd Preord = category_theory.forget₂ PartOrd Preord ⋙ Preord.dual

source

def Preord_to_PartOrd :

Preord ⥤ PartOrd

antisymmetrization as a functor. It is the free functor.

Equations

Preord_to_PartOrd = {obj := λ (X : Preord), PartOrd.of (antisymmetrization ↥X has_le.le), map := λ (X Y : Preord) (f : X ⟶ Y), order_hom.antisymmetrization f, map_id' := Preord_to_PartOrd._proof_2, map_comp' := Preord_to_PartOrd._proof_3}

source

def Preord_to_PartOrd_forget_adjunction :

Preord_to_PartOrd ⊣ category_theory.forget₂ PartOrd Preord

Preord_to_PartOrd is left adjoint to the forgetful functor, meaning it is the free functor from Preord to PartOrd.

Equations

Preord_to_PartOrd_forget_adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Preord) (Y : PartOrd), {to_fun := λ (f : Preord_to_PartOrd.obj X ⟶ Y), {to_fun := ⇑f ∘ to_antisymmetrization has_le.le, monotone' := _}, inv_fun := λ (f : X ⟶ (category_theory.forget₂ PartOrd Preord).obj Y), {to_fun := λ (a : ↥(Preord_to_PartOrd.obj X)), quotient.lift_on' a ⇑f _, monotone' := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := Preord_to_PartOrd_forget_adjunction._proof_6, hom_equiv_naturality_right' := Preord_to_PartOrd_forget_adjunction._proof_7}

source

@[simp]

theorem Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd_hom_app_coe (X : Preord) (a : ↥((Preord_to_PartOrd ⋙ PartOrd.dual).obj X)) :

⇑(Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd.hom.app X) a = ⇑(order_iso.dual_antisymmetrization ↥X) a

source

def Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd :

Preord_to_PartOrd ⋙ PartOrd.dual ≅ Preord.dual ⋙ Preord_to_PartOrd

Preord_to_PartOrd and order_dual commute.

Equations

Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd = category_theory.nat_iso.of_components (λ (X : Preord), PartOrd.iso.mk (order_iso.dual_antisymmetrization ↥X)) Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd._proof_1

source

@[simp]

theorem Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd_inv_app_coe (X : Preord) (a : ↥((Preord.dual ⋙ Preord_to_PartOrd).obj X)) :

⇑(Preord_to_PartOrd_comp_to_dual_iso_to_dual_comp_Preord_to_PartOrd.inv.app X) a = ⇑((order_iso.dual_antisymmetrization ↥X).symm) a

mathlib3 documentation

Category of partial orders #