opcyclesMap'_g' — Mathlib

English

The map opcyclesMap' satisfies a naturality-type relation with g', i.e., opcyclesMap' φ h₁ h₂ composed with h₂.g' equals h₁.g' composed with φ.τ₃.

Русский

Карта opcyclesMap' удовлетворяет натуральности с g': opcyclesMap' φ h₁ h₂ ∘ h₂.g' = h₁.g' ∘ φ.τ₃.

LaTeX

$$$opcyclesMap'\phi\, h_1\, h_2 \circ h_2.g' = h_1.g' \circ \phi.\tau_3$$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesMap'_g' : opcyclesMap' φ h₁ h₂ ≫ h₂.g' = h₁.g' ≫ φ.τ₃ := by
  simp only [← cancel_epi h₁.p, φ.comm₂₃, p_opcyclesMap'_assoc, RightHomologyData.p_g'_assoc, RightHomologyData.p_g']

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