induction — Mathlib

English

An elaborated induction step for HigherFacesVanish describing the behavior for intermediate indices a, m, j with refinements on Fin and δ/σ maps. It expresses how the vanishing at q propagates through a sequence of face and degeneracy maps.

Русский

Уточнённый шаг индукции для HigherFacesVanish, описывающий поведение на промежуточных индексах a, m, j с уточнениями по отображениям δ/σ и соответствующим образом распространяется исчезновение на последовательности граней и денегераций.

LaTeX

$$$\text{Induction step for } \text{HigherFacesVanish}$ with refinements on face/degeneracy maps.$$

Lean4

theorem induction {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) :
    HigherFacesVanish (q + 1) (φ ≫ (𝟙 _ + Hσ q).f (n + 1)) :=
  by
  intro j hj₁
  dsimp
  simp only [comp_add, add_comp, comp_id]
    -- when n < q, the result follows immediately from the assumption

  by_cases hqn : n < q
  ·
    rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by cutsat)]
      -- we now assume that n≥q, and write n=a+q

  obtain ⟨a, ha⟩ := Nat.le.dest (not_lt.mp hqn)
  rw [v.comp_Hσ_eq (show n = a + q by cutsat), neg_comp, add_neg_eq_zero, assoc, assoc]
  rcases n with - | m
  · simp only [Nat.eq_zero_of_add_eq_zero_left ha, Fin.eq_zero j, Fin.mk_zero, δ_comp_σ_succ, comp_id]
    rfl
      -- in the other case, we need to write n as m+1
        -- then, we first consider the particular case j = a

  by_cases hj₂ : a = (j : ℕ)
  · simp only [hj₂, Fin.eta, δ_comp_σ_succ, comp_id]
    rfl
      -- now, we assume j ≠ a (i.e. a < j)

  have haj : a < j := (Ne.le_iff_lt hj₂).mp (by cutsat)
  have ham : a ≤ m := by omega
  rw [X.δ_comp_σ_of_gt', j.pred_succ]
  swap
  · rw [Fin.lt_iff_val_lt_val]
    simpa only [Fin.val_mk, Fin.val_succ, add_lt_add_iff_right] using haj
  obtain _ | ham'' := ham.lt_or_eq
  · -- case where `a<m`

    rw [← X.δ_comp_δ''_assoc]
    swap
    · rw [Fin.le_iff_val_le_val]
      dsimp
      cutsat
    simp only [← assoc, v j (by cutsat), zero_comp]
  · -- in the last case, a=m, q=1 and j=a+1

    rw [X.δ_comp_δ_self'_assoc]
    swap
    · ext
      cases j
      dsimp
      dsimp only [Nat.succ_eq_add_one] at *
      cutsat
    simp only [← assoc, v j (by cutsat), zero_comp]

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