English
If θ: ⟦n+1⟧ ⟶ Δ' is noninjective, there exists i ∈ Fin(n+1) and θ' : ⟦n⟧ ⟶ Δ' with θ = σ_i ∘ θ'.
Русский
Если θ неинъективен, существует i ∈ Fin(n+1) и θ' : ⟦n⟧ ⟶ Δ', такое что θ = σ_i ∘ θ'.
LaTeX
$$$\\\\forall n \\\\forall Δ' \\\\big( θ: \\\\langle n+1 \\\\rangle \\\\to Δ' \\\\big)\\\\forall i\\\\in \\\\mathrm{Fin}(n+1),\\\\ left( h i : θ.toOrderHom(\\\\ castSucc i) = θ.toOrderHom i.succ \\right) \\\Rightarrow \\\\exists θ': \\\\langle n \\\\rangle \\\\to Δ',\\\\ θ = σ_i \\\\circ θ'$$$
Lean4
theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : ⦋n + 1⦌ ⟶ Δ') (i : Fin (n + 1))
(hi : θ.toOrderHom (Fin.castSucc i) = θ.toOrderHom i.succ) : ∃ θ' : ⦋n⦌ ⟶ Δ', θ = σ i ≫ θ' :=
by
use δ i.succ ≫ θ
ext x : 3
simp only [len_mk, σ, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe, Function.comp_apply,
Fin.predAboveOrderHom_coe]
by_cases h' : x ≤ Fin.castSucc i
· rw [Fin.predAbove_of_le_castSucc i x h']
dsimp [δ]
rw [Fin.succAbove_of_castSucc_lt _ _ _]
· rw [Fin.castSucc_castPred]
· exact (Fin.castSucc_lt_succ_iff.mpr h')
· simp only [not_le] at h'
let y := x.pred <| by rintro (rfl : x = 0); simp at h'
have hy : x = y.succ := (Fin.succ_pred x _).symm
rw [hy] at h' ⊢
rw [Fin.predAbove_of_castSucc_lt i y.succ h', Fin.pred_succ]
by_cases h'' : y = i
· rw [h'']
refine hi.symm.trans ?_
congr 1
dsimp [δ]
rw [Fin.succAbove_of_castSucc_lt i.succ]
exact Fin.lt_succ
· dsimp [δ]
rw [Fin.succAbove_of_le_castSucc i.succ _]
simp only [Fin.lt_iff_val_lt_val, Fin.le_iff_val_le_val, Fin.val_succ, Fin.coe_castSucc, Nat.lt_succ_iff,
Fin.ext_iff] at h' h'' ⊢
cutsat
