toCocycles — Mathlib

English

The map from i-cochains to j-cocycles is defined by applying the differential to appropriate indices.

Русский

Отображение от i-коцеп до j-коциклов задаётся применением дифференциала к соответствующим индексам.

LaTeX

$$$$ toCocycles(i,j) : C^i(G,A) \\to Z^j(G,A) \\quad \\text{defined by } x \\mapsto d^i x \\text{ (in the appropriate target).} $$$$

Lean4

/-- This is the map from `i`-cochains to `j`-cocycles induced by the differential in the complex of
inhomogeneous cochains. -/
abbrev toCocycles (i j : ℕ) : (inhomogeneousCochains A).X i ⟶ cocycles A j :=
  (inhomogeneousCochains A).toCycles i j

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