Linearly disjoint submodules

This file contains basics about linearly disjoint 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 and N are linearly disjoint (Submodule.LinearDisjoint M N or simply M.LinearDisjoint N), if the natural R-linear map M ⊗[R] N →ₗ[R] S (Submodule.mulMap M N) induced by the multiplication in S is injective.

The following is the first equivalent characterization of linear disjointness:

• Submodule.LinearDisjoint.linearIndependent_left_of_flat: 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) is injective.

• Submodule.LinearDisjoint.of_basis_left: conversely, if { m_i } is an R-basis of M, which is also N-linearly independent, then M and N are linearly disjoint.

Dually, we have:

• Submodule.LinearDisjoint.linearIndependent_right_of_flat: 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) is injective.

• Submodule.LinearDisjoint.of_basis_right: conversely, if { n_i } is an R-basis of N, which is also M-linearly independent, then M and N are linearly disjoint.

The following is the second equivalent characterization of linear disjointness:

• Submodule.LinearDisjoint.linearIndependent_mul_of_flat: 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.

• Submodule.LinearDisjoint.of_basis_mul: conversely, 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.

Other main results

• Submodule.LinearDisjoint.symm_of_commute, Submodule.linearDisjoint_comm_of_commute: linear disjointness is symmetric under some commutative conditions.

• Submodule.LinearDisjoint.map: linear disjointness is preserved by injective algebra homomorphisms.

• Submodule.linearDisjoint_op: linear disjointness 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: linear disjointness 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 of M and N are linearly disjoint, then M and N 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 of R in S 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 of R in S, 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: if M and N are linearly disjoint, if one of M and N is flat, then any two commutative elements contained in the intersection of M and N are not R-linearly independent (namely, their span is not R ^ 2). In particular, if any two elements in the intersection of M and N are commutative, then the rank of the intersection of M and N 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 with ha : a ∈ M ⊓ N), you may use LinearIndependent.of_comp and FinVec.map_eq (in Mathlib/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: if M and itself are linearly disjoint, if M is flat, if any two elements in M are commutative, then the rank of M is at most one.

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

Tags

linearly disjoint, linearly independent, tensor product

structure Submodule.LinearDisjoint {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M N : Submodule R S) : Prop

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)

theorem Submodule.linearDisjoint_iff {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M N : Submodule R S) : 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 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

• H.mulMap = (LinearEquiv.ofInjective (M.mulMap N) ⋯).trans (LinearEquiv.ofEq (LinearMap.range (M.mulMap N)) (M * N) ⋯)

@[simp]

theorem Submodule.LinearDisjoint.val_mulMap_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M 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 N : Submodule R S} [Subsingleton R] : M.LinearDisjoint N

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

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

Linear disjointness is preserved by taking multiplicative opposite.

theorem Submodule.LinearDisjoint.op {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M 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.

---

Linear disjointness 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 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.

---

Linear disjointness 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 N : Submodule R S} (H : M.LinearDisjoint N) (hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n) : N.LinearDisjoint M

Linear disjointness is symmetric if elements in the module commute.

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

Linear disjointness is symmetric if elements in the module commute.

theorem Submodule.LinearDisjoint.map {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M N : Submodule R S} (H : M.LinearDisjoint N) {T : Type w} [Semiring T] [Algebra R T] {F : Type u_1} [FunLike F S T] [AlgHomClass F R S T] (f : F) (hf : Function.Injective ⇑f) : (Submodule.map f M).LinearDisjoint (Submodule.map f N)

Linear disjointness is preserved by injective algebra homomorphisms.

theorem Submodule.LinearDisjoint.of_basis_left' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M 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 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 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.

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

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 N : Submodule R S) (H : ∀ M' ≤ M, M'.FG → M'.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 N : Submodule R S) (H : ∀ N' ≤ N, N'.FG → M.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 N : Submodule R S) (H : ∀ (M' N' : Submodule R S), M' ≤ M → N' ≤ N → M'.FG → N'.FG → M'.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 N : Submodule R S} (H : M.LinearDisjoint N) : N.LinearDisjoint M

Linear disjointness is symmetric in a commutative ring.

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

Linear disjointness 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 N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R ↥N] {ι : Type u_1} {m : ι → ↥M} (hm : LinearIndependent R m) : LinearMap.ker (Submodule.mulLeftMap N 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 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 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 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 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 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 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 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_j } 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 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 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 N : Submodule R S} (H : M.LinearDisjoint N) {M' 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 N : Submodule R S} (H : M.LinearDisjoint N) {M' 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 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 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 N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] [Module.Flat R ↥M] (a b : ↥(M ⊓ N)) (hc : Commute ↑a ↑b) : ¬LinearIndependent R ![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 N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] [Module.Flat R ↥N] (a b : ↥(M ⊓ N)) (hc : Commute ↑a ↑b) : ¬LinearIndependent R ![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 N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] (hf : Module.Flat R ↥M ∨ Module.Flat R ↥N) (a b : ↥(M ⊓ N)) (hc : Commute ↑a ↑b) : ¬LinearIndependent R ![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 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 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 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 N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] [Module.Flat R ↥M] (a b : ↥(M ⊓ N)) : ¬LinearIndependent R ![a, b]

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 N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] [Module.Flat R ↥N] (a b : ↥(M ⊓ N)) : ¬LinearIndependent R ![a, b]

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 N : Submodule R S} (H : M.LinearDisjoint N) [Nontrivial R] (hf : Module.Flat R ↥M ∨ Module.Flat R ↥N) (a b : ↥(M ⊓ N)) : ¬LinearIndependent R ![a, b]

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