extend_exactAt_iff — Mathlib

English

Relates inverses of extended cycles to the original cycles under extension by e, showing a compatibility between extend and iCycles.

Русский

Связанность обратных образов расширенных циклов с исходными циклами при расширении через e, демонстрирующая совместимость extend и iCycles.

LaTeX

$$(K.extendCyclesIso e hj').inv ≫ (K.extend e).iCycles j' = K.iCycles j ≫ (K.extendXIso e hj').inv$$

Lean4

theorem extend_exactAt_iff : (K.extend e).ExactAt j' ↔ K.ExactAt j :=
  by
  simp only [HomologicalComplex.exactAt_iff_isZero_homology]
  exact (K.extendHomologyIso e hj').isZero_iff

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