Category of preorders #

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

source

structure Preord :

Type (u_1 + 1)

The category of preorders.

of :: (

carrier : Type u_1
The underlying preordered type.
str : Preorder ↑self

)

Instances For

source

@[implicit_reducible]

instance Preord.instCoeSortType :

CoeSort Preord (Type u)

Equations

Preord.instCoeSortType = { coe := Preord.carrier }

source

structure Preord.Hom (X Y : Preord) :

Type u

The type of morphisms in Preord R.

hom' : ↑X →o ↑Y
The underlying OrderHom.

Instances For

source

theorem Preord.Hom.ext {X Y : Preord} {x y : X.Hom Y} (hom' : x.hom' = y.hom') :

x = y

source

theorem Preord.Hom.ext_iff {X Y : Preord} {x y : X.Hom Y} :

x = y ↔ x.hom' = y.hom'

source

@[implicit_reducible]

instance Preord.instCategory :

CategoryTheory.Category.{u, u + 1} Preord

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

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

f.hom = CategoryTheory.ConcreteCategory.hom f

Instances For

source

@[reducible, inline]

abbrev Preord.ofHom {X Y : Type u} [Preorder X] [Preorder Y] (f : X →o Y) :

{ carrier := X, str := inst✝ } ⟶ { carrier := Y, str := inst✝¹ }

Typecheck a OrderHom as a morphism in Preord.

Equations

Preord.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

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

Preord.Hom.Simps.hom X Y f = f.hom

Instances For

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

@[deprecated CategoryTheory.ConcreteCategory.forget_map_eq_ofHom (since := "2026-02-15")]

theorem Preord.forget_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) :

(CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)

Alias of CategoryTheory.ConcreteCategory.forget_map_eq_ofHom.

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.ext_iff {X Y : Preord} {f g : X ⟶ Y} :

f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

source

theorem Preord.coe_of (X : Type u) [Preorder X] :

↑{ carrier := X, str := inst✝ } = 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

theorem Preord.hom_ext_iff {X Y : Preord} {f g : X ⟶ Y} :

f = g ↔ Hom.hom f = Hom.hom 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 { carrier := X, str := inst✝ }

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

@[implicit_reducible]

instance Preord.instInhabited :

Inhabited Preord

Equations

Preord.instInhabited = { default := { carrier := PUnit.{?u.3 + 1}, str := PUnit.instCompleteBooleanAlgebra.toCompleteSemilatticeInf.toPreorder } }

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 := Preord.ofHom ↑e, inv := Preord.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

theorem Preord.Iso.mk_hom {α β : Preord} (e : ↑α ≃o ↑β) :

(mk e).hom = ofHom ↑e

source

@[simp]

theorem Preord.Iso.mk_inv {α β : Preord} (e : ↑α ≃o ↑β) :

(mk e).inv = ofHom ↑e.symm

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.

Instances For

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.

Instances For

source

@[simp]

theorem Preord.dualEquiv_functor :

dualEquiv.functor = dual

source

@[simp]

theorem Preord.dualEquiv_inverse :

dualEquiv.inverse = dual

source

def preordToCat :

CategoryTheory.Functor Preord CategoryTheory.Cat

The embedding of Preord into Cat.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem preordToCat_obj (X : Preord) :

preordToCat.obj X = CategoryTheory.Cat.of ↑X

source

@[simp]

theorem preordToCat_map {X✝ Y✝ : Preord} (f : X✝ ⟶ Y✝) :

preordToCat.map f = ⋯.functor.toCatHom

source

instance instFaithfulPreordCatPreordToCat :

preordToCat.Faithful

source

instance instFullPreordCatPreordToCat :

preordToCat.Full

Documentation

Mathlib.Order.Category.Preord

Category of preorders #