order.category.PartialOrder

source

def PartialOrder :

Type (u_1+1)

The category of partially ordered types.

Equations

PartialOrder = category_theory.bundled partial_order

Instances for PartialOrder

source

@[protected, instance]

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

category_theory.bundled_hom.parent_projection partial_order.to_preorder

Equations

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

source

@[protected, instance]

def PartialOrder.concrete_category :

category_theory.concrete_category PartialOrder

source

@[protected, instance]

def PartialOrder.large_category :

category_theory.large_category PartialOrder

source

@[protected, instance]

def PartialOrder.has_coe_to_sort :

has_coe_to_sort PartialOrder (Type u_1)

Equations

PartialOrder.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

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

PartialOrder

Construct a bundled PartialOrder from the underlying type and typeclass.

Equations

PartialOrder.of α = category_theory.bundled.of α

source

@[simp]

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

↥(PartialOrder.of α) = α

source

@[protected, instance]

def PartialOrder.inhabited :

inhabited PartialOrder

Equations

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

source

@[protected, instance]

def PartialOrder.partial_order (α : PartialOrder) :

partial_order ↥α

Equations

α.partial_order = α.str

source

@[protected, instance]

def PartialOrder.has_forget_to_Preorder :

category_theory.has_forget₂ PartialOrder Preorder

Equations

PartialOrder.has_forget_to_Preorder = category_theory.bundled_hom.forget₂ order_hom partial_order.to_preorder

source

@[simp]

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

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

source

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

α ≅ β

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

Equations

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

source

@[simp]

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

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

source

def PartialOrder.dual :

PartialOrder ⥤ PartialOrder

order_dual as a functor.

Equations

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

source

@[simp]

theorem PartialOrder.dual_obj (X : PartialOrder) :

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

source

@[simp]

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

PartialOrder.dual.map ᾰ = ⇑order_hom.dual ᾰ

source

@[simp]

theorem PartialOrder.dual_equiv_functor :

PartialOrder.dual_equiv.functor = PartialOrder.dual

source

def PartialOrder.dual_equiv :

PartialOrder ≌ PartialOrder

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

Equations

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

source

@[simp]

theorem PartialOrder.dual_equiv_inverse :

PartialOrder.dual_equiv.inverse = PartialOrder.dual

source

theorem PartialOrder_dual_comp_forget_to_Preorder :

PartialOrder.dual ⋙ category_theory.forget₂ PartialOrder Preorder = category_theory.forget₂ PartialOrder Preorder ⋙ Preorder.dual

source

def Preorder_to_PartialOrder :

Preorder ⥤ PartialOrder

antisymmetrization as a functor. It is the free functor.

Equations

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

source

def Preorder_to_PartialOrder_forget_adjunction :

Preorder_to_PartialOrder ⊣ category_theory.forget₂ PartialOrder Preorder

Preorder_to_PartialOrder is left adjoint to the forgetful functor, meaning it is the free functor from Preorder to PartialOrder.

Equations

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

source

def Preorder_to_PartialOrder_comp_to_dual_iso_to_dual_comp_Preorder_to_PartialOrder :

Preorder_to_PartialOrder ⋙ PartialOrder.dual ≅ Preorder.dual ⋙ Preorder_to_PartialOrder

Preorder_to_PartialOrder and order_dual commute.

Equations

Preorder_to_PartialOrder_comp_to_dual_iso_to_dual_comp_Preorder_to_PartialOrder = category_theory.nat_iso.of_components (λ (X : Preorder), PartialOrder.iso.mk (order_iso.dual_antisymmetrization ↥X)) Preorder_to_PartialOrder_comp_to_dual_iso_to_dual_comp_Preorder_to_PartialOrder._proof_1

source

@[simp]

theorem Preorder_to_PartialOrder_comp_to_dual_iso_to_dual_comp_Preorder_to_PartialOrder_hom_app_coe (X : Preorder) (a : ↥((Preorder_to_PartialOrder ⋙ PartialOrder.dual).obj X)) :

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

source

@[simp]

theorem Preorder_to_PartialOrder_comp_to_dual_iso_to_dual_comp_Preorder_to_PartialOrder_inv_app_coe (X : Preorder) (a : ↥((Preorder.dual ⋙ Preorder_to_PartialOrder).obj X)) :

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

mathlib documentation

Category of partial orders #