Linear maps involving submodules of a module #
In this file we define a number of linear maps involving submodules of a module.
Main declarations #
Submodule.subtype
: Embedding of a submodulep
to the ambient spaceM
as aSubmodule
.LinearMap.domRestrict
: The restriction of a semilinear mapf : M → M₂
to a submodulep ⊆ M
as a semilinear mapp → M₂
.LinearMap.restrict
: The restriction of a linear mapf : M → M₁
to a submodulep ⊆ M
andq ⊆ M₁
(ifq
contains the codomain).Submodule.inclusion
: the inclusionp ⊆ p'
of submodulesp
andp'
as a linear map.
Tags #
submodule, subspace, linear map
The natural R
-linear map from a submodule of an R
-module M
to M
.
Equations
Instances For
Alias of SMulMemClass.coe_subtype
.
Embedding of a submodule p
to the ambient space M
.
Equations
Instances For
Note the AddSubmonoid
version of this lemma is called AddSubmonoid.coe_finset_sum
.
The restriction of a linear map f : M → M₂
to a submodule p ⊆ M
gives a linear map
p → M₂
.
Equations
Instances For
A linear map f : M₂ → M
whose values lie in a submodule p ⊆ M
can be restricted to a
linear map M₂ → p.
See also LinearMap.codLift
.
Equations
Instances For
A linear map f : M → M₂
whose values lie in the image of an injective linear map
p : M₂' → M₂
admits a unique lift to a linear map M → M₂'
.
Equations
Instances For
Restrict domain and codomain of a linear map.
Equations
Instances For
Alternative version of domRestrict
as a linear map.