Theorems · Theorem · commutative algebra

Module.nonempty_basis_of_flat_of_finrank_eq

∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [Finite (MaximalSpectrum R)] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Finite R M] [Module.Flat R M] (n : ℕ),
  (∀ (P : MaximalSpectrum R), Module.finrank (R ⧸ P.asIdeal) (TensorProduct R (R ⧸ P.asIdeal) M) = n) →
    Nonempty (Module.Basis (Fin n) R M)

If M is a finite flat module over a commutative semilocal ring R that has the same rank n at every maximal ideal, then M is free of rank n.

Defined in

Mathlib.RingTheory.LocalRing.Module

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFiniteAddCommGroupModuleModule.FiniteModule.Flat