English
The linear sum with lsingle acts as the identity, i.e., lsum S (lsingle) = id.
Русский
Линейная сумма с lsingle действует как тождество: lsum S (lsingle) = id.
LaTeX
$$$\\mathrm{lsum}\\; (\\mathrm{lsingle}) = \\mathrm{id}$$$
Lean4
/-- The `DFinsupp` version of `Finsupp.lsum`.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/
@[simps]
def lsum [Semiring S] [Module S N] [SMulCommClass R S N] : (∀ i, M i →ₗ[R] N) ≃ₗ[S] (Π₀ i, M i) →ₗ[R] N
where
toFun
F :=
{ toFun := sumAddHom fun i => (F i).toAddMonoidHom
map_add' := (DFinsupp.liftAddHom fun (i : ι) => (F i).toAddMonoidHom).map_add
map_smul' := fun c f => by
dsimp
apply DFinsupp.induction f
· rw [smul_zero, AddMonoidHom.map_zero, smul_zero]
· intro a b f _ _ hf
rw [smul_add, AddMonoidHom.map_add, AddMonoidHom.map_add, smul_add, hf, ← single_smul, sumAddHom_single,
sumAddHom_single, LinearMap.toAddMonoidHom_coe, LinearMap.map_smul] }
invFun F i := F.comp (lsingle i)
left_inv
F := by
ext
simp
right_inv
F := by
refine DFinsupp.lhom_ext' (fun i ↦ ?_)
ext
simp
map_add' F
G := by
refine DFinsupp.lhom_ext' (fun i ↦ ?_)
ext
simp
map_smul' c
F := by
refine DFinsupp.lhom_ext' (fun i ↦ ?_)
ext
simp
