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.instParentProjectionPartialOrderLinearOrderToPartialOrder : CategoryTheory.BundledHom.ParentProjection @LinearOrder.toPartialOrder

Equations

• LinOrd.instParentProjectionPartialOrderLinearOrderToPartialOrder = ⋯

instance instLinOrdLargeCategory : CategoryTheory.LargeCategory LinOrd

Equations

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

instance LinOrd.instConcreteCategory : CategoryTheory.ConcreteCategory LinOrd

Equations

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

instance LinOrd.instCoeSortType : CoeSort LinOrd (Type u_1)

Equations

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

Equations

• LinOrd.instInhabited = { default := LinOrd.of PUnit.{?u.3 + 1} }

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

Equations

• α.instLinearOrderα = α.str

instance LinOrd.hasForgetToLat : CategoryTheory.HasForget₂ LinOrd Lat

Equations

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

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

@[simp]

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

@[simp]

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

def LinOrd.dual : CategoryTheory.Functor LinOrd LinOrd

OrderDual as a functor.

Equations

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

@[simp]

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

@[simp]

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

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.

@[simp]

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

@[simp]

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

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