Nonempty finite linear orders

This defines NonemptyFinLinOrd, the category of nonempty finite linear orders with monotone maps. This is the index category for simplicial objects.

Note: NonemptyFinLinOrd is not a subcategory of FinBddDistLat because its morphisms do not preserve ⊥ and ⊤.

structure NonemptyFinLinOrdextends LinOrd : Type (u_1 + 1)

The category of nonempty finite linear orders.

• carrier : Type u_1
• str : LinearOrder ↑self.toLinOrd
• nonempty : Nonempty ↑self.toLinOrd
• fintype : Fintype ↑self.toLinOrd

instance NonemptyFinLinOrd.instCoeSortType : CoeSort NonemptyFinLinOrd (Type u_1)

Equations

• NonemptyFinLinOrd.instCoeSortType = { coe := fun (X : NonemptyFinLinOrd) => ↑X.toLinOrd }

instance NonemptyFinLinOrd.instLargeCategory : CategoryTheory.LargeCategory NonemptyFinLinOrd

Equations

• NonemptyFinLinOrd.instLargeCategory = inferInstanceAs (CategoryTheory.Category.{?u.3, ?u.3 + 1} (CategoryTheory.InducedCategory LinOrd NonemptyFinLinOrd.toLinOrd))

instance NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier : CategoryTheory.ConcreteCategory NonemptyFinLinOrd fun (x1 x2 : NonemptyFinLinOrd) => ↑x1.toLinOrd →o ↑x2.toLinOrd

Equations

• NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier = CategoryTheory.InducedCategory.concreteCategory NonemptyFinLinOrd.toLinOrd

instance NonemptyFinLinOrd.instBoundedOrderCarrier (X : NonemptyFinLinOrd) : BoundedOrder ↑X.toLinOrd

Equations

• X.instBoundedOrderCarrier = Fintype.toBoundedOrder ↑X.toLinOrd

@[reducible, inline]

abbrev NonemptyFinLinOrd.of (α : Type u_1) [Nonempty α] [Fintype α] [LinearOrder α] : NonemptyFinLinOrd

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations

• NonemptyFinLinOrd.of α = { carrier := α, str := inst✝, nonempty := inst✝², fintype := inst✝¹ }

theorem NonemptyFinLinOrd.coe_of (α : Type u_1) [Nonempty α] [Fintype α] [LinearOrder α] : ↑(of α).toLinOrd = α

@[reducible, inline]

abbrev NonemptyFinLinOrd.ofHom {X Y : Type u} [Nonempty X] [LinearOrder X] [Fintype X] [Nonempty Y] [LinearOrder Y] [Fintype Y] (f : X →o Y) : of X ⟶ of Y

Typecheck a OrderHom as a morphism in NonemptyFinLinOrd.

Equations

• NonemptyFinLinOrd.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[simp]

theorem NonemptyFinLinOrd.hom_hom_id {X : NonemptyFinLinOrd} : LinOrd.Hom.hom (CategoryTheory.CategoryStruct.id X).hom = OrderHom.id

@[deprecated NonemptyFinLinOrd.hom_hom_id (since := "2025-12-18")]

theorem NonemptyFinLinOrd.hom_id {X : NonemptyFinLinOrd} : LinOrd.Hom.hom (CategoryTheory.CategoryStruct.id X).hom = OrderHom.id

Alias of NonemptyFinLinOrd.hom_hom_id.

theorem NonemptyFinLinOrd.id_apply (X : NonemptyFinLinOrd) (x : ↑X.toLinOrd) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem NonemptyFinLinOrd.hom_hom_comp {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) : LinOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom = (LinOrd.Hom.hom g.hom).comp (LinOrd.Hom.hom f.hom)

@[deprecated NonemptyFinLinOrd.hom_hom_comp (since := "2025-12-18")]

theorem NonemptyFinLinOrd.hom_comp {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) : LinOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom = (LinOrd.Hom.hom g.hom).comp (LinOrd.Hom.hom f.hom)

Alias of NonemptyFinLinOrd.hom_hom_comp.

theorem NonemptyFinLinOrd.comp_apply {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toLinOrd) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem NonemptyFinLinOrd.hom_ext {X Y : NonemptyFinLinOrd} {f g : X ⟶ Y} (hf : LinOrd.Hom.hom f.hom = LinOrd.Hom.hom g.hom) : f = g

