Submodules of a module #
In this file we define
-
Submodule R M
: a subset of aModule
M
that contains zero and is closed with respect to addition and scalar multiplication. -
Subspace k M
: an abbreviation forSubmodule
assuming thatk
is aField
.
Tags #
submodule, subspace, linear map
A submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.
Instances For
Reinterpret a Submodule
as a SubMulAction
.
Instances For
This can't be an instance because Lean wouldn't know how to find R
, but we can still use
this to manually derive Module
on specific types.
Instances For
The natural R
-linear map from a submodule of an R
-module M
to M
.
Instances For
Note the AddSubmonoid
version of this lemma is called AddSubmonoid.coe_finset_sum
.
Additive actions by Submodule
s #
These instances transfer the action by an element m : M
of an R
-module M
written as m +ᵥ a
onto the action by an element s : S
of a submodule S : Submodule R M
such that
s +ᵥ a = (s : M) +ᵥ a
.
These instances work particularly well in conjunction with AddGroup.toAddAction
, enabling
s +ᵥ m
as an alias for ↑s + m
.
The action by a submodule is the action by the underlying module.
V.restrict_scalars S
is the S
-submodule of the S
-module given by restriction of scalars,
corresponding to V
, an R
-submodule of the original R
-module.
Instances For
Even though p.restrictScalars S
has type Submodule S M
, it is still an R
-module.
restrictScalars S
is an embedding of the lattice of R
-submodules into
the lattice of S
-submodules.
Instances For
Turning p : Submodule R M
into an S
-submodule gives the same module structure
as turning it into a type and adding a module structure.
Instances For
Reinterpret a submodule as an additive subgroup.
Instances For
A submodule of an OrderedAddCommMonoid
is an OrderedAddCommMonoid
.
A submodule of a LinearOrderedAddCommMonoid
is a LinearOrderedAddCommMonoid
.
A submodule of an OrderedCancelAddCommMonoid
is an OrderedCancelAddCommMonoid
.
A submodule of a LinearOrderedCancelAddCommMonoid
is a
LinearOrderedCancelAddCommMonoid
.
A submodule of an OrderedAddCommGroup
is an OrderedAddCommGroup
.
A submodule of a LinearOrderedAddCommGroup
is a
LinearOrderedAddCommGroup
.