English
For the left regular representation ρ on k[G], the coinvariants ker equals the kernel of the norm-related map, identifying it with a standard subspace.
Русский
Для левого регулярного представления ρ на k[G] ядро коинвариант равно ядру соответствующей нормы, что идентифицирует его с стандартным подпространством.
LaTeX
$$$ \operatorname{Coinvariants.ker}(\mathrm{leftRegular}_{k,G}) = \ker\bigl( \mathrm{leftRegular}_{k,G} \text{-norm map} \bigr) $$$
Lean4
theorem coinvariantsKer_leftRegular_eq_ker :
Coinvariants.ker (Representation.leftRegular k G) = LinearMap.ker (linearCombination k (fun _ => (1 : k))) :=
by
refine le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_
· rintro x ⟨⟨g, y⟩, rfl⟩
simpa [linearCombination, sub_eq_zero, sum_fintype] using
Finset.sum_bijective _ (Group.mulLeft_bijective g⁻¹) (by aesop) (by aesop)
· have : x = x.sum (fun g r => single g r - single 1 r) :=
by
ext g
by_cases hg : g = 1
· simp_all [linearCombination, sum_apply']
· simp_all [sum_apply']
rw [this]
exact Submodule.finsuppSum_mem _ _ _ _ fun g _ => Coinvariants.mem_ker_of_eq g (single 1 (x g)) _ (by simp)
