extend_d_eq — Mathlib

English

The differential in the extended complex is obtained by conjugating the original differential with the canonical extension isomorphisms.

Русский

Дифференциал в расширенном комплексе получается за счет сопряжения исходного дифференциала каноническими изоморфизмами расширения.

LaTeX

$$$(K\\extend e)\\,d\\,i'\\,j' = (K\\extendXIso e\\; hi).\\hom \\;\\circ\\; K.d\\; i\\, j \\;\\circ\\; (K\\extendXIso e\\; hj).\\inv$$$

Lean4

theorem extend_d_eq {i' j' : ι'} {i j : ι} (hi : e.f i = i') (hj : e.f j = j') :
    (K.extend e).d i' j' = (K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv := by apply extend.d_eq

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