homologySequenceδ_naturality — Mathlib

English

δ commutes with morphisms of distinguished triangles: for φ: T → T′ the naturality square involving φ and the shift maps commutes.

Русский

δ удовлетворяет натурализму относительно морфизмов distinguished triangles: диаграмма с φ и соответствующими отображениями сдвигов commuting.

LaTeX

$$$\text{nat}_{F}(T,T',\phi): (F.shift n_0).map\phi.hom_3 \circ δ_{F,T',n_0,n_1,h} = δ_{F,T,n_0,n_1,h} \circ (F.shift n_1).map\phi.hom_1$$$

Lean4

@[reassoc]
theorem homologySequenceδ_naturality [F.ShiftSequence ℤ] (T T' : Triangle C) (φ : T ⟶ T') (n₀ n₁ : ℤ)
    (h : n₀ + 1 = n₁) :
    (F.shift n₀).map φ.hom₃ ≫ F.homologySequenceδ T' n₀ n₁ h =
      F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map φ.hom₁ :=
  by
  dsimp only [homologySequenceδ]
  rw [← shiftMap_comp', ← φ.comm₃, shiftMap_comp]

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