Documentation

Mathlib.LinearAlgebra.LinearDisjoint

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).

The following is the first equivalent characterization of linearly disjointness:

Dually, we have:

The following is the second equivalent characterization of linearly disjointness:

Other main results #

The results with name containing "of_commute" also have corresponding specified versions assuming S is commutative.

Tags #

linearly disjoint, linearly independent, tensor product

theorem Submodule.linearDisjoint_iff {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) :
M.LinearDisjoint N Function.Injective (M.mulMap N)
structure Submodule.LinearDisjoint {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) :

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.

Instances For
    theorem Submodule.LinearDisjoint.injective {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (self : M.LinearDisjoint N) :
    Function.Injective (M.mulMap N)
    def Submodule.LinearDisjoint.mulMap {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) :
    TensorProduct R M N ≃ₗ[R] (M * N)

    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
    Instances For
      @[simp]
      theorem Submodule.LinearDisjoint.val_mulMap_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) (m : M) (n : N) :
      (H.mulMap (m ⊗ₜ[R] n)) = m * n
      theorem Submodule.LinearDisjoint.of_subsingleton {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} [Subsingleton R] :
      M.LinearDisjoint N
      theorem Submodule.linearDisjoint_op {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} :
      M.LinearDisjoint N (Submodule.equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (Submodule.equivOpposite.symm (MulOpposite.op M))

      Linearly disjoint is preserved by taking multiplicative opposite.

      theorem Submodule.LinearDisjoint.of_op {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} :
      (Submodule.equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (Submodule.equivOpposite.symm (MulOpposite.op M))M.LinearDisjoint N

      Alias of the reverse direction of Submodule.linearDisjoint_op.


      Linearly disjoint is preserved by taking multiplicative opposite.

      theorem Submodule.LinearDisjoint.op {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} :
      M.LinearDisjoint N(Submodule.equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (Submodule.equivOpposite.symm (MulOpposite.op M))

      Alias of the forward direction of Submodule.linearDisjoint_op.


      Linearly disjoint is preserved by taking multiplicative opposite.

      theorem Submodule.LinearDisjoint.symm_of_commute {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) (hc : ∀ (m : M) (n : N), Commute m n) :
      N.LinearDisjoint M

      Linearly disjoint is symmetric if elements in the module commute.

      theorem Submodule.linearDisjoint_symm_of_commute {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (hc : ∀ (m : M) (n : N), Commute m n) :
      M.LinearDisjoint N N.LinearDisjoint M

      Linearly disjoint is symmetric if elements in the module commute.

      theorem Submodule.LinearDisjoint.of_basis_left' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) {ι : Type u_1} (m : Basis ι R M) (H : Function.Injective (Submodule.mulLeftMap N m)) :
      M.LinearDisjoint N

      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.

      theorem Submodule.LinearDisjoint.of_basis_right' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) {ι : Type u_1} (n : Basis ι R N) (H : Function.Injective (M.mulRightMap n)) :
      M.LinearDisjoint N

      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.

      theorem Submodule.LinearDisjoint.of_basis_mul' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) {κ : Type u_1} {ι : Type u_2} (m : Basis κ R M) (n : Basis ι R N) (H : Function.Injective (Finsupp.linearCombination R fun (i : κ × ι) => (m i.1) * (n i.2))) :
      M.LinearDisjoint N

      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.

      theorem Submodule.LinearDisjoint.bot_left {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (N : Submodule R S) :
      .LinearDisjoint N

      The zero module is linearly disjoint with any other submodules.

      theorem Submodule.LinearDisjoint.bot_right {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) :
      M.LinearDisjoint

      The zero module is linearly disjoint with any other submodules.

      The image of R in S is linearly disjoint with any other submodules.

      theorem Submodule.LinearDisjoint.one_right {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) :
      M.LinearDisjoint 1

      The image of R in S is linearly disjoint with any other submodules.

      theorem Submodule.LinearDisjoint.of_linearDisjoint_fg_left {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) (H : M'M, M'.FGM'.LinearDisjoint N) :
      M.LinearDisjoint N

      If for any finitely generated submodules M' of M, M' and N are linearly disjoint, then M and N themselves are linearly disjoint.

      theorem Submodule.LinearDisjoint.of_linearDisjoint_fg_right {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) (H : N'N, N'.FGM.LinearDisjoint N') :
      M.LinearDisjoint N

      If for any finitely generated submodules N' of N, M and N' are linearly disjoint, then M and N themselves are linearly disjoint.

      theorem Submodule.LinearDisjoint.of_linearDisjoint_fg {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) (H : ∀ (M' N' : Submodule R S), M' MN' NM'.FGN'.FGM'.LinearDisjoint N') :
      M.LinearDisjoint N

      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.

      theorem Submodule.LinearDisjoint.symm {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) :
      N.LinearDisjoint M

      Linearly disjoint is symmetric in a commutative ring.

      theorem Submodule.linearDisjoint_symm {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} :
      M.LinearDisjoint N N.LinearDisjoint M

      Linearly disjoint is symmetric in a commutative ring.

      theorem Submodule.LinearDisjoint.linearIndependent_left_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R N] {ι : Type u_1} {m : ιM} (hm : LinearIndependent R m) :

      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.

      theorem Submodule.LinearDisjoint.of_basis_left {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) {ι : Type u_1} (m : Basis ι R M) (H : LinearMap.ker (Submodule.mulLeftMap N m) = ) :
      M.LinearDisjoint N

      If { m_i } is an R-basis of M, which is also N-linearly independent, then M and N are linearly disjoint.

      theorem Submodule.LinearDisjoint.linearIndependent_right_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R M] {ι : Type u_1} {n : ιN} (hn : LinearIndependent R n) :
      LinearMap.ker (M.mulRightMap n) =

      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.

      theorem Submodule.LinearDisjoint.of_basis_right {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) {ι : Type u_1} (n : Basis ι R N) (H : LinearMap.ker (M.mulRightMap n) = ) :
      M.LinearDisjoint N

      If { n_i } is an R-basis of N, which is also M-linearly independent, then M and N are linearly disjoint.

      theorem Submodule.LinearDisjoint.linearIndependent_mul_of_flat_left {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R M] {κ : Type u_1} {ι : Type u_2} {m : κM} {n : ιN} (hm : LinearIndependent R m) (hn : LinearIndependent R n) :
      LinearIndependent R fun (i : κ × ι) => (m i.1) * (n i.2)

      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.

      theorem Submodule.LinearDisjoint.linearIndependent_mul_of_flat_right {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R N] {κ : Type u_1} {ι : Type u_2} {m : κM} {n : ιN} (hm : LinearIndependent R m) (hn : LinearIndependent R n) :
      LinearIndependent R fun (i : κ × ι) => (m i.1) * (n i.2)

      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.

      theorem Submodule.LinearDisjoint.linearIndependent_mul_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) (hf : Module.Flat R M Module.Flat R N) {κ : Type u_1} {ι : Type u_2} {m : κM} {n : ιN} (hm : LinearIndependent R m) (hn : LinearIndependent R n) :
      LinearIndependent R fun (i : κ × ι) => (m i.1) * (n i.2)

      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.

      theorem Submodule.LinearDisjoint.of_basis_mul {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) {κ : Type u_1} {ι : Type u_2} (m : Basis κ R M) (n : Basis ι R N) (H : LinearIndependent R fun (i : κ × ι) => (m i.1) * (n i.2)) :
      M.LinearDisjoint N

      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.

      theorem Submodule.LinearDisjoint.of_le_left_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) {M' : Submodule R S} (h : M' M) [Module.Flat R N] :
      M'.LinearDisjoint N

      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.

      theorem Submodule.LinearDisjoint.of_le_right_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) {N' : Submodule R S} (h : N' N) [Module.Flat R M] :
      M.LinearDisjoint N'

      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.

      theorem Submodule.LinearDisjoint.of_le_of_flat_right {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) {M' : Submodule R S} {N' : Submodule R S} (hm : M' M) (hn : N' N) [Module.Flat R N] [Module.Flat R M'] :
      M'.LinearDisjoint N'

      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.

      theorem Submodule.LinearDisjoint.of_le_of_flat_left {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) {M' : Submodule R S} {N' : Submodule R S} (hm : M' M) (hn : N' N) [Module.Flat R M] [Module.Flat R N'] :
      M'.LinearDisjoint N'

      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.

      theorem Submodule.LinearDisjoint.of_left_le_one_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) (h : M 1) [Module.Flat R N] :
      M.LinearDisjoint N

      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.

      theorem Submodule.LinearDisjoint.of_right_le_one_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) (h : N 1) [Module.Flat R M] :
      M.LinearDisjoint N

      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.

      theorem Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] [Module.Flat R M] (a : (M N)) (b : (M N)) (hc : Commute a b) :

      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).

      theorem Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] [Module.Flat R N] (a : (M N)) (b : (M N)) (hc : Commute a b) :

      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).

      theorem Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] (hf : Module.Flat R M Module.Flat R N) (a : (M N)) (b : (M N)) (hc : Commute a b) :

      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).

      theorem Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) (hf : Module.Flat R M Module.Flat R N) (hc : ∀ (m n : (M N)), Commute m n) :
      Module.rank R (M N) 1

      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.

      theorem Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R M] (hc : ∀ (m n : (M N)), Commute m n) :
      Module.rank R (M N) 1

      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.

      theorem Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R N] (hc : ∀ (m n : (M N)), Commute m n) :
      Module.rank R (M N) 1

      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.

      theorem Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M : Submodule R S} (H : M.LinearDisjoint M) [Module.Flat R M] (hc : ∀ (m n : M), Commute m n) :
      Module.rank R M 1

      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.

      theorem Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_left {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] [Module.Flat R M] (a : (M N)) (b : (M N)) :

      The Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left for commutative rings.

      theorem Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_right {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] [Module.Flat R N] (a : (M N)) (b : (M N)) :

      The Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right for commutative rings.

      theorem Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] (hf : Module.Flat R M Module.Flat R N) (a : (M N)) (b : (M N)) :

      The Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat for commutative rings.

      theorem Submodule.LinearDisjoint.rank_inf_le_one_of_flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) (hf : Module.Flat R M Module.Flat R N) :
      Module.rank R (M N) 1

      The Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat for commutative rings.

      theorem Submodule.LinearDisjoint.rank_inf_le_one_of_flat_left {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R M] :
      Module.rank R (M N) 1

      The Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left for commutative rings.

      theorem Submodule.LinearDisjoint.rank_inf_le_one_of_flat_right {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R N] :
      Module.rank R (M N) 1

      The Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right for commutative rings.

      theorem Submodule.LinearDisjoint.rank_le_one_of_flat_of_self {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Submodule R S} (H : M.LinearDisjoint M) [Module.Flat R M] :
      Module.rank R M 1

      The Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self for commutative rings.