English
Given an algebra homomorphism f: A →ₐ[R] A', there is a natural ring homomorphism from Submodule R A to Submodule R A' sending a submodule M to its image under f.
Русский
Дано алгебраическое гомоморфизм f: A →ₐ[R] A'; существует естественная кольцевая гомоморфизм Submodule R A → Submodule R A', отправляющий подмодуль M в образ M под действием f.
LaTeX
$$$\mathrm{mapHom}(f) : \mathrm{Submodule}(R,A) \to^+_* \mathrm{Submodule}(R,A') ,\quad \mathrm{mapHom}(f)(M) = \mathrm{Submodule.map}(f^{\mathrm{toLinearMap}})(M).$$$
Lean4
/-- `Submonoid.map` as a `RingHom`, when applied to an `AlgHom`. -/
@[simps]
def mapHom {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : Submodule R A →+* Submodule R A'
where
toFun := map f.toLinearMap
map_zero' := Submodule.map_bot _
map_add' := (Submodule.map_sup · · _)
map_one' := Submodule.map_one _
map_mul' := (Submodule.map_mul · · _)
