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.carrier
• nonempty : Nonempty self.carrier
• fintype : Fintype self.carrier

def NonemptyFinLinOrd.instCoeSortType : CoeSort NonemptyFinLinOrd (Type u_1)

Equations

• Eq NonemptyFinLinOrd.instCoeSortType { coe := fun (X : NonemptyFinLinOrd) => X.carrier }

def NonemptyFinLinOrd.instLargeCategory : CategoryTheory.LargeCategory NonemptyFinLinOrd

Equations

• Eq NonemptyFinLinOrd.instLargeCategory (CategoryTheory.InducedCategory.category NonemptyFinLinOrd.toLinOrd)

def NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier : CategoryTheory.ConcreteCategory NonemptyFinLinOrd fun (x1 x2 : NonemptyFinLinOrd) => OrderHom x1.carrier x2.carrier

Equations

• Eq NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier (CategoryTheory.InducedCategory.concreteCategory NonemptyFinLinOrd.toLinOrd)

def NonemptyFinLinOrd.instBoundedOrderCarrier (X : NonemptyFinLinOrd) : BoundedOrder X.carrier

Equations

• Eq X.instBoundedOrderCarrier (Fintype.toBoundedOrder X.carrier)

@[reducible, inline]

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

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations

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

theorem NonemptyFinLinOrd.coe_of (α : Type u_1) [Nonempty α] [Fintype α] [LinearOrder α] : Eq (of α).carrier α

@[reducible, inline]

abbrev NonemptyFinLinOrd.ofHom {X Y : Type u} [Nonempty X] [LinearOrder X] [Fintype X] [Nonempty Y] [LinearOrder Y] [Fintype Y] (f : OrderHom X Y) : Quiver.Hom (of X) (of Y)

Typecheck a OrderHom as a morphism in NonemptyFinLinOrd.

Equations

• Eq (NonemptyFinLinOrd.ofHom f) (CategoryTheory.ConcreteCategory.ofHom f)

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

theorem NonemptyFinLinOrd.id_apply (X : NonemptyFinLinOrd) (x : X.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x) x

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

theorem NonemptyFinLinOrd.comp_apply {X Y Z : NonemptyFinLinOrd} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) (x : X.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom g) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f) x))

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

theorem NonemptyFinLinOrd.hom_ext_iff {X Y : NonemptyFinLinOrd} {f g : Quiver.Hom X Y} : Iff (Eq f g) (Eq (LinOrd.Hom.hom f) (LinOrd.Hom.hom g))

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

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

def NonemptyFinLinOrd.instInhabited : Inhabited NonemptyFinLinOrd

Equations

• Eq NonemptyFinLinOrd.instInhabited { default := NonemptyFinLinOrd.of PUnit }

def NonemptyFinLinOrd.hasForgetToLinOrd : CategoryTheory.HasForget₂ NonemptyFinLinOrd LinOrd

Equations

• Eq NonemptyFinLinOrd.hasForgetToLinOrd (CategoryTheory.InducedCategory.hasForget₂ NonemptyFinLinOrd.toLinOrd)

def 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 : OrderIso α.carrier β.carrier) : CategoryTheory.Iso α β

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

Equations

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

theorem NonemptyFinLinOrd.Iso.mk_hom {α β : NonemptyFinLinOrd} (e : OrderIso α.carrier β.carrier) : Eq (mk e).hom (ofHom (OrderHomClass.toOrderHom e))

theorem NonemptyFinLinOrd.Iso.mk_inv {α β : NonemptyFinLinOrd} (e : OrderIso α.carrier β.carrier) : Eq (mk e).inv (ofHom (OrderHomClass.toOrderHom 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.

theorem NonemptyFinLinOrd.dual_map {X✝ Y✝ : NonemptyFinLinOrd} (f : Quiver.Hom X✝ Y✝) : Eq (dual.map f) (ofHom (DFunLike.coe OrderHom.dual (LinOrd.Hom.hom f)))

def NonemptyFinLinOrd.dualEquiv : CategoryTheory.Equivalence 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.

theorem NonemptyFinLinOrd.dualEquiv_functor : Eq dualEquiv.functor dual

theorem NonemptyFinLinOrd.dualEquiv_inverse : Eq dualEquiv.inverse dual

theorem NonemptyFinLinOrd.mono_iff_injective {A B : NonemptyFinLinOrd} (f : Quiver.Hom A B) : Iff (CategoryTheory.Mono f) (Function.Injective (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f)))

theorem NonemptyFinLinOrd.epi_iff_surjective {A B : NonemptyFinLinOrd} (f : Quiver.Hom A B) : Iff (CategoryTheory.Epi f) (Function.Surjective (DFunLike.coe (CategoryTheory.ConcreteCategory.hom f)))

theorem NonemptyFinLinOrd.instSplitEpiCategory : CategoryTheory.SplitEpiCategory NonemptyFinLinOrd

theorem NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations : CategoryTheory.Limits.HasStrongEpiMonoFactorisations NonemptyFinLinOrd

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

def nonemptyFinLinOrdDualCompForgetToFinPartOrd : CategoryTheory.Iso (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 : Nat} (i : Fin n) : Quiver.Hom i.castSucc i.succ

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

Equations

• Eq i.hom_succ (CategoryTheory.homOfLE ⋯)