δ_naturality — Mathlib

English

The δ morphism is natural with respect to a morphism φ of short complexes; the δ maps commute with the homology maps of φ.

Русский

δ-морфизм естествен по отношению к морфизму φ между короткими комплексами; отображения δ коммутируют с гомологическими отображениями φ.

LaTeX

$$hS₁.δ i j hij ≫ HomologicalComplex.homologyMap φ.τ₁ _ = HomologicalComplex.homologyMap φ.τ₃ _ ≫ hS₂.δ i j hij$$

Lean4

@[reassoc]
theorem δ_naturality (i j : ι) (hij : c.Rel i j) :
    hS₁.δ i j hij ≫ HomologicalComplex.homologyMap φ.τ₁ _ = HomologicalComplex.homologyMap φ.τ₃ _ ≫ hS₂.δ i j hij :=
  ShortComplex.SnakeInput.naturality_δ (mapSnakeInput φ hS₁ hS₂ i j hij)

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