English
If θ: ⟦n+1⟧ ⟶ Δ' is not injective, there exists i and θ' with θ = σ_i ∘ θ'.
Русский
Если θ: ⟦n+1⟧ ⟶ Δ' не инъективен, существует i и θ' с θ = σ_i ∘ θ'.
LaTeX
$$$\\\\forall {n} {Δ'} \\\\big( θ: \\\\langle n+1 \\\\rangle \\\\to Δ' \\\\big),\\\\ Not(Injective(OrderHom.instFunLike.coe (SimplexCategory.Hom.toOrderHom θ))) \\\\Rightarrow \\\\Exists i \\\\Rightarrow \\\\Exists θ': \\\\langle n \\\\rangle \\\\to Δ', \\\\ θ = σ_i \\\\circ θ'$$$
Lean4
theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : ⦋n + 1⦌ ⟶ Δ')
(hθ : ¬Function.Injective θ.toOrderHom) : ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ' :=
by
simp only [Function.Injective, exists_prop, not_forall] at hθ
have hθ₂ : ∃ x y : Fin (n + 2), (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y :=
by
rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
by_cases h : x < y
· exact ⟨x, y, ⟨h₁, h⟩⟩
· refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩
cutsat
rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩
use x.castPred ((Fin.le_last _).trans_lt' h₂).ne
apply eq_σ_comp_of_not_injective'
apply le_antisymm
· exact θ.toOrderHom.monotone (le_of_lt (Fin.castSucc_lt_succ _))
· rw [Fin.castSucc_castPred, h₁]
exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)
