Linearly disjoint of submodules #
This file contains basics about the linearly disjoint of submodules.
Mathematical background #
We adapt the definitions in https://en.wikipedia.org/wiki/Linearly_disjoint.
Let R
be a commutative ring, S
be an R
-algebra (not necessarily commutative).
Let M
and N
be R
-submodules in S
(Submodule R S
).
M
andN
are linearly disjoint (Submodule.LinearDisjoint M N
or simplyM.LinearDisjoint N
), if the naturalR
-linear mapM ⊗[R] N →ₗ[R] S
(Submodule.mulMap M N
) induced by the multiplication inS
is injective.
The following is the first equivalent characterization of linearly disjointness:
Submodule.LinearDisjoint.linearIndependent_left_of_flat
: ifM
andN
are linearly disjoint, ifN
is a flatR
-module, then for any family ofR
-linearly independent elements{ m_i }
ofM
, they are alsoN
-linearly independent, in the sense that theR
-linear map fromι →₀ N
toS
which maps{ n_i }
to the sum ofm_i * n_i
(Submodule.mulLeftMap N m
) is injective.Submodule.LinearDisjoint.of_basis_left
: conversely, if{ m_i }
is anR
-basis ofM
, which is alsoN
-linearly independent, thenM
andN
are linearly disjoint.
Dually, we have:
Submodule.LinearDisjoint.linearIndependent_right_of_flat
: ifM
andN
are linearly disjoint, ifM
is a flatR
-module, then for any family ofR
-linearly independent elements{ n_i }
ofN
, they are alsoM
-linearly independent, in the sense that theR
-linear map fromι →₀ M
toS
which maps{ m_i }
to the sum ofm_i * n_i
(Submodule.mulRightMap M n
) is injective.Submodule.LinearDisjoint.of_basis_right
: conversely, if{ n_i }
is anR
-basis ofN
, which is alsoM
-linearly independent, thenM
andN
are linearly disjoint.
The following is the second equivalent characterization of linearly disjointness:
Submodule.LinearDisjoint.linearIndependent_mul_of_flat
: ifM
andN
are linearly disjoint, if one ofM
andN
is flat, then for any family ofR
-linearly independent elements{ m_i }
ofM
, and any family ofR
-linearly independent elements{ n_j }
ofN
, the family{ m_i * n_j }
inS
is alsoR
-linearly independent.Submodule.LinearDisjoint.of_basis_mul
: conversely, if{ m_i }
is anR
-basis ofM
, if{ n_i }
is anR
-basis ofN
, such that the family{ m_i * n_j }
inS
isR
-linearly independent, thenM
andN
are linearly disjoint.
Other main results #
Submodule.LinearDisjoint.symm_of_commute
,Submodule.linearDisjoint_symm_of_commute
: linearly disjoint is symmetric under some commutative conditions.Submodule.linearDisjoint_op
: linearly disjoint is preserved by taking multiplicative opposite.Submodule.LinearDisjoint.of_le_left_of_flat
,Submodule.LinearDisjoint.of_le_right_of_flat
,Submodule.LinearDisjoint.of_le_of_flat_left
,Submodule.LinearDisjoint.of_le_of_flat_right
: linearly disjoint is preserved by taking submodules under some flatness conditions.Submodule.LinearDisjoint.of_linearDisjoint_fg_left
,Submodule.LinearDisjoint.of_linearDisjoint_fg_right
,Submodule.LinearDisjoint.of_linearDisjoint_fg
: conversely, if any finitely generated submodules ofM
andN
are linearly disjoint, thenM
andN
themselves are linearly disjoint.Submodule.LinearDisjoint.bot_left
,Submodule.LinearDisjoint.bot_right
: the zero module is linearly disjoint with any other submodules.Submodule.LinearDisjoint.one_left
,Submodule.LinearDisjoint.one_right
: the image ofR
inS
is linearly disjoint with any other submodules.Submodule.LinearDisjoint.of_left_le_one_of_flat
,Submodule.LinearDisjoint.of_right_le_one_of_flat
: if a submodule is contained in the image ofR
inS
, then it is linearly disjoint with any other submodules, under some flatness conditions.Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat
,Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat
: ifM
andN
are linearly disjoint, if one ofM
andN
is flat, then any two commutative elements contained in the intersection ofM
andN
are notR
-linearly independent (namely, their span is notR ^ 2
). In particular, if any two elements in the intersection ofM
andN
are commutative, then the rank of the intersection ofM
andN
is at most one.These results are stated using bundled version (i.e.
a : ↥(M ⊓ N)
). If you want a not bundled version (i.e.a : S
withha : a ∈ M ⊓ N
), you may useLinearIndependent.of_comp
andFinVec.map_eq
(inMathlib/Data/Fin/Tuple/Reflection.lean
), see the following code snippet:have h := H.not_linearIndependent_pair_of_commute_of_flat hf ⟨a, ha⟩ ⟨b, hb⟩ hc contrapose! h refine .of_comp (M ⊓ N).subtype ?_ convert h exact (FinVec.map_eq _ _).symm
Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self
: ifM
and itself are linearly disjoint, ifM
is flat, if any two elements inM
are commutative, then the rank ofM
is at most one.
The results with name containing "of_commute" also have corresponding specified versions
assuming S
is commutative.
Tags #
linearly disjoint, linearly independent, tensor product
Two submodules M
and N
in an algebra S
over R
are linearly disjoint if the natural map
M ⊗[R] N →ₗ[R] S
induced by multiplication in S
is injective.
- injective : Function.Injective ⇑(M.mulMap N)
Instances For
If M
and N
are linearly disjoint submodules, then there is the natural isomorphism
M ⊗[R] N ≃ₗ[R] M * N
induced by multiplication in S
.
Equations
- H.mulMap = (LinearEquiv.ofInjective (M.mulMap N) ⋯).trans (LinearEquiv.ofEq (LinearMap.range (M.mulMap N)) (M * N) ⋯)
Instances For
Linearly disjoint is preserved by taking multiplicative opposite.
Alias of the reverse direction of Submodule.linearDisjoint_op
.
Linearly disjoint is preserved by taking multiplicative opposite.
Alias of the forward direction of Submodule.linearDisjoint_op
.
Linearly disjoint is preserved by taking multiplicative opposite.
Linearly disjoint is symmetric if elements in the module commute.
Linearly disjoint is symmetric if elements in the module commute.
If { m_i }
is an R
-basis of M
, which is also N
-linearly independent
(in this result it is stated as Submodule.mulLeftMap
is injective),
then M
and N
are linearly disjoint.
If { n_i }
is an R
-basis of N
, which is also M
-linearly independent
(in this result it is stated as Submodule.mulRightMap
is injective),
then M
and N
are linearly disjoint.
If { m_i }
is an R
-basis of M
, if { n_i }
is an R
-basis of N
,
such that the family { m_i * n_j }
in S
is R
-linearly independent
(in this result it is stated as the relevant Finsupp.linearCombination
is injective),
then M
and N
are linearly disjoint.
The zero module is linearly disjoint with any other submodules.
The zero module is linearly disjoint with any other submodules.
The image of R
in S
is linearly disjoint with any other submodules.
The image of R
in S
is linearly disjoint with any other submodules.
If for any finitely generated submodules M'
of M
, M'
and N
are linearly disjoint,
then M
and N
themselves are linearly disjoint.
If for any finitely generated submodules N'
of N
, M
and N'
are linearly disjoint,
then M
and N
themselves are linearly disjoint.
If for any finitely generated submodules M'
and N'
of M
and N
, respectively,
M'
and N'
are linearly disjoint, then M
and N
themselves are linearly disjoint.
Linearly disjoint is symmetric in a commutative ring.
Linearly disjoint is symmetric in a commutative ring.
If M
and N
are linearly disjoint, if N
is a flat R
-module, then for any family of
R
-linearly independent elements { m_i }
of M
, they are also N
-linearly independent,
in the sense that the R
-linear map from ι →₀ N
to S
which maps { n_i }
to the sum of m_i * n_i
(Submodule.mulLeftMap N m
) has trivial kernel.
If { m_i }
is an R
-basis of M
, which is also N
-linearly independent,
then M
and N
are linearly disjoint.
If M
and N
are linearly disjoint, if M
is a flat R
-module, then for any family of
R
-linearly independent elements { n_i }
of N
, they are also M
-linearly independent,
in the sense that the R
-linear map from ι →₀ M
to S
which maps { m_i }
to the sum of m_i * n_i
(Submodule.mulRightMap M n
) has trivial kernel.
If { n_i }
is an R
-basis of N
, which is also M
-linearly independent,
then M
and N
are linearly disjoint.
If M
and N
are linearly disjoint, if M
is flat, then for any family of
R
-linearly independent elements { m_i }
of M
, and any family of
R
-linearly independent elements { n_j }
of N
, the family { m_i * n_j }
in S
is
also R
-linearly independent.
If M
and N
are linearly disjoint, if N
is flat, then for any family of
R
-linearly independent elements { m_i }
of M
, and any family of
R
-linearly independent elements { n_j }
of N
, the family { m_i * n_j }
in S
is
also R
-linearly independent.
If M
and N
are linearly disjoint, if one of M
and N
is flat, then for any family of
R
-linearly independent elements { m_i }
of M
, and any family of
R
-linearly independent elements { n_j }
of N
, the family { m_i * n_j }
in S
is
also R
-linearly independent.
If { m_i }
is an R
-basis of M
, if { n_i }
is an R
-basis of N
,
such that the family { m_i * n_j }
in S
is R
-linearly independent,
then M
and N
are linearly disjoint.
If M
and N
are linearly disjoint, if N
is flat, then for any submodule M'
of M
,
M'
and N
are also linearly disjoint.
If M
and N
are linearly disjoint, if M
is flat, then for any submodule N'
of N
,
M
and N'
are also linearly disjoint.
If M
and N
are linearly disjoint, M'
and N'
are submodules of M
and N
,
respectively, such that N
and M'
are flat, then M'
and N'
are also linearly disjoint.
If M
and N
are linearly disjoint, M'
and N'
are submodules of M
and N
,
respectively, such that M
and N'
are flat, then M'
and N'
are also linearly disjoint.
If N
is flat, M
is contained in i(R)
, where i : R → S
is the structure map,
then M
and N
are linearly disjoint.
If M
is flat, N
is contained in i(R)
, where i : R → S
is the structure map,
then M
and N
are linearly disjoint.
If M
and N
are linearly disjoint, if M
is flat, then any two commutative
elements of ↥(M ⊓ N)
are not R
-linearly independent (namely, their span is not R ^ 2
).
If M
and N
are linearly disjoint, if N
is flat, then any two commutative
elements of ↥(M ⊓ N)
are not R
-linearly independent (namely, their span is not R ^ 2
).
If M
and N
are linearly disjoint, if one of M
and N
is flat, then any two commutative
elements of ↥(M ⊓ N)
are not R
-linearly independent (namely, their span is not R ^ 2
).
If M
and N
are linearly disjoint, if one of M
and N
is flat,
if any two elements of ↥(M ⊓ N)
are commutative, then the rank of ↥(M ⊓ N)
is at most one.
If M
and N
are linearly disjoint, if M
is flat,
if any two elements of ↥(M ⊓ N)
are commutative, then the rank of ↥(M ⊓ N)
is at most one.
If M
and N
are linearly disjoint, if N
is flat,
if any two elements of ↥(M ⊓ N)
are commutative, then the rank of ↥(M ⊓ N)
is at most one.
If M
and itself are linearly disjoint, if M
is flat,
if any two elements of M
are commutative, then the rank of M
is at most one.
The Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left
for commutative rings.
The Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right
for commutative rings.
The Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat
for commutative rings.
The Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat
for commutative rings.
The Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left
for commutative rings.
The Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right
for commutative rings.
The Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self
for commutative rings.