map_opcyclesMap' — Mathlib

English

For S with right homology data, the mapped short complex under F has right homology iso equal to the transposition of the mapped right homology iso and F.mapIso: S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm.

Русский

Для S с правой гомологией отображение S под F имеет изоморфизм правой гомологии, образованный через трансизоморфизм и F.mapIso.

LaTeX

$$$S.mapRightHomologyIso F = (hr.map F).rightHomologyIso \;\overset{\text{trans}}{=}\; F.mapIso hr.rightHomologyIso.symm.$$$

Lean4

theorem map_opcyclesMap' :
    F.map (ShortComplex.opcyclesMap' φ hr₁ hr₂) =
      ShortComplex.opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F) :=
  by
  have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default
  rw [γ.opcyclesMap'_eq, (γ.map F).opcyclesMap'_eq, ShortComplex.RightHomologyMapData.map_φQ]

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