Theorems · Theorem · commutative algebra

Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ [Nontrivial R],
      Module.Flat R ↥M ∨ Module.Flat R ↥N → ∀ (a b : ↥(M ⊓ N)), 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).

Defined in

Mathlib.LinearAlgebra.LinearDisjoint

Cited by

2 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebraNontrivial