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
Reinterpret a submodule
as an add_submonoid
.
- carrier : set M
- add_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- smul_mem' : ∀ (c : R) {x : M}, x ∈ self.carrier → c • x ∈ self.carrier
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 submodule
- submodule.has_sizeof_inst
- submodule.set_like
- submodule.add_submonoid_class
- submodule.add_subgroup_class
- submodule.has_bot
- submodule.inhabited'
- submodule.order_bot
- submodule.has_top
- submodule.order_top
- submodule.has_Inf
- submodule.has_inf
- submodule.complete_lattice
- submodule.unique
- submodule.unique'
- submodule.nontrivial
- submodule.is_compactly_generated
- submodule.is_modular_lattice
- submodule.has_quotient
- module.submodule.is_complemented
- submodule.pointwise_add_comm_monoid
- submodule.canonically_ordered_add_monoid
- submodule.pointwise_central_scalar
- submodule.has_one
- submodule.has_mul
- submodule.semiring
- submodule.comm_semiring
- submodule.module_set
- submodule.has_div
- ideal.is_coatomic
- ideal.nontrivial
- ideal.has_quotient
- submodule.has_scalar'
- ideal.has_mul
- ideal.no_zero_divisors
- ideal.comm_semiring
- submodule.module_submodule
- Module.has_coe
- is_semisimple_module.is_semisimple_submodule
- is_simple_module_of_simple
- submodule.has_coe
- lie_submodule.coe_submodule
- fractional_ideal.submodule.has_coe
- fractional_ideal.coe_to_fractional_ideal
- ideal.cancel_comm_monoid_with_zero
- ideal.wf_dvd_monoid
- ideal.unique_factorization_monoid
- ideal.normalization_monoid
- monoid_algebra.submodule.is_complemented
- valuation_ring.ideal.linear_order
Reinterpret a submodule
as an sub_mul_action
.
Equations
- submodule.set_like = {coe := submodule.carrier _inst_3, coe_injective' := _}
Equations
- submodule.add_submonoid_class = {to_add_mem_class := {add_mem := _}, zero_mem := _}
Copy of a submodule with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Equations
- p.add_comm_monoid = {add := has_add.add p.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul p.to_add_submonoid.to_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Equations
- p.module' = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul p.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
Note the add_submonoid
version of this lemma is called add_submonoid.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
Instances for ↥submodule.restrict_scalars
Even though p.restrict_scalars S
has type submodule S M
, it is still an R
-module.
Equations
- submodule.restrict_scalars.orig_module S R M p = p.module
restrict_scalars S
is an embedding of the lattice of R
-submodules into
the lattice of S
-submodules.
Equations
- submodule.restrict_scalars_embedding S R M = {to_embedding := {to_fun := submodule.restrict_scalars S _inst_7, inj' := _}, map_rel_iff' := _}
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.
Reinterpret a submodule as an additive subgroup.
Equations
- p.to_add_subgroup = {carrier := p.to_add_submonoid.carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}
Equations
- p.add_comm_group = {add := has_add.add p.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul p.to_add_subgroup.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg add_subgroup_class.has_neg, sub := add_comm_group.sub p.to_add_subgroup.to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul p.to_add_subgroup.to_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
A submodule of an ordered_add_comm_monoid
is an ordered_add_comm_monoid
.
Equations
A submodule of a linear_ordered_add_comm_monoid
is a linear_ordered_add_comm_monoid
.
Equations
A submodule of an ordered_cancel_add_comm_monoid
is an ordered_cancel_add_comm_monoid
.
Equations
A submodule of a linear_ordered_cancel_add_comm_monoid
is a
linear_ordered_cancel_add_comm_monoid
.
A submodule of an ordered_add_comm_group
is an ordered_add_comm_group
.
Equations
- S.to_ordered_add_comm_group = function.injective.ordered_add_comm_group coe _ _ _ _ _ _ _
A submodule of a linear_ordered_add_comm_group
is a
linear_ordered_add_comm_group
.