map
and comap
for Submodule
s #
Main declarations #
Submodule.map
: The pushforward of a submodulep ⊆ M
byf : M → M₂
Submodule.comap
: The pullback of a submodulep ⊆ M₂
alongf : M → M₂
Submodule.giMapComap
:map f
andcomap f
form aGaloisInsertion
whenf
is surjective.Submodule.gciMapComap
:map f
andcomap f
form aGaloisCoinsertion
whenf
is injective.
Tags #
submodule, subspace, linear map, pushforward, pullback
The pushforward of a submodule p ⊆ M
by f : M → M₂
Equations
Instances For
The pushforward of a submodule by an injective linear map is
linearly equivalent to the original submodule. See also LinearEquiv.submoduleMap
for a
computable version when f
has an explicit inverse.
Equations
Instances For
The pullback of a submodule p ⊆ M₂
along f : M → M₂
Equations
Instances For
For any R
submodules p
and q
, p ⊓ q
as a submodule of q
.
Equations
Instances For
If p ≤ q
, then p
as a subgroup of q
is isomorphic to p
.
Equations
Instances For
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Equations
Instances For
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Equations
Instances For
A linear isomorphism induces an order isomorphism of submodules.
Equations
Instances For
A linear isomorphism induces an order isomorphism of submodules.
Equations
Instances For
The infimum of a family of invariant submodule of an endomorphism is also an invariant submodule.
Given modules M
, M₂
over a commutative ring, together with submodules p ⊆ M
, q ⊆ M₂
,
the set of maps $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \}$ is a submodule of Hom(M, M₂)
.
Equations
Instances For
The LinearMap
from the preimage of a submodule to itself.
This is the linear version of AddMonoidHom.addSubmonoidComap
and AddMonoidHom.addSubgroupComap
.
Equations
Instances For
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
.
Equations
Instances For
Linear equivalences #
A linear equivalence of two modules restricts to a linear equivalence from any submodule
p
of the domain onto the image of that submodule.
This is the linear version of AddEquiv.submonoidMap
and AddEquiv.subgroupMap
.
This is LinearEquiv.ofSubmodule'
but with map
on the right instead of comap
on the left.