The rank decomposition of a finitely generated projective module (GPR Exc. 9.31)

A finitely generated projective module M over a commutative ring R takes only finitely many ranks, and R splits — uniquely — into a finite product of rings on each factor of which M becomes of constant rank.

This is the tool that lets constant-rank hypotheses be assumed without loss of generality: GPR uses it repeatedly, in the form "by the rank decomposition we may assume M (or the composition algebra C) has constant rank r".

Main definitions

• Module.rankIdempotent R M i : the unique idempotent of R cutting out {p ∈ Spec R | rankAtStalk M p = i}.

Main results

• Module.finite_range_rankAtStalk : GPR Exc. 9.31(a) — the set of ranks of M is finite.
• Module.completeOrthogonalIdempotents_rankIdempotent : the rankIdempotent R M i, for i ranging over any finite set containing all the ranks, form a complete orthogonal system of idempotents. With CompleteOrthogonalIdempotents.bijective_pi this is the ring decomposition R ≃ ∏ᵢ R ⧸ (1 - εᵢ) of GPR Exc. 9.31(b)(1), and with CompleteOrthogonalIdempotents.linearEquivPiQuotientTensor (Module/IdempotentDecomposition.lean) the module decomposition (2).
• Module.rankAtStalk_quotientTensor_rankIdempotent : on the ith factor, M has constant rank i. This is the point of the whole construction.
• Module.rankAtStalk_baseChange_of_eq : constant rank survives base change.
• Module.nonempty_basis_atPrime_of_rankAtStalk_eq : a module of constant rank n is free of rank n at every prime.
• Module.eq_rankIdempotent_of_completeOrthogonalIdempotents : uniqueness — any complete orthogonal system with pairwise distinct constant ranks on its factors is the one above.

Proof idea

