mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃

English

A recurrence expressing mkInductiveAux₂ at n+1 in terms of the previous auxiliary I and isomorphisms, mirroring the previous add-one lemma.

Русский

Рекуррентное выражение mkInductiveAux₂ на n+1 через предыдущий вспомогательный объект I и изоморфизмы.

LaTeX

$$$(mkInductiveAux₂\ e zero comm_zero one comm_one succ (n + 1)) = \langle (P.xNextIso rfl).hom \circ I.1, I.2.1 \circ (Q.xPrevIso rfl).inv, \text{...} \rangle$$$

Lean4

@[reassoc (attr := simp)]
theorem mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃ :
    (mappingConeHomOfDegreewiseSplitIso S σ).inv ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃ =
      -S.g⟦(1 : ℤ)⟧' :=
  by
  ext n
  dsimp [mappingConeHomOfDegreewiseSplitXIso]
  simp only [Int.reduceNeg, id_comp, sub_comp, assoc, mappingCone.inl_v_triangle_mor₃_f, shiftFunctor_obj_X,
    shiftFunctorObjXIso, XIsoOfEq_rfl, Iso.refl_inv, comp_neg, comp_id, mappingCone.inr_f_triangle_mor₃_f, comp_zero,
    sub_zero]

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