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
SubmoduleClass S R M
says S
is a type of submodules s ≤ M
.
Note that only R
is marked as outParam
since M
is already supplied by the SetLike
class.
Instances
The carrier set is closed under scalar multiplication.
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 an SubMulAction
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Submodule.submoduleClass = SubmoduleClass.mk
Copy of a submodule with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Equations
- One or more equations did not get rendered due to their size.
A submodule of a Module
is a Module
.
Equations
- SubmoduleClass.toModule S' = Function.Injective.module R (AddSubmonoidClass.Subtype S') (_ : Function.Injective fun a => ↑a) (_ : ∀ (r : R) (x : { x // x ∈ S' }), ↑(r • x) = r • ↑x)
The natural R
-linear map from a submodule of an R
-module M
to M
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Submodule.zero p = { zero := { val := 0, property := (_ : 0 ∈ p) } }
Equations
- Submodule.inhabited p = { default := 0 }
Equations
- Submodule.smul p = { smul := fun c x => { val := c • ↑x, property := (_ : c • ↑x ∈ p) } }
Equations
- Submodule.addCommMonoid p = let src := AddSubmonoid.toAddCommMonoid p.toAddSubmonoid; AddCommMonoid.mk (_ : ∀ (a b : { x // x ∈ p.toAddSubmonoid }), a + b = b + a)
Equations
- One or more equations did not get rendered due to their size.
Equations
Note the AddSubmonoid
version of this lemma is called AddSubmonoid.coe_finset_sum
.
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.
Equations
- One or more equations did not get rendered due to their size.
Even though p.restrictScalars S
has type Submodule S M
, it is still an R
-module.
Equations
- Submodule.restrictScalars.origModule S R M p = inferInstance
restrictScalars S
is an embedding of the lattice of R
-submodules into
the lattice of S
-submodules.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Reinterpret a submodule as an additive subgroup.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Submodule.addCommGroup p = let src := AddSubgroup.toAddCommGroup (Submodule.toAddSubgroup p); AddCommGroup.mk (_ : ∀ (a b : { x // x ∈ Submodule.toAddSubgroup p }), a + b = b + a)
A submodule of an OrderedAddCommMonoid
is an OrderedAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
A submodule of a LinearOrderedAddCommMonoid
is a LinearOrderedAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
A submodule of an OrderedCancelAddCommMonoid
is an OrderedCancelAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
A submodule of a LinearOrderedCancelAddCommMonoid
is a
LinearOrderedCancelAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
A submodule of an OrderedAddCommGroup
is an OrderedAddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
A submodule of a LinearOrderedAddCommGroup
is a
LinearOrderedAddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.