English
The set-smul of a submodule N by sR ⊆ R is equal to the image of a certain linear map from a finitely supported combination of elements of N, i.e., sR • N = Submodule.map (N.subtype . .) (Finsupp.supported N R sR).
Русский
Образ множества Smul над подмодулем N равен образу определенной линейной карты из конечной комбинации элементов N, то есть sR • N = Submodule.map ... .
LaTeX
$$$ s_R \cdot N = \operatorname{Submodule}.map (N.{\text{subtype}} \circ \text{lsum}...) (\operatorname{Finsupp}.supported (N) (R) s_R) $$$
Lean4
theorem set_smul_eq_map [SMulCommClass R R N] :
sR • N =
Submodule.map (N.subtype.comp (Finsupp.lsum R <| DistribMulAction.toLinearMap _ _)) (Finsupp.supported N R sR) :=
by
classical
apply set_smul_eq_of_le
· intro r n hr hn
exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩
· intro x hx
obtain ⟨c, hc, rfl⟩ := hx
simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]
rw [AddSubmonoid.coe_finset_sum]
refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
· rintro r hr
rw [mem_set_smul_def, Submodule.mem_sInf]
rintro p hp
exact hp (hc hr) (c r).2
· ext x : 1
simp only [Set.mem_iInter, SetLike.mem_coe]
fconstructor
· refine fun h ↦ h fun r n hr hn ↦ ?_
rw [mem_set_smul_def, mem_sInf]
exact fun p hp ↦ hp hr hn
· simp_all
