Category of preorders

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

def Preord : Type (u_1 + 1)

The category of preorders.

Equations

• Preord = CategoryTheory.Bundled Preorder

instance Preord.instBundledHomTypePreorderOrderHom : CategoryTheory.BundledHom OrderHom

Equations

• Preord.instBundledHomTypePreorderOrderHom = CategoryTheory.BundledHom.mk @OrderHom.toFun @OrderHom.id @OrderHom.comp

instance Preord.instConcreteCategoryPreordInstPreordLargeCategory : CategoryTheory.ConcreteCategory Preord

Equations

• Preord.instConcreteCategoryPreordInstPreordLargeCategory = CategoryTheory.BundledHom.concreteCategory OrderHom

instance Preord.instCoeSortPreordType : CoeSort Preord (Type u_1)

Equations

• Preord.instCoeSortPreordType = CategoryTheory.Bundled.coeSort

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

Construct a bundled Preord from the underlying type and typeclass.

Equations

• Preord.of α = CategoryTheory.Bundled.of α

@[simp]

theorem Preord.coe_of (α : Type u_1) [Preorder α] : ↑(Preord.of α) = α

instance Preord.instInhabitedPreord : Inhabited Preord

Equations

• Preord.instInhabitedPreord = { default := Preord.of PUnit.{u_1 + 1} }

instance Preord.instPreorderα (α : Preord) : Preorder ↑α

Equations

• Preord.instPreorderα α = α.str

@[simp]

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

@[simp]

theorem Preord.Iso.mk_inv {α : Preord} {β : Preord} (e : ↑α ≃o ↑β) : (Preord.Iso.mk e).inv = ↑(OrderIso.symm e)

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

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

Equations

• Preord.Iso.mk e = CategoryTheory.Iso.mk ↑e ↑(OrderIso.symm e)

@[simp]

theorem Preord.dual_map : ∀ {X Y : Preord} (a : ↑X →o ↑Y), Preord.dual.toPrefunctor.map a = OrderHom.dual a

@[simp]

theorem Preord.dual_obj (X : Preord) : Preord.dual.toPrefunctor.obj X = Preord.of (↑X)ᵒᵈ

def Preord.dual : CategoryTheory.Functor Preord Preord

OrderDual as a functor.

Equations

• Preord.dual = CategoryTheory.Functor.mk { obj := fun (X : Preord) => Preord.of (↑X)ᵒᵈ, map := fun {X Y : Preord} => ⇑OrderHom.dual }

@[simp]

theorem Preord.dualEquiv_inverse : Preord.dualEquiv.inverse = Preord.dual

@[simp]

theorem Preord.dualEquiv_functor : Preord.dualEquiv.functor = Preord.dual

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.

@[simp]

theorem preordToCat_obj (X : Preord) : preordToCat.toPrefunctor.obj X = CategoryTheory.Cat.of ↑X

@[simp]

theorem preordToCat_map : ∀ {X Y : Preord} (f : X ⟶ Y), preordToCat.toPrefunctor.map f = Monotone.functor (_ : Monotone ⇑f)

def preordToCat : CategoryTheory.Functor Preord CategoryTheory.Cat

The embedding of Preord into Cat.

Equations

• preordToCat = CategoryTheory.Functor.mk { obj := fun (X : Preord) => CategoryTheory.Cat.of ↑X, map := fun {X Y : Preord} (f : X ⟶ Y) => Monotone.functor (_ : Monotone ⇑f) }

instance instFaithfulPreordInstPreordLargeCategoryCatCategoryPreordToCat : CategoryTheory.Faithful preordToCat

Equations

• instFaithfulPreordInstPreordLargeCategoryCatCategoryPreordToCat = (_ : CategoryTheory.Faithful preordToCat)

instance instFullPreordInstPreordLargeCategoryCatCategoryPreordToCat : CategoryTheory.Full preordToCat

Equations

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