English
Let k be a commutative ring and G a group acting on a k-module A through a representation. Then the image of the first differential in the inhomogeneous chain complex, after passing to homology, equals the kernel of the G-action on coinvariants; equivalently, the image is the subgroup of coinvariants consisting of elements fixed by every group element.
Русский
Пусть k — коммутативное кольцо, G — группа, действующая на k-модуле A через представление. Тогда образ первого различителя в комплексe не гомологичных цепей, когда ограничен до собственных коинвариантов, совпадает с ядром действия группы на коинвариантах; эквивалентно, образ состоит из элементов, фиксированных для всех элементов группы.
LaTeX
$$$\operatorname{Im}\big((d_{10}A)^{\mathrm{hom}}\big) = \ker\big(A \mapsto \rho\big) \quad\text{on coinvariants}$$$
Lean4
theorem range_d₁₀_eq_coinvariantsKer : LinearMap.range (d₁₀ A).hom = Coinvariants.ker A.ρ :=
by
symm
apply Submodule.span_eq_of_le
· rintro _ ⟨x, rfl⟩
use single x.1⁻¹ x.2
simp [d₁₀]
· rintro x ⟨y, hy⟩
induction y using Finsupp.induction generalizing x with
| zero => simp [← hy]
| single_add _ _ _ _ _ h =>
simpa [← hy, add_sub_add_comm, sum_add_index, d₁₀_single (G := G)] using
Submodule.add_mem _ (Coinvariants.mem_ker_of_eq _ _ _ rfl) (h rfl)
