mathlib documentation

order.category.Preorder

Category of preorders #

This defines Preorder, the category of preorders with monotone maps.

source
def Preorder  :
Type (u_1+1)

The category of preorders.

Equations
Instances for Preorder
source
@[protected, instance]
def Preorder.order_hom.category_theory.bundled_hom  :
category_theory.bundled_hom order_hom
Equations
source
@[protected, instance]
def Preorder.large_category  :
category_theory.large_category Preorder
source
@[protected, instance]
def Preorder.concrete_category  :
category_theory.concrete_category Preorder
source
@[protected, instance]
def Preorder.has_coe_to_sort  :
has_coe_to_sort Preorder (Type u_1)
Equations
source
def Preorder.of (α : Type u_1) [preorder α] :
Preorder

Construct a bundled Preorder from the underlying type and typeclass.

Equations
source
@[simp]
theorem Preorder.coe_of (α : Type u_1) [preorder α] :
↥(Preorder.of α) = α
source
@[protected, instance]
def Preorder.inhabited  :
inhabited Preorder
Equations
source
@[protected, instance]
def Preorder.preorder (α : Preorder) :
preorder ↥α
Equations
source
def Preorder.iso.mk {α β : Preorder} (e : ↥α ≃o ↥β) :
α ≅ β

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

Equations
source
@[simp]
theorem Preorder.iso.mk_inv {α β : Preorder} (e : ↥α ≃o ↥β) :
(Preorder.iso.mk e).inv = ↑(e.symm)
source
@[simp]
theorem Preorder.iso.mk_hom {α β : Preorder} (e : ↥α ≃o ↥β) :
(Preorder.iso.mk e).hom = ↑e
source
def Preorder.dual  :
Preorder ⥤ Preorder

order_dual as a functor.

Equations
source
@[simp]
theorem Preorder.dual_map (X Y : Preorder) (ᾰ : ↥X →o ↥Y) :
Preorder.dual.map ᾰ = ⇑order_hom.dual ᾰ
source
@[simp]
theorem Preorder.dual_obj (X : Preorder) :
Preorder.dual.obj X = Preorder.of (↥X)ᵒᵈ
source
@[simp]
theorem Preorder.dual_equiv_functor  :
Preorder.dual_equiv.functor = Preorder.dual
source
def Preorder.dual_equiv  :
Preorder ≌ Preorder

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

Equations
source
@[simp]
theorem Preorder.dual_equiv_inverse  :
Preorder.dual_equiv.inverse = Preorder.dual
source
@[simp]
theorem Preorder_to_Cat_obj (X : Preorder) :
Preorder_to_Cat.obj X = category_theory.Cat.of X.α
source
def Preorder_to_Cat  :
Preorder ⥤ category_theory.Cat

The embedding of Preorder into Cat.

Equations
Instances for Preorder_to_Cat
source
@[simp]
theorem Preorder_to_Cat_map (X Y : Preorder) (f : X ⟶ Y) :
Preorder_to_Cat.map f = _.functor
source
@[protected, instance]
def Preorder_to_Cat.category_theory.faithful  :
category_theory.faithful Preorder_to_Cat
source
@[protected, instance]
def Preorder_to_Cat.category_theory.full  :
category_theory.full Preorder_to_Cat
Equations