English
For every natural number n, there exist morphisms f and f' making the component e.f(n) decompose as a sum of a left- and right-hand differential: e.f(n) = P.dFrom(n) ∘ f + f' ∘ Q.dTo(n). This is the inductive description of e along the two-term step in the degreewise construction.
Русский
Пусть для каждого натурального числа n существует пара морфизмов f и f', таких что компонент e.f(n) раскладывается как сумма двух частей: e.f(n) = P.dFrom(n) ∘ f + f' ∘ Q.dTo(n). Это индуктивное разложение e вдоль двухступенчатого шага в единообразной степени.
LaTeX
$$$\forall n \in \mathbb{N}, \exists f : P.X_n \to Q.X_{n+1}, \exists f' : P.X_{n+1} \to Q.X_{n+2},\ e.f(n) = P.dFrom(n) \circ f + f' \circ Q.dTo(n).$$$
Lean4
/-- An auxiliary construction for `mkInductive`.
-/
def mkInductiveAux₂ : ∀ n, Σ' (f : P.xNext n ⟶ Q.X n) (f' : P.X n ⟶ Q.xPrev n), e.f n = P.dFrom n ≫ f + f' ≫ Q.dTo n
| 0 => ⟨0, zero ≫ (Q.xPrevIso rfl).inv, by simpa using comm_zero⟩
| n + 1 =>
let I := mkInductiveAux₁ e zero one comm_one succ n
⟨(P.xNextIso rfl).hom ≫ I.1, I.2.1 ≫ (Q.xPrevIso rfl).inv, by simpa using I.2.2⟩
