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 ⊤.

class NonemptyFiniteLinearOrder (α : Type u_1) extends Fintype , LinearOrder : Type u_1

A typeclass for nonempty finite linear orders.

• elems : Finset α
• complete : ∀ (x : α), x ∈ Fintype.elems
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
• Nonempty : Nonempty α

instance NonemptyFiniteLinearOrder.toBoundedOrder (α : Type u_1) [NonemptyFiniteLinearOrder α] : BoundedOrder α

Equations

• NonemptyFiniteLinearOrder.toBoundedOrder α = Fintype.toBoundedOrder α

instance PUnit.nonemptyFiniteLinearOrder : NonemptyFiniteLinearOrder PUnit.{u_1 + 1}

Equations

• PUnit.nonemptyFiniteLinearOrder = NonemptyFiniteLinearOrder.mk

instance Fin.nonemptyFiniteLinearOrder (n : ℕ) : NonemptyFiniteLinearOrder (Fin (n + 1))

Equations

• Fin.nonemptyFiniteLinearOrder n = NonemptyFiniteLinearOrder.mk

instance ULift.nonemptyFiniteLinearOrder (α : Type u) [NonemptyFiniteLinearOrder α] : NonemptyFiniteLinearOrder (ULift.{v, u} α)

Equations

• ULift.nonemptyFiniteLinearOrder α = let src := LinearOrder.lift' ⇑Equiv.ulift (_ : Function.Injective ⇑Equiv.ulift); NonemptyFiniteLinearOrder.mk

instance instNonemptyFiniteLinearOrderOrderDual (α : Type u_1) [NonemptyFiniteLinearOrder α] : NonemptyFiniteLinearOrder αᵒᵈ

Equations

• instNonemptyFiniteLinearOrderOrderDual α = let src := OrderDual.fintype α; NonemptyFiniteLinearOrder.mk

def NonemptyFinLinOrd : Type (u_1 + 1)

The category of nonempty finite linear orders.

Equations

• NonemptyFinLinOrd = CategoryTheory.Bundled NonemptyFiniteLinearOrder

instance NonemptyFinLinOrd.instParentProjectionTypeLinearOrderNonemptyFiniteLinearOrderToLinearOrder : CategoryTheory.BundledHom.ParentProjection @NonemptyFiniteLinearOrder.toLinearOrder

Equations

• NonemptyFinLinOrd.instParentProjectionTypeLinearOrderNonemptyFiniteLinearOrderToLinearOrder = (_ : CategoryTheory.BundledHom.ParentProjection @NonemptyFiniteLinearOrder.toLinearOrder)

instance NonemptyFinLinOrd.instConcreteCategoryNonemptyFinLinOrdInstNonemptyFinLinOrdLargeCategory : CategoryTheory.ConcreteCategory NonemptyFinLinOrd

Equations

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

instance NonemptyFinLinOrd.instCoeSortNonemptyFinLinOrdType : CoeSort NonemptyFinLinOrd (Type u_1)

Equations

• NonemptyFinLinOrd.instCoeSortNonemptyFinLinOrdType = CategoryTheory.Bundled.coeSort

def NonemptyFinLinOrd.of (α : Type u_1) [NonemptyFiniteLinearOrder α] : NonemptyFinLinOrd

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations

• NonemptyFinLinOrd.of α = CategoryTheory.Bundled.of α

@[simp]

theorem NonemptyFinLinOrd.coe_of (α : Type u_1) [NonemptyFiniteLinearOrder α] : ↑(NonemptyFinLinOrd.of α) = α

instance NonemptyFinLinOrd.instInhabitedNonemptyFinLinOrd : Inhabited NonemptyFinLinOrd

Equations

• NonemptyFinLinOrd.instInhabitedNonemptyFinLinOrd = { default := NonemptyFinLinOrd.of PUnit.{u_1 + 1} }

instance NonemptyFinLinOrd.instNonemptyFiniteLinearOrderα (α : NonemptyFinLinOrd) : NonemptyFiniteLinearOrder ↑α

Equations

• NonemptyFinLinOrd.instNonemptyFiniteLinearOrderα α = α.str

instance NonemptyFinLinOrd.hasForgetToLinOrd : CategoryTheory.HasForget₂ NonemptyFinLinOrd LinOrd

Equations

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

instance NonemptyFinLinOrd.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ NonemptyFinLinOrd FinPartOrd

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def NonemptyFinLinOrd.dual : CategoryTheory.Functor NonemptyFinLinOrd NonemptyFinLinOrd

OrderDual as a functor.

Equations

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

@[simp]

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

@[simp]

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

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.

instance NonemptyFinLinOrd.instFunLikeHomNonemptyFinLinOrdToQuiverToCategoryStructInstNonemptyFinLinOrdLargeCategoryαNonemptyFiniteLinearOrder {A : NonemptyFinLinOrd} {B : NonemptyFinLinOrd} : FunLike (A ⟶ B) ↑A ↑B

Equations

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

instance NonemptyFinLinOrd.instOrderHomClassHomNonemptyFinLinOrdToQuiverToCategoryStructInstNonemptyFinLinOrdLargeCategoryαNonemptyFiniteLinearOrderToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeToLinearOrderInstNonemptyFiniteLinearOrderαInstFunLikeHomNonemptyFinLinOrdToQuiverToCategoryStructInstNonemptyFinLinOrdLargeCategoryαNonemptyFiniteLinearOrder {A : NonemptyFinLinOrd} {B : NonemptyFinLinOrd} : OrderHomClass (A ⟶ B) ↑A ↑B

Equations

• (_ : OrderHomClass (A ⟶ B) ↑A ↑B) = (_ : RelHomClass (A ⟶ B) (fun (x x_1 : ↑A) => x ≤ x_1) fun (x x_1 : ↑B) => x ≤ x_1)

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

theorem NonemptyFinLinOrd.forget_map_apply {A : NonemptyFinLinOrd} {B : NonemptyFinLinOrd} (f : A ⟶ B) (a : ↑A) : (CategoryTheory.forget NonemptyFinLinOrd).toPrefunctor.map f a = f.toFun a

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

instance NonemptyFinLinOrd.instSplitEpiCategoryNonemptyFinLinOrdInstNonemptyFinLinOrdLargeCategory : CategoryTheory.SplitEpiCategory NonemptyFinLinOrd

Equations

• NonemptyFinLinOrd.instSplitEpiCategoryNonemptyFinLinOrdInstNonemptyFinLinOrdLargeCategory = (_ : CategoryTheory.SplitEpiCategory NonemptyFinLinOrd)

instance NonemptyFinLinOrd.instHasStrongEpiMonoFactorisationsNonemptyFinLinOrdInstNonemptyFinLinOrdLargeCategory : CategoryTheory.Limits.HasStrongEpiMonoFactorisations NonemptyFinLinOrd

Equations

• NonemptyFinLinOrd.instHasStrongEpiMonoFactorisationsNonemptyFinLinOrdInstNonemptyFinLinOrdLargeCategory = (_ : CategoryTheory.Limits.HasStrongEpiMonoFactorisations NonemptyFinLinOrd)

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

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

The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd and order_dual commute.

Equations

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