rightHomologyι_naturality' — Mathlib

English

RightHomology maps commute with the ι-map in a natural way: rightHomologyMap' φ h₁ h₂ composed with h₂.ι equals h₁.ι composed with opcyclesMap' φ h₁ h₂.

Русский

Правые гомологические отображения commute с ι-маршрутом естественным образом: rightHomologyMap' φ h₁ h₂ ∘ h₂.ι = h₁.ι ∘ opcyclesMap' φ h₁ h₂.

LaTeX

$$$rightHomologyMap'\phi\, h_1\, h_2 \circ h_2.\iota = h_1.\iota \circ opcyclesMap'\phi\, h_1\, h_2$$$

Lean4

@[reassoc (attr := simp)]
theorem rightHomologyι_naturality' : rightHomologyMap' φ h₁ h₂ ≫ h₂.ι = h₁.ι ≫ opcyclesMap' φ h₁ h₂ :=
  RightHomologyMapData.commι _

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