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 (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• 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 α

theorem NonemptyFiniteLinearOrder.Nonempty {α : Type u_1} [self : NonemptyFiniteLinearOrder α] : Nonempty α

@[instance 100]

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 PUnit.nonemptyFiniteLinearOrder.proof_1

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 α = NonemptyFiniteLinearOrder.mk ⋯

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

Equations

• instNonemptyFiniteLinearOrderOrderDual α = NonemptyFiniteLinearOrder.mk ⋯

def NonemptyFinLinOrd : Type (u_1 + 1)

The category of nonempty finite linear orders.

Equations

• NonemptyFinLinOrd = CategoryTheory.Bundled NonemptyFiniteLinearOrder

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

Equations

• NonemptyFinLinOrd.instParentProjectionLinearOrderNonemptyFiniteLinearOrderToLinearOrder = ⋯

instance NonemptyFinLinOrd.instConcreteCategory : CategoryTheory.ConcreteCategory NonemptyFinLinOrd

Equations

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

instance NonemptyFinLinOrd.instCoeSortType : CoeSort NonemptyFinLinOrd (Type u_1)

Equations

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

Equations

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

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

Equations

• α.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 = ↑e.symm

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

@[simp]

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

@[simp]

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

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.dualEquiv_inverse : NonemptyFinLinOrd.dualEquiv.inverse = NonemptyFinLinOrd.dual

@[simp]

theorem NonemptyFinLinOrd.dualEquiv_functor : NonemptyFinLinOrd.dualEquiv.functor = 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.instFunLikeHomαNonemptyFiniteLinearOrder {A : NonemptyFinLinOrd} {B : NonemptyFinLinOrd} : FunLike (A ⟶ B) ↑A ↑B

Equations

• NonemptyFinLinOrd.instFunLikeHomαNonemptyFiniteLinearOrder = { coe := fun (f : A ⟶ B) => ⇑(let_fun this := f; this), coe_injective' := ⋯ }

instance NonemptyFinLinOrd.instOrderHomClassHomαNonemptyFiniteLinearOrder {A : NonemptyFinLinOrd} {B : NonemptyFinLinOrd} : OrderHomClass (A ⟶ B) ↑A ↑B

Equations

• ⋯ = ⋯

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).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.instSplitEpiCategory : CategoryTheory.SplitEpiCategory NonemptyFinLinOrd

Equations

• NonemptyFinLinOrd.instSplitEpiCategory = ⋯

instance NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations : CategoryTheory.Limits.HasStrongEpiMonoFactorisations NonemptyFinLinOrd

Equations

• NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations = ⋯

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 ⋯