Generic freeness

Let A be a reduced Noetherian ring, B a finitely generated A-algebra and M a finite B-module. Then M, viewed as an A-module, is free at every prime of an open neighbourhood of the minimal primes of A; in particular the interior of its free locus is dense in Spec A. Over a Noetherian domain this says that M_q is free over A_q for every prime q in some nonempty basic open set.

The module M is usually not finitely generated over A, so openness of the free locus of a finitely presented module does not apply directly. Instead, the proof is by induction on the number of generators of B. A finite module M over a polynomial ring R[X], with generators m₁, …, mₜ, is filtered by the R-submodules F j spanned by the X ^ i • mₖ with i < j. Each subquotient F (j + 1) ⧸ F j is a quotient of Rᵗ by the submodule K j of coefficient vectors c with ∑ cₖ • X ^ j • mₖ ∈ F j. Multiplication by X shows that K j increases with j, so by Noetherianity only finitely many distinct subquotients occur. The induction hypothesis makes each of them free on an open neighbourhood of the minimal primes, and the finite intersection of these sets is an open neighbourhood on which every subquotient, hence M itself, is free.

Main declarations

• Module.freeLocus_mem_nhds_of_mem_minimalPrimes: a finite module over a finitely generated algebra over a reduced Noetherian ring is free over that ring near every minimal prime.
• Module.dense_interior_freeLocus_of_finiteType: such a module is free over the base on a dense open subset of its spectrum.

References

• H. Matsumura, Commutative Ring Theory, Theorem 24.1.
• The Stacks Project, Tag 051R.

theorem Module.freeLocus_mem_nhds_of_mem_minimalPrimes {A : Type uA} [CommRing A] [IsNoetherianRing A] [IsReduced A] {B : Type u_1} [CommRing B] [Algebra A B] [Algebra.FiniteType A B] (M : Type uM) [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] [Module.Finite B M] {p : Ideal A} (hp : p ∈ minimalPrimes A) : freeLocus A M ∈ nhds { asIdeal := p, isPrime := ⋯ }

Generic freeness. Let A be a reduced Noetherian ring, B a finitely generated A-algebra and M a finite B-module. Then M is free over A on a neighbourhood of every minimal prime of A.

For a Noetherian domain A this means that there is a nonzero a : A such that M_q is free over A_q for every prime q not containing a.

theorem Module.dense_interior_freeLocus_of_finiteType {A : Type uA} [CommRing A] [IsNoetherianRing A] [IsReduced A] {B : Type u_1} [CommRing B] [Algebra A B] [Algebra.FiniteType A B] (M : Type uM) [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] [Module.Finite B M] : Dense (interior (freeLocus A M))

Generic freeness. Let A be a reduced Noetherian ring, B a finitely generated A-algebra and M a finite B-module. Then M is free over A on a dense open subset of Spec A.