H2π_comp_map — Mathlib

English

H²π commutes with the cocycle map up to left isomorphism.

Русский

H²π коммутирует с отображением кокайклов относительно левого изоморфизма.

LaTeX

$$$ H^2\pi A \circ map\ f\phi\, 2 = mapCocycles_2(f,\phi) \circ H^2\pi B $$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem H2π_comp_map : H2π A ≫ map f φ 2 = mapCocycles₂ f φ ≫ H2π B := by
  simp [H2π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoCocycles₂_hom_assoc]

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