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.instBundledHomPreorderOrderHom : CategoryTheory.BundledHom OrderHom

Equations

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

instance Preord.instConcreteCategory : CategoryTheory.ConcreteCategory Preord

Equations

• Preord.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory OrderHom

instance Preord.instCoeSortType : CoeSort Preord (Type u_1)

Equations

• Preord.instCoeSortType = 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.instInhabited : Inhabited Preord

Equations

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

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

Equations

• α.instPreorderα = α.str

@[simp]

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

@[simp]

theorem Preord.Iso.mk_hom {α : Preord} {β : Preord} (e : ↑α ≃o ↑β) : (Preord.Iso.mk e).hom = ↑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 = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

def Preord.dual : CategoryTheory.Functor Preord Preord

OrderDual as a functor.

Equations

• Preord.dual = { obj := fun (X : Preord) => Preord.of (↑X)ᵒᵈ, map := fun {X Y : Preord} => ⇑OrderHom.dual, map_id := Preord.dual.proof_1, map_comp := @Preord.dual.proof_2 }

@[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_map : ∀ {X Y : Preord} (f : X ⟶ Y), preordToCat.map f = ⋯.functor

@[simp]

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

def preordToCat : CategoryTheory.Functor Preord CategoryTheory.Cat

The embedding of Preord into Cat.

Equations

• preordToCat = { obj := fun (X : Preord) => CategoryTheory.Cat.of ↑X, map := fun {X Y : Preord} (f : X ⟶ Y) => ⋯.functor, map_id := preordToCat.proof_2, map_comp := @preordToCat.proof_3 }

instance instFaithfulPreordCatPreordToCat : preordToCat.Faithful

Equations

• instFaithfulPreordCatPreordToCat = ⋯

instance instFullPreordCatPreordToCat : preordToCat.Full

Equations

• instFullPreordCatPreordToCat = ⋯