The free locus of a module

Main definitions and results

Let M be a finitely presented R-module.

• Module.freeLocus: The set of points x in Spec R such that Mₓ is free over Rₓ.
• Module.freeLocus_eq_univ_iff: The free locus is the whole Spec R if and only if M is projective.
• Module.basicOpen_subset_freeLocus_iff: D(f) is contained in the free locus if and only if M_f is projective over R_f.
• Module.rankAtStalk: The function Spec R → ℕ sending x to rank_{Rₓ} Mₓ.
• Module.isLocallyConstant_rankAtStalk: If M is flat over R, then rankAtStalk is locally constant.

def Module.freeLocus (R : Type uR) (M : Type uM) [CommRing R] [AddCommGroup M] [Module R M] : Set (PrimeSpectrum R)

The free locus of a module, i.e. the set of primes p such that Mₚ is free over Rₚ.

Equations

• Module.freeLocus R M = {p : PrimeSpectrum R | Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M)}

theorem Module.mem_freeLocus {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} : p ∈ Module.freeLocus R M ↔ Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M)

theorem Module.mem_freeLocus_of_isLocalization {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (p : PrimeSpectrum R) (Rₚ : Type u_1) (Mₚ : Type u_2) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p.asIdeal] [AddCommGroup Mₚ] [Module R Mₚ] (f : M →ₗ[R] Mₚ) [IsLocalizedModule p.asIdeal.primeCompl f] [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ] : p ∈ Module.freeLocus R M ↔ Module.Free Rₚ Mₚ

theorem Module.mem_freeLocus_iff_tensor {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (p : PrimeSpectrum R) (Rₚ : Type u_1) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p.asIdeal] : p ∈ Module.freeLocus R M ↔ Module.Free Rₚ (TensorProduct R Rₚ M)

theorem Module.freeLocus_congr {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {M' : Type u_1} [AddCommGroup M'] [Module R M'] (e : M ≃ₗ[R] M') : Module.freeLocus R M = Module.freeLocus R M'

theorem Module.comap_freeLocus_le {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {A : Type u_1} [CommRing A] [Algebra R A] : ⇑(PrimeSpectrum.comap (algebraMap R A)) ⁻¹' Module.freeLocus R M ≤ Module.freeLocus A (TensorProduct R A M)

theorem Module.freeLocus_localization {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (S : Submonoid R) : Module.freeLocus (Localization S) (LocalizedModule S M) = ⇑(PrimeSpectrum.comap (algebraMap R (Localization S))) ⁻¹' Module.freeLocus R M

theorem Module.freeLocus_eq_univ_iff {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] : Module.freeLocus R M = Set.univ ↔ Module.Projective R M

theorem Module.freeLocus_eq_univ {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] [Module.Flat R M] : Module.freeLocus R M = Set.univ

theorem Module.basicOpen_subset_freeLocus_iff {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] {f : R} : ↑(PrimeSpectrum.basicOpen f) ⊆ Module.freeLocus R M ↔ Module.Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) M)

theorem Module.isOpen_freeLocus {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] : IsOpen (Module.freeLocus R M)

noncomputable def Module.rankAtStalk {R : Type uR} (M : Type uM) [CommRing R] [AddCommGroup M] [Module R M] (p : PrimeSpectrum R) : ℕ

The rank of M at the stalk of p is the rank of Mₚ as a Rₚ-module.

Equations

• Module.rankAtStalk M p = Module.finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M)

theorem Module.isLocallyConstant_rankAtStalk_freeLocus {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] : IsLocallyConstant fun (x : ↑(Module.freeLocus R M)) => Module.rankAtStalk M ↑x

theorem Module.isLocallyConstant_rankAtStalk {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] [Module.Flat R M] : IsLocallyConstant (Module.rankAtStalk M)