H2π — Mathlib

English

There is a natural quotient map from the 2-cycles of A, viewed as a submodule of the inhomogeneous chain complex, onto H2(G,A).

Русский

Существует естественная факторная карта из подмодуля 2-циклов (2-cycle) A в H2(G,A).

LaTeX

$$$H_2^{\\pi}(A) : \\mathrm{cycles}_2(A) \\to H_2(A), \\quad x \\mapsto [x].$$$

Lean4

/-- The quotient map from the 2-cycles of `A`, as a submodule of `G × G →₀ A`, to `H₂(G, A)`. -/
def H2π : ModuleCat.of k (cycles₂ A) ⟶ H2 A :=
  (isoCycles₂ A).inv ≫ π A 2

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