English
An inductive auxiliary construction producing a family of diagrams, parameterized by n, encoding stepwise compatibility conditions for inductive definitions in homological settings.
Русский
Индуктивная вспомогательная конструкция порождает семейство диаграмм, параметризованных по n, кодируя пошаговые условия совместимости для индуктивных определений в гомологической алгебре.
LaTeX
$$$ \\mathrm{mkInductiveAux}_1 : \\mathbb{N} \\to \\Sigma' (f : P.X n \\to Q.X (n+1)) (f' : P.X (n+1) \\to Q.X (n+2)), \\ e.f(n+1) = P.d(n+1,n) \\circ f + f' \\circ Q.d(n+2,n+1) $$$
Lean4
theorem nullHomotopicMap_f_of_not_rel_left {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₀ : ∀ l : ι, ¬c.Rel k₀ l)
(hom : ∀ i j, C.X i ⟶ D.X j) : (nullHomotopicMap hom).f k₀ = hom k₀ k₁ ≫ D.d k₁ k₀ :=
by
dsimp only [nullHomotopicMap]
rw [prevD_eq hom r₁₀, dNext, AddMonoidHom.mk'_apply, C.shape, zero_comp, zero_add]
exact
hk₀
_
-- Cannot be @[simp] because `k₁` cannot be inferred by `simp`.
