English
A higher inductive compatibility: mkInductiveAux₃ relates mkInductiveAux₂ at two indices i and j with i+1 = j and uses the already proven compatibility to produce a coherent identity of morphisms in the two-step extension.
Русский
Совместимость на более высоком уровне: mkInductiveAux₃ связывает mkInductiveAux₂ на двух индексаx i и j при условии i+1 = j и использует уже доказанную совместимость для получения связной тождности морфизмов в двухшаговом продолжении.
LaTeX
$$$\forall i\ j,\ h:\; i+1=j \; →\n\ (Homotopy.mkInductiveAux₂\ e\ zero comm_zero one comm_one succ i).snd.fst \\; \cdot (HomologicalComplex.xPrevIso Q\ h).hom = (HomologicalComplex.xNextIso P\ h).inv \\cdot (Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst$$$
Lean4
/-- The canonical isomorphism `mappingCone (homOfDegreewiseSplit S σ) ≅ S.X₂⟦(1 : ℤ)⟧`. -/
@[simps!]
noncomputable def mappingConeHomOfDegreewiseSplitIso : mappingCone (homOfDegreewiseSplit S σ) ≅ S.X₂⟦(1 : ℤ)⟧ :=
Hom.isoOfComponents (fun p => mappingConeHomOfDegreewiseSplitXIso S σ p _ rfl)
(by
rintro p _ rfl
have r_f := (σ (p + 1 + 1)).r_f
have s_g := (σ (p + 1)).s_g
dsimp at r_f s_g ⊢
simp only [mappingConeHomOfDegreewiseSplitXIso, mappingCone.ext_from_iff _ _ _ rfl,
mappingCone.inl_v_d_assoc _ (p + 1) _ (p + 1 + 1) (by linarith) (by cutsat), cocycleOfDegreewiseSplit, r_f,
Int.reduceNeg, Cochain.ofHom_v, sub_comp, assoc, Hom.comm, comp_sub, mappingCone.inl_v_fst_v_assoc,
mappingCone.inl_v_snd_v_assoc, shiftFunctor_obj_X', zero_comp, sub_zero, homOfDegreewiseSplit_f,
mappingCone.inr_f_fst_v_assoc, comp_zero, zero_sub, mappingCone.inr_f_snd_v_assoc, neg_neg,
mappingCone.inr_f_d_assoc, shiftFunctor_obj_d', Int.negOnePow_one, neg_comp, sub_neg_eq_add, zero_add, and_true,
Units.neg_smul, one_smul, comp_neg, ShortComplex.map_X₂, eval_obj, Cocycle.mk_coe, Cochain.mk_v]
simp only [← S.g.comm_assoc, reassoc_of% s_g, comp_id]
abel)
