The nondegenerate simplices in the nerve of a partially ordered type

In this file, we show that if X is a partially ordered type, then an n-simplex s of the nerve is nondegenerate iff the monotone map s.obj : Fin (n + 1) → X is strictly monotone.

theorem PartialOrder.mem_range_nerve_σ_iff {X : Type u_1} [PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n + 1 })) (i : Fin (n + 1)) : s ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (CategoryTheory.nerve X) i)) ↔ s.obj i.castSucc = s.obj i.succ

theorem PartialOrder.mem_nerve_degenerate_of_eq {X : Type u_1} [PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n + 1 })) {i : Fin (n + 1)} (hi : s.obj i.castSucc = s.obj i.succ) : s ∈ (CategoryTheory.nerve X).degenerate (n + 1)

theorem PartialOrder.mem_nerve_nonDegenerate_iff_strictMono {X : Type u_1} [PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n })) : s ∈ (CategoryTheory.nerve X).nonDegenerate n ↔ StrictMono s.obj

theorem PartialOrder.mem_nerve_nonDegenerate_iff_injective {X : Type u_1} [PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n })) : s ∈ (CategoryTheory.nerve X).nonDegenerate n ↔ Function.Injective s.obj

theorem PartialOrder.nerve_ofSimplex_le_ofSimplex_iff {X : Type u_1} [PartialOrder X] {n m : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n })) (t : (CategoryTheory.nerve X).obj (Opposite.op { len := m })) : SSet.Subcomplex.ofSimplex s ≤ SSet.Subcomplex.ofSimplex t ↔ Set.range s.obj ⊆ Set.range t.obj