mapAlgHom — Mathlib

English

For an algebra hom f: A →ₐ[R] B, there is a natural AlgHom sending Submodule R A to Submodule R B by applying mapHom along f to submodules.

Русский

Для алгебра-гомоморфа f: A →ₐ[R] B существует естественный AlgHom, отправляющий Submodule R A в Submodule R B через применение mapHom к подмодулям.

LaTeX

$$$\\text{Submodule}(R,A) \\to_{\\text{Alg}} \\text{Submodule}(R,B)$ given by $I \\mapsto f(I)$$$

Lean4

/-- `Submonoid.map` as an `AlgHom`, when applied to an `AlgHom`. -/
@[simps!]
def mapAlgHom (f : A →ₐ[R] B) : Submodule R A →ₐ[Ideal R] Submodule R B
    where
  __ := mapHom f
  commutes' I := (map_comp _ _ I).symm.trans (congr_arg (map · I) <| LinearMap.ext f.commutes)

Похожие утверждения