English
Naturality with respect to a morphism φ: S1 → S2 states that pre- and post-compositions with left/right maps commute with the left-right homology comparison, up to the appropriate maps on S1 and S2.
Русский
Естественность по отношению к морфизму φ: S1 → S2 формулирует, что предварительная и последующая композиции с левыми/правыми отображениями коммутируют с сопоставлением лево-правой гомологии через соответствующие отображения на S1 и S2.
LaTeX
$$$\\text{leftHomologyMap}'(\\varphi,h_1,h_1') \\; \\text{leftRightHomologyComparison}'(h_1',h_2') = \\text{leftRightHomologyComparison}'(h_1,h_2) \\; \\text{rightHomologyMap}'(\\varphi,h_2,h_2')$$$
Lean4
@[reassoc]
theorem leftRightHomologyComparison'_naturality (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₁.RightHomologyData)
(h₁' : S₂.LeftHomologyData) (h₂' : S₂.RightHomologyData) :
leftHomologyMap' φ h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' =
leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' φ h₂ h₂' :=
by
simp only [← cancel_epi h₁.π, ← cancel_mono h₂'.ι, assoc, leftHomologyπ_naturality'_assoc, rightHomologyι_naturality',
π_leftRightHomologyComparison'_ι, π_leftRightHomologyComparison'_ι_assoc, cyclesMap'_i_assoc, p_opcyclesMap']
