English
Equivalence of Splittings is determined by their component s.s.
Русский
Эквивалентность разбиений определяется компонентой s.s.
LaTeX
$$ext_s (s s' : S.Splitting) (h : s.s = s'.s) : s = s' $$
Lean4
/-- An auxiliary construction for `mkInductive`.
Here we build by induction a family of diagrams,
but don't require at the type level that these successive diagrams actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy)
in `mkInductive`.
At this stage, we don't check the homotopy condition in degree 0,
because it "falls off the end", and is easier to treat using `xNext` and `xPrev`,
which we do in `mkInductiveAux₂`.
-/
@[simp, nolint unusedArguments]
def mkInductiveAux₁ :
∀ n,
Σ' (f : P.X n ⟶ Q.X (n + 1)) (f' : P.X (n + 1) ⟶ Q.X (n + 2)),
e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)
| 0 => ⟨zero, one, comm_one⟩
| 1 => ⟨one, (succ 0 ⟨zero, one, comm_one⟩).1, (succ 0 ⟨zero, one, comm_one⟩).2⟩
| n + 2 =>
⟨(mkInductiveAux₁ (n + 1)).2.1, (succ (n + 1) (mkInductiveAux₁ (n + 1))).1,
(succ (n + 1) (mkInductiveAux₁ (n + 1))).2⟩
