Documentation

Mathlib.Order.Category.Preord

Category of preorders #

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

source
structure Preord :
Type (u_1 + 1)

The category of preorders.

  • carrier : Type u_1

    The underlying preordered type.

  • str : Preorder ↑self
Instances For
source
instance Preord.instCoeSortType :
CoeSort Preord (Type u)
Equations
source
@[reducible, inline]
abbrev Preord.of (X : Type u) [Preorder X] :
Preord

Construct a bundled Preord from the underlying type and typeclass.

Equations
source
structure Preord.Hom (X Y : Preord) :
Type u

The type of morphisms in Preord R.

source
theorem Preord.Hom.ext {X Y : Preord} {x y : X.Hom Y} (hom' : x.hom' = y.hom') :
x = y
source
instance Preord.instCategory :
CategoryTheory.Category.{u, u + 1} Preord
Equations
source
instance Preord.instConcreteCategoryOrderHomCarrier :
CategoryTheory.ConcreteCategory Preord fun (x1 x2 : Preord) => ↑x1 →o ↑x2
Equations
  • One or more equations did not get rendered due to their size.
source
@[reducible, inline]
abbrev Preord.Hom.hom {X Y : Preord} (f : X.Hom Y) :
↑X →o ↑Y

Turn a morphism in Preord back into a OrderHom.

Equations
source
@[reducible, inline]
abbrev Preord.ofHom {X Y : Type u} [Preorder X] [Preorder Y] (f : X →o Y) :
of X ⟶ of Y

Typecheck a OrderHom as a morphism in Preord.

Equations
source
def Preord.Hom.Simps.hom (X Y : Preord) (f : X.Hom Y) :
↑X →o ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

source
@[simp]
theorem Preord.coe_id {X : Preord} :
⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
source
@[simp]
theorem Preord.coe_comp {X Y Z : Preord} {f : X ⟶ Y} {g : Y ⟶ Z} :
⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
source
@[simp]
theorem Preord.forget_map {X Y : Preord} (f : X ⟶ Y) :
(CategoryTheory.forget Preord).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)
source
theorem Preord.ext {X Y : Preord} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) :
f = g
source
theorem Preord.coe_of (X : Type u) [Preorder X] :
↑(of X) = X
source
@[simp]
theorem Preord.hom_id {X : Preord} :
Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id
source
theorem Preord.id_apply (X : Preord) (x : ↑X) :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
source
@[simp]
theorem Preord.hom_comp {X Y Z : Preord} (f : X ⟶ Y) (g : Y ⟶ Z) :
Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)
source
theorem Preord.comp_apply {X Y Z : Preord} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) :
(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
source
theorem Preord.hom_ext {X Y : Preord} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) :
f = g
source
@[simp]
theorem Preord.hom_ofHom {X Y : Type u} [Preorder X] [Preorder Y] (f : X →o Y) :
Hom.hom (ofHom f) = f
source
@[simp]
theorem Preord.ofHom_hom {X Y : Preord} (f : X ⟶ Y) :
ofHom (Hom.hom f) = f
source
@[simp]
theorem Preord.ofHom_id {X : Type u} [Preorder X] :
ofHom OrderHom.id = CategoryTheory.CategoryStruct.id (of X)
source
@[simp]
theorem Preord.ofHom_comp {X Y Z : Type u} [Preorder X] [Preorder Y] [Preorder Z] (f : X →o Y) (g : Y →o Z) :
ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)
source
theorem Preord.ofHom_apply {X Y : Type u} [Preorder X] [Preorder Y] (f : X →o Y) (x : X) :
(CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x
source
theorem Preord.inv_hom_apply {X Y : Preord} (e : X ≅ Y) (x : ↑X) :
(CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
source
theorem Preord.hom_inv_apply {X Y : Preord} (e : X ≅ Y) (s : ↑Y) :
(CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
source
instance Preord.instInhabited :
Inhabited Preord
Equations
source
def Preord.Iso.mk {α β : Preord} (e : ↑α ≃o ↑β) :
α ≅ β

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

Equations
source
@[simp]
theorem Preord.Iso.mk_inv {α β : Preord} (e : ↑α ≃o ↑β) :
(mk e).inv = ofHom ↑e.symm
source
@[simp]
theorem Preord.Iso.mk_hom {α β : Preord} (e : ↑α ≃o ↑β) :
(mk e).hom = ofHom ↑e
source
def Preord.dual :
CategoryTheory.Functor Preord Preord

OrderDual as a functor.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Preord.dual_map {X✝ Y✝ : Preord} (f : X✝ ⟶ Y✝) :
dual.map f = ofHom (OrderHom.dual (Hom.hom f))
source
def Preord.dualEquiv :
Preord ≌ Preord

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Preord.dualEquiv_inverse :
dualEquiv.inverse = dual
source
@[simp]
theorem Preord.dualEquiv_functor :
dualEquiv.functor = dual
source
def preordToCat :
CategoryTheory.Functor Preord CategoryTheory.Cat

The embedding of Preord into Cat.

Equations
Instances For
source
@[simp]
theorem preordToCat_map {X✝ Y✝ : Preord} (f : X✝ ⟶ Y✝) :
preordToCat.map f = ⋯.functor
source
@[simp]
theorem preordToCat_obj (X : Preord) :
preordToCat.obj X = CategoryTheory.Cat.of ↑X
source
instance instFaithfulPreordCatPreordToCat :
preordToCat.Faithful
source
instance instFullPreordCatPreordToCat :
preordToCat.Full