extendHomologyIso_hom_naturality — Mathlib

English

Reiterates the naturality relation between extendCyclesIso and cyclesMap.

Русский

Повторение естественного соотношения между extendCyclesIso и cyclesMap.

LaTeX

$$cyclesMap (extendMap φ e) j' ≫ (L.extendCyclesIso e hj').hom = (K.extendCyclesIso e hj').hom ≫ cyclesMap φ j$$

Lean4

@[reassoc (attr := simp)]
theorem extendHomologyIso_hom_naturality :
    homologyMap (extendMap φ e) j' ≫ (L.extendHomologyIso e hj').hom =
      (K.extendHomologyIso e hj').hom ≫ homologyMap φ j :=
  by simp [← cancel_epi ((K.extend e).homologyπ _)]

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