English
For x ∈ Finsupp(G, k), the kernel of the leftRegular norm map equals the kernel of the linearCombination map: ker((leftRegular k G).norm) = ker(linearCombination k (fun x => 1)).
Русский
Для x ∈ Finsupp(G, k) ядро отображения нормы левого регулярного действия совпадает с ядром линейной комбинации по единице: ker((leftRegular k G).norm) = ker(linearCombination k (fun x => 1)).
LaTeX
$$$ \\ker\\big((leftRegular k G).norm\\big) = \\ker\\big( linearCombination k (\\text{fun } x => 1) \\big) $$$
Lean4
theorem smul_tprod_one_asModule (r : MonoidAlgebra k G) (x : V) (y : W) :
r • (show (ρV.tprod 1).asModule from x ⊗ₜ y) = (r • show ρV.asModule from x) ⊗ₜ y :=
by
change asAlgebraHom (ρV ⊗ 1) _ _ = asAlgebraHom ρV _ _ ⊗ₜ _
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply, LinearMap.finsupp_sum_apply,
LinearMap.smul_apply, TensorProduct.map_tmul, Module.End.one_apply]
simp only [Finsupp.sum, TensorProduct.sum_tmul]
rfl
