mappingConeHomOfDegreewiseSplitXIso

English

There is a canonical isomorphism between the mapping cone of the degreewise split homomorphism and the shifted second component of the short complex S, i.e., mappingCone(homOfDegreewiseSplit S σ) ≅ S.X₂⟦1⟧.

Русский

Существует каноническое изоморфизм между отображающим конем гомоморфизма с разложением по степеням и смещённым вторым компонентом короткого комплекса S, то есть mappingCone(homOfDegreewiseSplit S σ) ≅ S.X₂⟦1⟧.

LaTeX

$$$\operatorname{mappingCone}(\mathrm{homOfDegreewiseSplit} S\ σ) \cong S.X_2\langle 1 \rangle,$$$

Lean4

/-- The canonical isomorphism `(mappingCone (homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X q`
when `p + 1 = q`. -/
noncomputable def mappingConeHomOfDegreewiseSplitXIso (p q : ℤ) (hpq : p + 1 = q) :
    (mappingCone (homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X q
    where
  hom :=
    (mappingCone.fst (homOfDegreewiseSplit S σ)).1.v p q hpq ≫ (σ q).s -
      (mappingCone.snd (homOfDegreewiseSplit S σ)).v p p (add_zero p) ≫ by
        exact (Cochain.ofHom S.f).v (p + 1) q (by omega)
  inv :=
    S.g.f q ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v q p (by omega) - by
      exact (σ q).r ≫ (S.X₁.XIsoOfEq hpq.symm).hom ≫ (mappingCone.inr (homOfDegreewiseSplit S σ)).f p
  hom_inv_id := by
    subst hpq
    have s_g := (σ (p + 1)).s_g
    have f_r := (σ (p + 1)).f_r
    dsimp at s_g f_r
        ⊢
          -- the following list of lemmas was obtained by doing
              -- simp? [mappingCone.ext_from_iff _ (p + 1) _ rfl, reassoc_of% f_r, reassoc_of% s_g]
              -- which may require increasing maximum heart beats

    simp only [Cochain.ofHom_v, Int.reduceNeg, id_comp, comp_sub, sub_comp, assoc, reassoc_of% s_g,
      ShortComplex.Splitting.s_r_assoc, ShortComplex.map_X₃, eval_obj, ShortComplex.map_X₁, zero_comp, comp_zero,
      reassoc_of% f_r, zero_sub, sub_neg_eq_add, mappingCone.ext_from_iff _ (p + 1) _ rfl, comp_add,
      mappingCone.inl_v_fst_v_assoc, mappingCone.inl_v_snd_v_assoc, shiftFunctor_obj_X', sub_zero, add_zero, comp_id,
      mappingCone.inr_f_fst_v_assoc, mappingCone.inr_f_snd_v_assoc, add_eq_right, neg_eq_zero, true_and]
    rw [← comp_f_assoc, S.zero, zero_f, zero_comp]
  inv_hom_id := by
    subst hpq
    have h := (σ (p + 1)).id
    dsimp at h ⊢
    simp only [id_comp, Cochain.ofHom_v, comp_sub, sub_comp, assoc, mappingCone.inl_v_fst_v_assoc,
      mappingCone.inr_f_fst_v_assoc, shiftFunctor_obj_X', zero_comp, comp_zero, sub_zero, mappingCone.inl_v_snd_v_assoc,
      mappingCone.inr_f_snd_v_assoc, zero_sub, sub_neg_eq_add, ← h]
    abel

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