Category of linear orders

This defines LinOrd, the category of linear orders with monotone maps.

def LinOrd : Type (u_1 + 1)

The category of linear orders.

Equations

• LinOrd = CategoryTheory.Bundled LinearOrder

instance LinOrd.instParentProjectionTypePartialOrderLinearOrderToPartialOrder : CategoryTheory.BundledHom.ParentProjection @LinearOrder.toPartialOrder

Equations

• LinOrd.instParentProjectionTypePartialOrderLinearOrderToPartialOrder = (_ : CategoryTheory.BundledHom.ParentProjection @LinearOrder.toPartialOrder)

instance LinOrd.instConcreteCategoryLinOrdInstLinOrdLargeCategory : CategoryTheory.ConcreteCategory LinOrd

Equations

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

instance LinOrd.instCoeSortLinOrdType : CoeSort LinOrd (Type u_1)

Equations

• LinOrd.instCoeSortLinOrdType = CategoryTheory.Bundled.coeSort

def LinOrd.of (α : Type u_1) [LinearOrder α] : LinOrd

Construct a bundled LinOrd from the underlying type and typeclass.

Equations

• LinOrd.of α = CategoryTheory.Bundled.of α

@[simp]

theorem LinOrd.coe_of (α : Type u_1) [LinearOrder α] : ↑(LinOrd.of α) = α

instance LinOrd.instInhabitedLinOrd : Inhabited LinOrd

Equations

• LinOrd.instInhabitedLinOrd = { default := LinOrd.of PUnit.{u_1 + 1} }

instance LinOrd.instLinearOrderα (α : LinOrd) : LinearOrder ↑α

Equations

• LinOrd.instLinearOrderα α = α.str

instance LinOrd.hasForgetToLat : CategoryTheory.HasForget₂ LinOrd Lat

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def LinOrd.dual : CategoryTheory.Functor LinOrd LinOrd

OrderDual as a functor.

Equations

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

@[simp]

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

@[simp]

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

def LinOrd.dualEquiv : LinOrd ≌ LinOrd

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

Equations

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

theorem linOrd_dual_comp_forget_to_Lat : CategoryTheory.Functor.comp LinOrd.dual (CategoryTheory.forget₂ LinOrd Lat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ LinOrd Lat) Lat.dual