splitMonoδ — Mathlib

English

For each i, δ_i is a split monomorphism, with a specified retraction σ_i (and the identity realized by δ_i.castSucc ≫ σ_i).

Русский

Для каждого i диаграмма δ_i образует разложение как split-mono: существует прогоражение σ_i и δ_i.castSucc ≫ σ_i = id.

LaTeX

$$$\mathrm{SplitMono}(\delta_i)$$$

Lean4

/-- `δ i` is a split monomorphism thanks to the simplicial identities. -/
def splitMonoδ {n : ℕ} (i : Fin (n + 2)) : SplitMono (δ i)
    where
  retraction := by
    induction i using Fin.lastCases with
    | last => exact σ (Fin.last n)
    | cast i => exact σ i
  id := by
    cases i using Fin.lastCases
    · simp only [Fin.lastCases_last]
      exact δ_comp_σ_succ
    · simp only [Fin.lastCases_castSucc]
      exact δ_comp_σ_self

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