homologyπ_extendHomologyIso_inv — Mathlib

English

Relates the π-morphism composed with the inverse of extendHomologyIso to the inverse of extendCyclesIso composed with homologyπ.

Русский

Связь композиции π с обратным extendHomologyIso и композиции extendCyclesIso с homologyπ.

LaTeX

$$K.homologyπ j ≫ (K.extendHomologyIso e hj').inv = (K.extendCyclesIso e hj').inv ≫ (K.extend e).homologyπ j'$$

Lean4

@[reassoc (attr := simp)]
theorem homologyπ_extendHomologyIso_inv :
    K.homologyπ j ≫ (K.extendHomologyIso e hj').inv = (K.extendCyclesIso e hj').inv ≫ (K.extend e).homologyπ j' := by
  simp only [← cancel_mono (K.extendHomologyIso e hj').hom, assoc, Iso.inv_hom_id, comp_id,
    homologyπ_extendHomologyIso_hom, Iso.inv_hom_id_assoc]

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