f'_cyclesMap' — Mathlib

English

The morphism f' from left-homology data commutes with cyclesMap'; i.e., h1.f' followed by cyclesMap' equals φ.τ₁ followed by h2.f'.

Русский

Гомоморфизм f' совместим с cyclesMap'; то есть h1.f' затем cyclesMap' равняется φ.τ₁ затем h2.f'.

LaTeX

$$$h_1.f' \circ cyclesMap'(\phi,h_1,h_2) = \phi.\tau_1 \circ h_2.f'$$

Lean4

@[reassoc (attr := simp)]
theorem f'_cyclesMap' : h₁.f' ≫ cyclesMap' φ h₁ h₂ = φ.τ₁ ≫ h₂.f' := by
  simp only [← cancel_mono h₂.i, assoc, φ.comm₁₂, cyclesMap'_i, LeftHomologyData.f'_i_assoc, LeftHomologyData.f'_i]

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