submoduleMap — Mathlib

English

For a linear map f and a submodule p, the induced map f.submoduleMap p is surjective onto p.map f.

Русский

Для линейного отображения f и подмодуля p соответствующее отображение f.submoduleMap p совпадает с сюръективным на p.map f.

LaTeX

$$$ Surjective (f.submoduleMap p) $$$

Lean4

/-- A linear map between two modules restricts to a linear map from any submodule p of the
domain onto the image of that submodule.

This is the linear version of `AddMonoidHom.addSubmonoidMap` and `AddMonoidHom.addSubgroupMap`. -/
def submoduleMap (f : M →ₗ[R] M₁) (p : Submodule R M) : p →ₗ[R] p.map f :=
  f.restrict fun x hx ↦ Submodule.mem_map.mpr ⟨x, hx, rfl⟩

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