cyclesMap'_i — Mathlib

English

The morphism cyclesMap' between two left-homology data intertwines the inclusions i; i.e., cyclesMap' φ h1 h2 followed by h2.i equals h1.i followed by φ.τ₂.

Русский

Гомоморфизм cyclesMap' между двумя данными левой гомологии интерпретирует включения i; то есть cyclesMap' φ h1 h2 затем i₂ равно i₁ затем φ.τ₂.

LaTeX

$$$cyclesMap'(\phi,h_1,h_2) \circ h_2.i = h_1.i \circ \phi.\tau_2$$$

Lean4

@[reassoc (attr := simp)]
theorem cyclesMap'_i : cyclesMap' φ h₁ h₂ ≫ h₂.i = h₁.i ≫ φ.τ₂ :=
  LeftHomologyMapData.commi _

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