English
If for all k ∈ Fin(m+1) we have f.toOrderHom k ≠ j, then factor_δ f j ≫ δ j = f; i.e., the factorization is exact when j is not in the image of f.
Русский
Если для всех k ∈ Fin(m+1) выполняется f.toOrderHom k ≠ j, то factor_δ f j ∘ δ j = f; факторизация точна, когда j не лежит в образе f.
LaTeX
$$$\\forall f, j, (\\forall k \\in \\mathrm{Fin}(m+1), f.toOrderHom k \\neq j) \\Rightarrow \\text{factor}_{\\delta}(f,j) \\circ δ_j = f.$$$
Lean4
theorem factor_δ_spec {m n : ℕ} (f : ⦋m⦌ ⟶ ⦋n + 1⦌) (j : Fin (n + 2)) (hj : ∀ (k : Fin (m + 1)), f.toOrderHom k ≠ j) :
factor_δ f j ≫ δ j = f := by
ext k : 3
cases j using Fin.cases <;> simp_all [factor_δ, δ, σ]