submoduleComap — Mathlib

English

There is a canonical linear map from q.comap f to q obtained by restricting f to the domain q.

Русский

Существует каноничное линейное отображение из q.comap f в q, получаемое ограничением f к области определения q.

LaTeX

$$$\\text{def }\\text{submoduleComap}(f,q) : q.comap f \\to q$$$

Lean4

/-- The `LinearMap` from the preimage of a submodule to itself.

This is the linear version of `AddMonoidHom.addSubmonoidComap`
and `AddMonoidHom.addSubgroupComap`. -/
@[simps!]
def submoduleComap (f : M →ₗ[R] M₁) (q : Submodule R M₁) : q.comap f →ₗ[R] q :=
  f.restrict fun _ ↦ Submodule.mem_comap.1

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