order.category.Preord - mathlib3 docs

source

def Preord :

Type (u_1+1)

The category of preorders.

Equations

Preord = category_theory.bundled preorder

Instances for Preord

source

@[protected, instance]

def Preord.order_hom.category_theory.bundled_hom :

category_theory.bundled_hom order_hom

Equations

Preord.order_hom.category_theory.bundled_hom = {to_fun := order_hom.to_fun, id := order_hom.id, comp := order_hom.comp, hom_ext := order_hom.ext, id_to_fun := Preord.order_hom.category_theory.bundled_hom._proof_1, comp_to_fun := Preord.order_hom.category_theory.bundled_hom._proof_2}

source

@[protected, instance]

def Preord.large_category :

category_theory.large_category Preord

source

@[protected, instance]

def Preord.concrete_category :

category_theory.concrete_category Preord

source

@[protected, instance]

def Preord.has_coe_to_sort :

has_coe_to_sort Preord (Type u_1)

Equations

Preord.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

def Preord.of (α : Type u_1) [preorder α] :

Preord

Construct a bundled Preord from the underlying type and typeclass.

Equations

Preord.of α = category_theory.bundled.of α

source

@[simp]

theorem Preord.coe_of (α : Type u_1) [preorder α] :

↥(Preord.of α) = α

source

@[protected, instance]

def Preord.inhabited :

inhabited Preord

Equations

Preord.inhabited = {default := Preord.of punit (partial_order.to_preorder punit)}

source

@[protected, instance]

def Preord.preorder (α : Preord) :

preorder ↥α

Equations

α.preorder = α.str

source

@[simp]

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

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

source

@[simp]

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

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

source

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

α ≅ β

Constructs an equivalence between preorders from an order isomorphism between them.

Equations

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

source

@[simp]

theorem Preord.dual_obj (X : Preord) :

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

source

def Preord.dual :

Preord ⥤ Preord

order_dual as a functor.

Equations

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

source

@[simp]

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

Preord.dual.map ᾰ = ⇑order_hom.dual ᾰ

source

@[simp]

theorem Preord.dual_equiv_functor :

Preord.dual_equiv.functor = Preord.dual

source

@[simp]

theorem Preord.dual_equiv_inverse :

Preord.dual_equiv.inverse = Preord.dual

source

def Preord.dual_equiv :

Preord ≌ Preord

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

Equations

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

source

def Preord_to_Cat :

Preord ⥤ category_theory.Cat

The embedding of Preord into Cat.

Equations

Preord_to_Cat = {obj := λ (X : Preord), category_theory.Cat.of X.α, map := λ (X Y : Preord) (f : X ⟶ Y), _.functor, map_id' := Preord_to_Cat._proof_2, map_comp' := Preord_to_Cat._proof_3}

Instances for Preord_to_Cat

source

@[simp]

theorem Preord_to_Cat_map (X Y : Preord) (f : X ⟶ Y) :

Preord_to_Cat.map f = _.functor

source

@[simp]

theorem Preord_to_Cat_obj (X : Preord) :

Preord_to_Cat.obj X = category_theory.Cat.of X.α

source

@[protected, instance]

def Preord_to_Cat.category_theory.faithful :

category_theory.faithful Preord_to_Cat

source

@[protected, instance]

def Preord_to_Cat.category_theory.full :

category_theory.full Preord_to_Cat

Equations

Preord_to_Cat.category_theory.full = {preimage := λ (X Y : Preord) (f : Preord_to_Cat.obj X ⟶ Preord_to_Cat.obj Y), {to_fun := f.obj, monotone' := _}, witness' := Preord_to_Cat.category_theory.full._proof_2}

mathlib3 documentation

Category of preorders #