shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv

English

A shifted boundary morphism composed with the isomorphism of the degreewise split mapping cone equals the negative of the inr morphism of the mapping cone.

Русский

Сдвинутый границы и изоморфизм отображающего коня образуют равенство: f-shift ∘ mappingConeIso.inv = - mappingCone.inr.

LaTeX

$$$S.f^{\langle 1 \rangle}' \circ (\mathrm{mappingConeHomOfDegreewiseSplitIso} S\ σ)^{-1} = -\mathrm{mappingCone.inr} (\mathrm{homOfDegreewiseSplit} S\ σ).$$$

Lean4

@[reassoc (attr := simp)]
theorem shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv :
    S.f⟦(1 : ℤ)⟧' ≫ (mappingConeHomOfDegreewiseSplitIso S σ).inv = -mappingCone.inr _ :=
  by
  ext n
  have h := (σ (n + 1)).f_r
  dsimp at h
  dsimp [mappingConeHomOfDegreewiseSplitXIso]
  rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]

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