Category of partial orders #

This defines PartOrd, the category of partial orders with monotone maps.

source

structure PartOrd :

Type (u_1 + 1)

The category of partial orders.

carrier : Type u_1
The underlying partially ordered type.
str : PartialOrder ↑self

Instances For

source

instance PartOrd.instCoeSortType :

CoeSort PartOrd (Type u_1)

Equations

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

source

@[reducible, inline]

abbrev PartOrd.of (X : Type u_1) [PartialOrder X] :

PartOrd

Construct a bundled PartOrd from the underlying type and typeclass.

Equations

PartOrd.of X = PartOrd.mk X

Instances For

source

structure PartOrd.Hom (X Y : PartOrd) :

Type u

The type of morphisms in PartOrd R.

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

Instances For

source

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

x = y

source

instance PartOrd.instCategory :

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

Equations

PartOrd.instCategory = CategoryTheory.Category.mk @PartOrd.instCategory.proof_1 @PartOrd.instCategory.proof_2 @PartOrd.instCategory.proof_3

source

instance PartOrd.instConcreteCategoryOrderHomCarrier :

CategoryTheory.ConcreteCategory PartOrd fun (x1 x2 : PartOrd) => ↑x1 →o ↑x2

Equations

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

source

@[reducible, inline]

abbrev PartOrd.Hom.hom {X Y : PartOrd} (f : X.Hom Y) :

↑X →o ↑Y

Turn a morphism in PartOrd back into a OrderHom.

Equations

f.hom = CategoryTheory.ConcreteCategory.hom f

Instances For

source

@[reducible, inline]

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

of X ⟶ of Y

Typecheck a OrderHom as a morphism in PartOrd.

Equations

PartOrd.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

def PartOrd.Hom.Simps.hom (X Y : PartOrd) (f : X.Hom Y) :

↑X →o ↑Y

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

Equations

PartOrd.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 PartOrd.coe_id {X : PartOrd} :

⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

source

@[simp]

theorem PartOrd.coe_comp {X Y Z : PartOrd} {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 PartOrd.forget_map {X Y : PartOrd} (f : X ⟶ Y) :

(CategoryTheory.forget PartOrd).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

source

theorem PartOrd.ext {X Y : PartOrd} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) :

f = g

source

theorem PartOrd.coe_of (X : Type u) [PartialOrder X] :

↑(of X) = X

source

@[simp]

theorem PartOrd.hom_id {X : PartOrd} :

Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id

source

theorem PartOrd.id_apply (X : PartOrd) (x : ↑X) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

source

@[simp]

theorem PartOrd.hom_comp {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) :

Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

source

theorem PartOrd.comp_apply {X Y Z : PartOrd} (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 PartOrd.hom_ext {X Y : PartOrd} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) :

f = g

source

@[simp]

theorem PartOrd.hom_ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) :

Hom.hom (ofHom f) = f

source

@[simp]

theorem PartOrd.ofHom_hom {X Y : PartOrd} (f : X ⟶ Y) :

ofHom (Hom.hom f) = f

source

@[simp]

theorem PartOrd.ofHom_id {X : Type u} [PartialOrder X] :

ofHom OrderHom.id = CategoryTheory.CategoryStruct.id (of X)

source

@[simp]

theorem PartOrd.ofHom_comp {X Y Z : Type u} [PartialOrder X] [PartialOrder Y] [PartialOrder Z] (f : X →o Y) (g : Y →o Z) :

ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

source

theorem PartOrd.ofHom_apply {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) (x : X) :

(CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

source

theorem PartOrd.inv_hom_apply {X Y : PartOrd} (e : X ≅ Y) (x : ↑X) :

(CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

source

theorem PartOrd.hom_inv_apply {X Y : PartOrd} (e : X ≅ Y) (s : ↑Y) :

(CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

source

instance PartOrd.hasForgetToPreord :

CategoryTheory.HasForget₂ PartOrd Preord

Equations

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

source

def PartOrd.Iso.mk {α β : PartOrd} (e : ↑α ≃o ↑β) :

α ≅ β

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

Equations

PartOrd.Iso.mk e = { hom := PartOrd.ofHom ↑e, inv := PartOrd.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

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

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

source

@[simp]

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

(mk e).hom = ofHom ↑e

source

def PartOrd.dual :

CategoryTheory.Functor PartOrd PartOrd

OrderDual as a functor.

Equations

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

Instances For

source

@[simp]

theorem PartOrd.dual_map {X✝ Y✝ : PartOrd} (f : X✝ ⟶ Y✝) :

dual.map f = ofHom (OrderHom.dual (Hom.hom f))

source

def PartOrd.dualEquiv :

PartOrd ≌ PartOrd

The equivalence between PartOrd 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 PartOrd.dualEquiv_inverse :

dualEquiv.inverse = dual

source

@[simp]

theorem PartOrd.dualEquiv_functor :

dualEquiv.functor = dual

source

theorem partOrd_dual_comp_forget_to_preord :

PartOrd.dual.comp (CategoryTheory.forget₂ PartOrd Preord) = (CategoryTheory.forget₂ PartOrd Preord).comp Preord.dual

source

def preordToPartOrd :

CategoryTheory.Functor Preord PartOrd

Antisymmetrization as a functor. It is the free functor.

Equations

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

Instances For

source

def preordToPartOrdForgetAdjunction :

preordToPartOrd ⊣ CategoryTheory.forget₂ PartOrd Preord

preordToPartOrd is left adjoint to the forgetful functor, meaning it is the free functor from Preord to PartOrd.

Equations

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

Instances For

source

def preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd :

preordToPartOrd.comp PartOrd.dual ≅ Preord.dual.comp preordToPartOrd

PreordToPartOrd and OrderDual commute.

Equations

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

Instances For

source

@[simp]

theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe (X : Preord) (a : ↑((Preord.dual.comp preordToPartOrd).obj X)) :

(PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)) a = (OrderIso.dualAntisymmetrization ↑X).symm a

source

theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe (X : Preord) (a : ↑((preordToPartOrd.comp PartOrd.dual).obj X)) :

(PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X)) a = (OrderIso.dualAntisymmetrization ↑X) a

Documentation

Mathlib.Order.Category.PartOrd

Category of partial orders #