The free locus over a reduced ring, and of a filtered module

Every module over a reduced ring is free at each minimal prime. For a finitely presented module, Mathlib's openness of the free locus therefore gives an open neighbourhood of the minimal primes where it is locally free.

A module with an exhaustive increasing filtration is free at every prime where all the subquotients of the filtration are free. No finiteness is assumed, so this applies to modules that are not finitely generated over the base, as in the proof of generic freeness in TauCeti.RingTheory.Spectrum.Prime.GenericFreeness.

Main declarations

• Module.mem_freeLocus_of_mem_minimalPrimes: over a reduced ring, every module is free at the minimal primes.
• Module.iInter_freeLocus_subquotient_subset_freeLocus: a filtered module is free wherever all subquotients of the filtration are.

References

• The Stacks Project, Tags 051R and 051Z, for generic freeness.

theorem Module.mem_freeLocus_of_mem_minimalPrimes {R : Type u_1} (M : Type u_2) [CommRing R] [IsReduced R] [AddCommGroup M] [Module R M] {p : Ideal R} (hp : p ∈ minimalPrimes R) : { asIdeal := p, isPrime := ⋯ } ∈ freeLocus R M

Over a reduced ring, every module is free at each minimal prime, where the localization of the ring is a field.

theorem Module.freeLocus_nonempty (R : Type u_1) (M : Type u_2) [CommRing R] [IsReduced R] [AddCommGroup M] [Module R M] [Nontrivial R] : (freeLocus R M).Nonempty

A module over a nonzero reduced ring has nonempty free locus.

theorem Module.iInter_freeLocus_subquotient_subset_freeLocus {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : ℕ → Submodule R M) (hN : Monotone N) (h0 : N 0 = ⊥) (htop : ⨆ (j : ℕ), N j = ⊤) : ⋂ (j : ℕ), freeLocus R (↥(N (j + 1)) ⧸ (N j).submoduleOf (N (j + 1))) ⊆ freeLocus R M

A module is free at every prime at which all subquotients N (j + 1) ⧸ N j of an exhaustive increasing filtration ⊥ = N 0 ≤ N 1 ≤ ⋯ are free.

No finiteness is assumed, so this applies to filtrations of modules that are not finitely generated over the base ring.

theorem PrimeSpectrum.flat_localization_of_comap_mem_freeLocus {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : PrimeSpectrum S) (hq : comap (algebraMap R S) q ∈ Module.freeLocus R S) : Module.Flat R (Localization.AtPrime q.asIdeal)

If a base prime belongs to the free locus of an algebra, that algebra is flat over the base after localizing at any prime above it.