homologyOpIso_hom_naturality — Mathlib

English

Given S1,S2 with homology, the naturality of the homology op is reflected in the commutativity between the maps obtained from φ and the op-map. This ensures compatibility of the opIsos with homology maps.

Русский

У гомологии op естественным образом сохраняется совместимость с гомологическими отображениями: гомология в противоположном контексте согласуется с отображением φ и операциями противоположного контекста.

LaTeX

$$homologyMap (opMap φ) ≫ (S1.homologyOpIso).hom = S2.homologyOpIso.hom ≫ (homologyMap φ).op$$

Lean4

@[reassoc]
theorem homologyOpIso_hom_naturality [S₁.HasHomology] [S₂.HasHomology] :
    homologyMap (opMap φ) ≫ (S₁.homologyOpIso).hom = S₂.homologyOpIso.hom ≫ (homologyMap φ).op := by
  simp [homologyMap_op]

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