factor_δ_spec — Mathlib

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_δ, δ, σ]

Похожие утверждения