Module.rankAtStalk is locally constant on Spec R for a finitely presented flat module (mathlib's Module.isLocallyConstant_rankAtStalk), and Spec R is quasi-compact, so the range is finite — that is (a). Each fibre Uᵢ := {p | rankAtStalk M p = i} is then clopen, so by GPR Exc. 9.29 — mathlib's PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen — there is a unique idempotent εᵢ with D(εᵢ) = Uᵢ. Orthogonality and completeness are read off from the fact that the Uᵢ partition Spec R, via the observation that an idempotent whose basic open set is empty is nilpotent, hence zero.

That the ith factor has constant rank i is Module.rankAtStalk_baseChange: a prime of R ⧸ (1 - εᵢ) pulls back to a prime of R at which εᵢ is a unit — indeed εᵢ ↦ 1 — hence to a point of D(εᵢ) = Uᵢ.

Uniqueness follows because a competing system's basic opens are contained in the corresponding Uᵢ (same base-change computation, in the other direction, using that Spec (R ⧸ (1 - ηⱼ)) surjects onto D(ηⱼ)) and both families cover Spec R.

Implementation notes

GPR indexes the decomposition by all of ℕ, with εᵢ = 0 for i outside the (finite) set of ranks. Module.rankIdempotent is likewise defined for every i : ℕ and is 0 off the range (Module.rankIdempotent_eq_zero_of_notMem_range), but the complete-orthogonal-system statement is indexed by a Finset ℕ containing the ranks, since mathlib's CompleteOrthogonalIdempotents requires a Fintype.

The rank is mathlib's Module.rankAtStalk, not a bespoke rank function; GPR writes rk_p(M) for the same thing.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, Exc. 9.29, Exc. 9.31.

theorem Module.finite_range_rankAtStalk (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] : (Set.range (rankAtStalk M)).Finite

GPR Exc. 9.31(a). A finitely generated projective module takes only finitely many ranks.

Module.rankAtStalk is locally constant and Spec R is quasi-compact.

theorem Module.isClopen_setOf_rankAtStalk_eq (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (i : ℕ) : IsClopen {p : PrimeSpectrum R | rankAtStalk M p = i}

The locus where M has rank i is clopen.

noncomputable def Module.rankIdempotent (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (i : ℕ) : R

The idempotent of R cutting out the locus where M has rank i (GPR Exc. 9.31(b), GPR Exc. 9.29). It is 0 exactly when M has rank i nowhere.

Equations

• Module.rankIdempotent R M i = ⋯.choose

theorem Module.isIdempotentElem_rankIdempotent (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (i : ℕ) : IsIdempotentElem (rankIdempotent R M i)

theorem Module.coe_basicOpen_rankIdempotent (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (i : ℕ) : ↑(PrimeSpectrum.basicOpen (rankIdempotent R M i)) = {p : PrimeSpectrum R | rankAtStalk M p = i}

theorem Module.rankAtStalk_eq_of_mem_basicOpen_rankIdempotent (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] {i : ℕ} {p : PrimeSpectrum R} (hp : p ∈ PrimeSpectrum.basicOpen (rankIdempotent R M i)) : rankAtStalk M p = i

theorem Module.eq_rankIdempotent_of_coe_basicOpen_eq (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] {e : R} (he : IsIdempotentElem e) (i : ℕ) (h : ↑(PrimeSpectrum.basicOpen e) = {p : PrimeSpectrum R | rankAtStalk M p = i}) : e = rankIdempotent R M i

The rank idempotents are characterized by their basic open sets: an idempotent cutting out the rank-i locus is Module.rankIdempotent R M i (GPR Exc. 9.29(b)).

theorem Module.rankIdempotent_mul_rankIdempotent (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] {i j : ℕ} (h : i ≠ j) : rankIdempotent R M i * rankIdempotent R M j = 0

Distinct ranks give orthogonal idempotents: the rank loci are disjoint.

theorem Module.rankIdempotent_eq_zero_of_notMem_range (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] {i : ℕ} (h : i ∉ Set.range (rankAtStalk M)) : rankIdempotent R M i = 0

Ranks that do not occur give the zero idempotent.

theorem Module.completeOrthogonalIdempotents_rankIdempotent (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (s : Finset ℕ) (hs : ∀ (p : PrimeSpectrum R), rankAtStalk M p ∈ s) : CompleteOrthogonalIdempotents fun (i : ↥s) => rankIdempotent R M ↑i

GPR Exc. 9.31(b), existence. For any finite set of naturals containing every rank of M, the corresponding rank idempotents form a complete orthogonal system.

Feeding this to CompleteOrthogonalIdempotents.bijective_pi gives the ring decomposition R ≃ ∏ᵢ R ⧸ (1 - εᵢ), and to CompleteOrthogonalIdempotents.linearEquivPiQuotientTensor the module decomposition M ≃ ∏ᵢ (R ⧸ (1 - εᵢ)) ⊗[R] M.

theorem Module.rankAtStalk_quotientTensor_rankIdempotent (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (i : ℕ) : rankAtStalk (TensorProduct R (R ⧸ Ideal.span {1 - rankIdempotent R M i}) M) = fun (x : PrimeSpectrum (R ⧸ Ideal.span {1 - rankIdempotent R M i})) => i

The point of the rank decomposition. On the factor R ⧸ (1 - εᵢ), the module M has constant rank i.

Every prime of the factor pulls back to a prime of R at which εᵢ is invertible — it maps to 1 — hence to a point of D(εᵢ), which is exactly the rank-i locus.

theorem Module.eq_rankIdempotent_of_completeOrthogonalIdempotents (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] {ι : Type u_1} [Fintype ι] (η : ι → R) (hη : CompleteOrthogonalIdempotents η) (r : ι → ℕ) (hr : Function.Injective r) (h : ∀ (j : ι), rankAtStalk (TensorProduct R (R ⧸ Ideal.span {1 - η j}) M) = fun (x : PrimeSpectrum (R ⧸ Ideal.span {1 - η j})) => r j) (j : ι) : η j = rankIdempotent R M (r j)

GPR Exc. 9.31(b), uniqueness. A complete orthogonal system of idempotents whose factors give M pairwise distinct constant ranks consists of rank idempotents.

Injectivity of r is needed: without it two factors could carry the same rank, and their idempotents would sum to — rather than equal — the corresponding rank idempotent.

The decomposition, packaged

Indexing by the set of ranks itself, so that no Finset has to be supplied at the call site.

noncomputable def Module.rankFinset (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] : Finset ℕ

The set of ranks of M, as a Finset — finite by GPR Exc. 9.31(a). GPR writes Rk(M).

Equations

• Module.rankFinset R M = ⋯.toFinset

@[simp]

theorem Module.mem_rankFinset (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] {i : ℕ} : i ∈ rankFinset R M ↔ i ∈ Set.range (rankAtStalk M)

theorem Module.rankAtStalk_mem_rankFinset (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (p : PrimeSpectrum R) : rankAtStalk M p ∈ rankFinset R M

theorem Module.completeOrthogonalIdempotents_rankIdempotent_rankFinset (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] : CompleteOrthogonalIdempotents fun (i : ↥(rankFinset R M)) => rankIdempotent R M ↑i

The rank idempotents indexed by Rk(M) form a complete orthogonal system.

noncomputable def Module.rankDecompositionRingEquiv (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] : R ≃+* ((i : ↥(rankFinset R M)) → R ⧸ Ideal.span {1 - rankIdempotent R M ↑i})

GPR Exc. 9.31(b)(1), the rank decomposition of the ring. R is the product of the rings R ⧸ (1 - εᵢ), one for each rank i of M.

Equations

• Module.rankDecompositionRingEquiv R M = RingEquiv.ofBijective (RingHom.pi fun (i : ↥(Module.rankFinset R M)) => Ideal.Quotient.mk (Ideal.span {1 - Module.rankIdempotent R M ↑i})) ⋯

noncomputable def Module.rankDecompositionLinearEquiv (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] : M ≃ₗ[R] (i : ↥(rankFinset R M)) → TensorProduct R (R ⧸ Ideal.span {1 - rankIdempotent R M ↑i}) M

GPR Exc. 9.31(b)(2), the rank decomposition of the module. M is the product of its base changes to the factor rings, and by Module.rankAtStalk_quotientTensor_rankIdempotent the ith of these has constant rank i.

This is what licenses "by the rank decomposition we may assume M has constant rank".

Equations

• Module.rankDecompositionLinearEquiv R M = CompleteOrthogonalIdempotents.linearEquivPiQuotientTensor M (fun (i : ↥(Module.rankFinset R M)) => Module.rankIdempotent R M ↑i) ⋯

The rank-zero idempotent

ε₀ = Module.rankIdempotent R M 0 cuts out the locus where M vanishes. Two facts about it are used, without ever performing the product decomposition of R that it induces:

• it annihilates M (Module.rankIdempotent_zero_smul), and
• it is a unit at every maximal ideal where M has trivial residue space (Module.notMem_rankIdempotent_zero).

Together they let an argument treat the vanishing locus of M separately while staying over R: multiplying by ε₀ kills everything coming from M, and reducing modulo a maximal ideal in the vanishing locus turns ε₀ into 1.

theorem Module.rankIdempotent_zero_smul (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (x : M) : rankIdempotent R M 0 • x = 0

The rank-zero idempotent annihilates M.

Checked one maximal ideal P at a time. If ε₀ ∈ P then 1 - ε₀ ∉ P annihilates ε₀ • x; if ε₀ ∉ P then M has rank 0 at P, so P is outside the support of M and some r ∉ P already annihilates x. An element annihilated modulo every maximal ideal is zero.

theorem Module.notMem_rankIdempotent_zero (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 : Subsingleton (TensorProduct R (R ⧸ 𝔪) M)) : rankIdempotent R M 0 ∉ 𝔪

The rank-zero idempotent is a unit where M vanishes. If M ⊗ κ(𝔪) is trivial at a maximal ideal 𝔪 then ε₀ ∉ 𝔪.

M ⊗ R⧸𝔪 is M ⧸ 𝔪 M, whose support is Supp M ∩ V(𝔪); triviality makes that empty, and 𝔪 lies in V(𝔪), so 𝔪 ∉ Supp M — that is, M has rank 0 at 𝔪, which is exactly membership in D(ε₀).

Detecting vanishing on the factors

The two lemmas the phrase "by the rank decomposition we may assume constant rank" needs when the statement to be transported is an equation rather than a structure: an element of M vanishes as soon as it vanishes in each (R ⧸ (1 - εᵢ)) ⊗ M. They are stated separately because the second is about a single factor and carries no finiteness.

theorem Module.eq_zero_of_forall_rankIdempotent_smul_eq_zero (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] {x : M} (h : ∀ (i : ↥(rankFinset R M)), rankIdempotent R M ↑i • x = 0) : x = 0

An element killed by every rank idempotent is zero, the idempotents summing to 1.

theorem Module.rankIdempotent_smul_eq_zero_of_one_tmul_eq_zero (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] (i : ℕ) {x : M} (h : 1 ⊗ₜ[R] x = 0) : rankIdempotent R M i • x = 0

If x dies in the ith factor (R ⧸ (1 - εᵢ)) ⊗ M of the rank decomposition, then εᵢ kills it.

Reducing M modulo an ideal is tensoring with the quotient ring (TensorProduct.quotTensorEquivQuotSMul), so the hypothesis says x ∈ span{1 - εᵢ} • ⊤; and εᵢ annihilates that submodule, since εᵢ(1 - εᵢ) = 0.

Constant rank means locally free of that rank

theorem Module.rankAtStalk_baseChange_of_eq {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Flat R M] [Module.Finite R M] (S : Type u_1) [CommRing S] [Algebra R S] {n : ℕ} (hM : rankAtStalk M = fun (x : PrimeSpectrum R) => n) : rankAtStalk (TensorProduct R S M) = fun (x : PrimeSpectrum S) => n

Constant rank survives base change: if M has rank n at every prime of R, then S ⊗[R] M has rank n at every prime of S.

theorem Module.nonempty_basis_atPrime_of_rankAtStalk_eq {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Projective R M] {n : ℕ} (hM : rankAtStalk M = fun (x : PrimeSpectrum R) => n) (J : Ideal R) [J.IsPrime] : Nonempty (Basis (Fin n) (Localization.AtPrime J) (TensorProduct R (Localization.AtPrime J) M))

A finitely generated projective module of constant rank n becomes free of rank n at every prime.