English
A subset of a ring R acts on Submodule R M by multiplication, giving a MulAction of Set R on Submodule R M with the unit and associativity properties transported from the ring action.
Русский
Подмножество кольца R действует на Submodule R M через умножение, задавая действие множества Set R на Submodule R M с единичным и ассоциативным свойствами, перенесёнными из кольцевого действия.
LaTeX
$$$\text{Set }R \curvearrowright \operatorname{Submodule} R M$ с ед., ассоц. свойствами.$$
Lean4
/-- A subset of a ring `R` has a multiplicative action on submodules of a module over `R`. -/
protected noncomputable def pointwiseSetMulAction [SMulCommClass R R M] : MulAction (Set R) (Submodule R M)
where
one_smul
x :=
show {(1 : R)} • x = x from
SetLike.ext fun m =>
(mem_singleton_set_smul _ _ _).trans
⟨by rintro ⟨_, h, rfl⟩; rwa [one_smul], fun h => ⟨m, h, (one_smul _ _).symm⟩⟩
mul_smul s t
x :=
le_antisymm (set_smul_le _ _ _ <| by rintro _ _ ⟨_, _, _, _, rfl⟩ _; rw [mul_smul]; aesop)
(set_smul_le _ _ _ fun r m hr hm ↦
by
have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩
obtain ⟨c, hc1, rfl⟩ := mem_set_smul _ _ _ |>.mp hm
rw [Finsupp.sum, AddSubmonoid.coe_finset_sum]
simp only [SetLike.val_smul, Finset.smul_sum, smul_smul]
exact Submodule.sum_mem _ fun r' hr' ↦ mem_set_smul_of_mem_mem (Set.mul_mem_mul hr (hc1 hr')) (c _).2)
