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 ∈ freeLocus R M ↔ 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 ∈ freeLocus R M ↔ 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 ∈ freeLocus R M ↔ 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') : freeLocus R M = 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) ⁻¹' freeLocus R M ⊆ 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) : freeLocus (Localization S) (LocalizedModule S M) = PrimeSpectrum.comap (algebraMap R (Localization S)) ⁻¹' freeLocus R M

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

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

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

theorem Module.isOpen_freeLocus {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [FinitePresentation R M] : IsOpen (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] [FinitePresentation R M] : IsLocallyConstant fun (x : ↑(freeLocus R M)) => rankAtStalk M ↑x

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

@[simp]

theorem Module.rankAtStalk_eq_zero_of_subsingleton {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Subsingleton M] : rankAtStalk M = 0

theorem Module.nontrivial_of_rankAtStalk_pos {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (h : 0 < rankAtStalk M) : Nontrivial M

theorem Module.rankAtStalk_eq_of_equiv {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : rankAtStalk M = rankAtStalk N

@[simp]

theorem Module.rankAtStalk_eq_finrank_of_free {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Free R M] : rankAtStalk M = ↑(finrank R M)

If M is R-free, its rank at stalks is constant and agrees with the R-rank of M.

theorem Module.rankAtStalk_self {R : Type uR} [CommRing R] [Nontrivial R] : rankAtStalk R = 1

theorem Module.rankAtStalk_pi {R : Type uR} [CommRing R] {ι : Type u_1} [Finite ι] (M : ι → Type u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Flat R (M i)] [∀ (i : ι), Module.Finite R (M i)] (p : PrimeSpectrum R) : rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk (M i) p

The rank of Π i, M i at a prime p is the sum of the ranks of M i at p.

theorem Module.rankAtStalk_eq_finrank_tensorProduct {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (p : PrimeSpectrum R) : rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (TensorProduct R (Localization.AtPrime p.asIdeal) M)

theorem Module.rankAtStalk_eq_zero_iff_notMem_support {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] (p : PrimeSpectrum R) : rankAtStalk M p = 0 ↔ p ∉ support R M

theorem Module.rankAtStalk_pos_iff_mem_support {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] (p : PrimeSpectrum R) : 0 < rankAtStalk M p ↔ p ∈ support R M

theorem Module.rankAtStalk_eq_zero_iff_subsingleton {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] : rankAtStalk M = 0 ↔ Subsingleton M

theorem Module.rankAtStalk_prod {R : Type uR} (M : Type uM) [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] (N : Type u_1) [AddCommGroup N] [Module R N] [Flat R N] [Module.Finite R N] : rankAtStalk (M × N) = rankAtStalk M + rankAtStalk N

The rank of M × N at p is equal to the sum of the ranks.

theorem Module.rankAtStalk_baseChange {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] {S : Type u_1} [CommRing S] [Algebra R S] (p : PrimeSpectrum S) : rankAtStalk (TensorProduct R S M) p = rankAtStalk M (PrimeSpectrum.comap (algebraMap R S) p)

theorem Module.rankAtStalk_isBaseChange {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] {S : Type u_1} {Mₛ : Type u_2} [CommRing S] [Algebra R S] [AddCommGroup Mₛ] [Module R Mₛ] [Module S Mₛ] [IsScalarTower R S Mₛ] {f : M →ₗ[R] Mₛ} (hf : IsBaseChange S f) (p : PrimeSpectrum S) : rankAtStalk Mₛ p = rankAtStalk M (PrimeSpectrum.comap (algebraMap R S) p)

theorem Module.rankAtStalk_eq_of_le_of_finite_of_flat {R : Type uR} (M : Type uM) [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] {p q : PrimeSpectrum R} (hpq : p ≤ q) : rankAtStalk M p = rankAtStalk M q

theorem Module.rankAtStalk_eq_of_le_of_finite_of_flat' {R : Type uR} (M : Type uM) [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] {p q : Ideal R} [hp : p.IsPrime] [hq : q.IsPrime] (hpq : p ≤ q) : rankAtStalk M { asIdeal := p, isPrime := hp } = rankAtStalk M { asIdeal := q, isPrime := hq }

theorem Module.rankAtStalk_tensorProduct {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] (N : Type u_1) [AddCommGroup N] [Module R N] [Module.Finite R N] [Flat R N] : rankAtStalk (TensorProduct R M N) = rankAtStalk M * rankAtStalk N

See rankAtStalk_tensorProduct_of_isScalarTower for a hetero-basic version.

theorem Module.rankAtStalk_tensorProduct_of_isScalarTower {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] {S : Type u_1} [CommRing S] [Algebra R S] (N : Type u_2) [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] [Module.Finite S N] [Flat S N] (p : PrimeSpectrum S) : rankAtStalk (TensorProduct R N M) p = rankAtStalk N p * rankAtStalk M (PrimeSpectrum.comap (algebraMap R S) p)

theorem Module.rankAtStalk_eq {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] (p : PrimeSpectrum R) : rankAtStalk M p = finrank p.asIdeal.ResidueField (p.asIdeal.Fiber M)

The rank of a module M at a prime p is equal to the dimension of κ(p) ⊗[R] M as a κ(p)-module.

theorem Ideal.finrank_fiber_eq_rankAtStalk {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] [Module.Finite R M] (p : Ideal R) [hp : p.IsPrime] : Module.finrank p.ResidueField (p.Fiber M) = Module.rankAtStalk M { asIdeal := p, isPrime := hp }

Variant of Module.rankAtStalk_eq for better rewriting.

theorem Ideal.finrank_fiber_eq_finrank {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] [Module.Finite R M] [IsDomain R] (p : Ideal R) [p.IsPrime] : Module.finrank p.ResidueField (p.Fiber M) = Module.finrank R M