theorem NonemptyFinLinOrd.hom_ext_iff {X Y : NonemptyFinLinOrd} {f g : X ⟶ Y} : f = g ↔ LinOrd.Hom.hom f.hom = LinOrd.Hom.hom g.hom

@[simp]

theorem NonemptyFinLinOrd.hom_hom_ofHom {X Y : Type u} [Nonempty X] [LinearOrder X] [Fintype X] [Nonempty Y] [LinearOrder Y] [Fintype Y] (f : X →o Y) : LinOrd.Hom.hom (ofHom f).hom = f

@[deprecated NonemptyFinLinOrd.hom_hom_ofHom (since := "2025-12-18")]

theorem NonemptyFinLinOrd.hom_ofHom {X Y : Type u} [Nonempty X] [LinearOrder X] [Fintype X] [Nonempty Y] [LinearOrder Y] [Fintype Y] (f : X →o Y) : LinOrd.Hom.hom (ofHom f).hom = f

Alias of NonemptyFinLinOrd.hom_hom_ofHom.

@[simp]

theorem NonemptyFinLinOrd.ofHom_hom {X Y : NonemptyFinLinOrd} (f : X ⟶ Y) : ofHom (LinOrd.Hom.hom f.hom) = f

instance NonemptyFinLinOrd.instInhabited : Inhabited NonemptyFinLinOrd

Equations

• NonemptyFinLinOrd.instInhabited = { default := NonemptyFinLinOrd.of PUnit.{?u.2 + 1} }

instance NonemptyFinLinOrd.hasForgetToLinOrd : CategoryTheory.HasForget₂ NonemptyFinLinOrd LinOrd

Equations

• NonemptyFinLinOrd.hasForgetToLinOrd = CategoryTheory.InducedCategory.hasForget₂ NonemptyFinLinOrd.toLinOrd

instance NonemptyFinLinOrd.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ NonemptyFinLinOrd FinPartOrd

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def NonemptyFinLinOrd.dual : CategoryTheory.Functor NonemptyFinLinOrd NonemptyFinLinOrd

OrderDual as a functor.

Equations

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

@[simp]

theorem NonemptyFinLinOrd.dual_map {X✝ Y✝ : NonemptyFinLinOrd} (f : X✝ ⟶ Y✝) : dual.map f = ofHom (OrderHom.dual (LinOrd.Hom.hom f.hom))

def NonemptyFinLinOrd.dualEquiv : NonemptyFinLinOrd ≌ NonemptyFinLinOrd

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

Equations

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

@[simp]

theorem NonemptyFinLinOrd.dualEquiv_inverse : dualEquiv.inverse = dual

@[simp]

theorem NonemptyFinLinOrd.dualEquiv_functor : dualEquiv.functor = dual

theorem NonemptyFinLinOrd.mono_iff_injective {A B : NonemptyFinLinOrd} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem NonemptyFinLinOrd.epi_iff_surjective {A B : NonemptyFinLinOrd} (f : A ⟶ B) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

instance NonemptyFinLinOrd.instSplitEpiCategory : CategoryTheory.SplitEpiCategory NonemptyFinLinOrd

instance NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations : CategoryTheory.Limits.HasStrongEpiMonoFactorisations NonemptyFinLinOrd

theorem nonemptyFinLinOrd_dual_comp_forget_to_linOrd : NonemptyFinLinOrd.dual.comp (CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd) = (CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd).comp LinOrd.dual

def nonemptyFinLinOrdDualCompForgetToFinPartOrd : NonemptyFinLinOrd.dual.comp (CategoryTheory.forget₂ NonemptyFinLinOrd FinPartOrd) ≅ (CategoryTheory.forget₂ NonemptyFinLinOrd FinPartOrd).comp FinPartOrd.dual

The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd and OrderDual commute.

Equations

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

def Fin.hom_succ {n : ℕ} (i : Fin n) : i.castSucc ⟶ i.succ

The generating arrow i ⟶ i+1 in the category Fin n

Equations

• i.hom_succ = CategoryTheory.homOfLE ⋯