English
This asserts compatibility of the free module basis with the product in the group algebra: the action of the product gh on the nested single elements is the single (gh) with the same coefficient.
Русский
Это утверждает совместимость базиса свободного модуля с умножением в группе: действие gh на вложенные одинарные элементы даёт одинарный элемент (gh) с тем же коэффициентом.
LaTeX
$$$ free k G α g (single i (single h r)) = single i (single (g h) r) $$$
Lean4
/-- The free `k[G]`-module on a type `α` is isomorphic to the representation `free k G α`. -/
noncomputable def finsuppLEquivFreeAsModule : (α →₀ MonoidAlgebra k G) ≃ₗ[MonoidAlgebra k G] (free k G α).asModule :=
{ AddEquiv.refl _ with
map_smul' _
x :=
by
simp only [AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, AddEquiv.refl_apply, RingHom.id_apply]
induction x using Finsupp.induction with
| zero => simp only [smul_zero]
| single_add _ _ _ _ _ h =>
rw [smul_add, h]
change _ + asAlgebraHom _ _ _ = asAlgebraHom _ _ _
simp only [map_add, smul_single, smul_eq_mul, MonoidAlgebra.mul_def, asAlgebraHom_def, MonoidAlgebra.lift_apply]
simp [free, MonoidAlgebra, asModule, ofMulAction_def, mapDomain, smul_sum, single_sum] }
