submoduleImage — Mathlib

English

If N ⊆ O, then φ.submoduleImage N = range (φ ∘ inclusion h).

Русский

Если N ⊆ O, то φ.submoduleImage N = range (φ ∘ inclusion h).

LaTeX

$$$$ \varphi.\mathrm{submoduleImage }N = \operatorname{range}(\varphi \circ (\mathrm{inclusion}\; h)) $$$$

Lean4

/-- If `O` is a submodule of `M`, and `Φ : O →ₗ M'` is a linear map,
then `(ϕ : O →ₗ M').submoduleImage N` is `ϕ(N)` as a submodule of `M'` -/
def submoduleImage {M' : Type*} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} (ϕ : O →ₗ[R] M')
    (N : Submodule R M) : Submodule R M' :=
  (N.comap O.subtype).map ϕ

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