English
There is a canonical Algebra structure on the pair (Ideal R, Submodule R A), turning Submodule R A into a module over Ideal R, compatible with Submodule operations.
Русский
Существует каноническая структура алгебры на паре (Ideal R, Submodule R A), превращающая Submodule R A в модуль над Ideal R и совместимую с операциями Submodule.
LaTeX
$$$\\text{Algebra}(\\operatorname{Ideal}(R), \\operatorname{Submodule}(R,A))$ with the given maps$$
Lean4
instance algebraIdeal : Algebra (Ideal R) (Submodule R A)
where
__ := moduleSubmodule
algebraMap :=
{ toFun := map (Algebra.linearMap R A)
map_one' := by rw [one_eq_span, map_span, Set.image_singleton, Algebra.linearMap_apply, map_one, one_eq_span]
map_mul' := (Submodule.map_mul · · <| Algebra.ofId R A)
map_zero' := map_bot _
map_add' := (map_sup · · _) }
commutes' I M := mul_comm_of_commute <| by rintro _ ⟨r, _, rfl⟩ a _; apply Algebra.commutes
smul_def' I
M :=
le_antisymm (smul_le.mpr fun r hr a ha ↦ by rw [Algebra.smul_def]; exact Submodule.mul_mem_mul ⟨r, hr, rfl⟩ ha)
(Submodule.mul_le.mpr <| by
rintro _ ⟨r, hr, rfl⟩ a ha; rw [Algebra.linearMap_apply, ← Algebra.smul_def]
exact Submodule.smul_mem_smul hr ha)
