English
There exists a canonical k-linear map from the free k-module on G-words with coefficients in A to the kernel (in k) of the action map on coinvariants; this map is realized by restricting the 0-th differential to the span that generates the coinvariants-ker of the action.
Русский
Существует каноническое k-линейное отображение от свободного k-модуля на элементы G с коэффициентами в A к ядру (в k) отображения действия на коинвариантах; такое отображение задаётся ограничением нулевого дифференциала на порождающей подпросте Коинвариантов-ядро действия.
LaTeX
$$$\text{chains}_{1\to\mathrm{CoinvariantsKer}}(A): (G \to_0 A) \to \mathrm{Coinvariants.ker}(A.\rho)$$$
Lean4
/-- The 0th differential in the complex of inhomogeneous chains of a `G`-representation `A` as a
linear map into the `k`-submodule of `A` spanned by elements of the form
`ρ(g)(x) - x, g ∈ G, x ∈ A`. -/
def chains₁ToCoinvariantsKer : ModuleCat.of k (G →₀ A) ⟶ ModuleCat.of k (Coinvariants.ker A.ρ) :=
ModuleCat.ofHom <| (d₁₀ A).hom.codRestrict _ <| range_d₁₀_eq_coinvariantsKer A ▸ LinearMap.mem_range_self _
