p_opcyclesMap' — Mathlib

English

For any φ between short complexes, the p-component is compatible with opcyclesMap' in the sense that h₁.p followed by opcyclesMap' equals φ.τ₂ followed by h₂.p.

Русский

Для любого отображения φ между короткими комплексами, p-компонента совместима с opcyclesMap': h₁.p затем opcyclesMap' равняется φ.τ₂ затем h₂.p.

LaTeX

$$$h_1.p \circ opcyclesMap' \phi\, h_1\, h_2 = \phi.\tau_2 \circ h_2.p$$$

Lean4

@[reassoc (attr := simp)]
theorem p_opcyclesMap' : h₁.p ≫ opcyclesMap' φ h₁ h₂ = φ.τ₂ ≫ h₂.p :=
  RightHomologyMapData.commp _

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