Submodules of a module #
In this file we define
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.
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.
These instances transfer the action by an element
m : M of an
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
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,
R-submodule of the original
restrictScalars S is an embedding of the lattice of
the lattice of
p : Submodule R M into an
S-submodule gives the same module structure
as turning it into a type and adding a module structure.