Constant-rank projective modules over an LG-ring are free (GN 2.6(b), GPR 11.24)

This is the motto of LG-rings, made precise: over an LG-ring, a finitely generated projective module whose rank is the same at every prime is free.

Main results

• Module.nontrivial_quotient_tensor_of_rankAtStalk_pos : positive rank at a maximal ideal makes the residue-field fibre nonzero — the bridge from Module.rankAtStalk to the hypothesis of IsLGRing.exists_isUnimodular.
• Module.free_of_isLGRing_of_rankAtStalk_eq : GN 2.6(b), by induction on the rank.

Proof idea

Induct on the common rank d, with M generalized.

At d = 0 the module is a subsingleton (Module.rankAtStalk_eq_zero_iff_subsingleton), hence free. At d + 1 the rank is positive at every prime, so every residue-field fibre is nonzero and GN 2.6(a) (IsLGRing.exists_isUnimodular, LGRing/Unimodular.lean) produces a unimodular m ∈ M. That splits M ≃ R × ker l (LinearMap.equivProdKerOfApplyEqOne), and Module.rankAtStalk_prod together with Module.rankAtStalk_self turns the rank equation into rankAtStalk (ker l) = d — constant again, one lower. The induction hypothesis makes ker l free, and R × ker l is then free, hence so is M.

The complement is ker l, a Submodule R M: it lives in the same universe as M, which is what lets the induction quantify over a single Type v.

Implementation notes

The rank is Module.rankAtStalk, mathlib's rank of the localization at a prime. Everything the induction needs — additivity over products, invariance under equivalence, the value at R, and vanishing exactly on subsingletons — is already in Mathlib.RingTheory.Spectrum.Prime.FreeLocus, so this file adds no rank theory of its own.

The one genuinely new bridge is Module.nontrivial_quotient_tensor_of_rankAtStalk_pos: the LG axiom speaks about residue fields R ⧸ 𝔪, whereas rankAtStalk is defined through localizations R_𝔪. Module.rankAtStalk_baseChange relates them — base changing M to the field R ⧸ 𝔪 and reading the rank at that field's unique prime ⊥ gives back the rank of M at 𝔪, because ⊥ pulls back along R → R ⧸ 𝔪 to 𝔪. Over a field every module is free, so that rank is a finrank, and a positive finrank forces nontriviality.

References

• [GN] Gille, Neher, Group schemes over LG-rings and applications to cancellation theorems and Azumaya algebras, European Journal of Mathematics 11 (2025), article 42, Lemma 2.6(b), also stated as 2.1(c).
• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.24.

theorem Module.nontrivial_quotient_tensor_of_rankAtStalk_pos {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (𝔪 : Ideal R) (h𝔪 : 𝔪.IsMaximal) (h : 0 < rankAtStalk M { asIdeal := 𝔪, isPrime := ⋯ }) : Nontrivial (TensorProduct R (R ⧸ 𝔪) M)

Positive rank at a maximal ideal makes the residue-field fibre nonzero.

This is the bridge from Module.rankAtStalk, which is defined through the localization R_𝔪, to the hypothesis of IsLGRing.exists_isUnimodular, which — like the LG axiom itself — speaks about the residue field R ⧸ 𝔪. See the module docstring.

theorem Module.free_of_isLGRing_of_rankAtStalk_eq {R : Type u} [CommRing R] (hLG : IsLGRing R) (d : ℕ) (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] : (rankAtStalk M = fun (x : PrimeSpectrum R) => d) → Free R M

GN 2.6(b), GPR 11.24. Over an LG-ring, a finitely generated projective module of constant rank is free.

The rank is Module.rankAtStalk, and "constant" means literally the constant function d. See the module docstring for the induction.