Modules over an idempotent factor of a ring

For an idempotent e of a commutative ring k, the quotient S = k ⧸ (1 - e) is the factor of k cut out by e, and Spec S is the clopen set of primes containing 1 - e. This file compares modules over S with modules over k.

An S-module P is a k-module by restriction of scalars, and as such it is the base change of itself (Module.isBaseChange_self_of_surjective): S ⊗[k] P ≅ P. If P is finitely generated projective over S, it is finitely generated projective over k, and its rank at a prime p of k is its rank over S at the corresponding prime when 1 - e ∈ p, and 0 otherwise.

The point is Module.free_of_forall_free_of_isIdempotentElem: if every finitely generated projective k-module of constant rank is free, then so is every finitely generated projective S-module of constant rank. A constant-rank-r module P over S becomes one over k after adding the free module of rank r over the complementary factor k ⧸ (e); that sum is free over k, and P is its base change to S. This is the reduction used tacitly in GPR 22.16 when the freeness hypothesis on k is applied to the rank components of a composition algebra.

Main results

• Module.isBaseChange_self_of_surjective : over a surjection k → S, an S-module is its own base change.
• Module.projective_of_isIdempotentElem, Module.finite_of_isIdempotentElem : a finitely generated projective module over k ⧸ (1 - e) is finitely generated projective over k.
• Module.rankAtStalk_comap_of_isIdempotentElem, Module.rankAtStalk_eq_zero_of_isIdempotentElem : its rank over k.
• Module.free_of_forall_free_of_isIdempotentElem : freeness of constant-rank projectives passes from k to its idempotent factors.

References

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

theorem Module.isBaseChange_self_of_surjective {k : Type u} {S : Type v} [CommRing k] [CommRing S] [Algebra k S] (hS : Function.Surjective ⇑(algebraMap k S)) (P : Type w) [AddCommGroup P] [Module k P] [Module S P] [IsScalarTower k S P] : IsBaseChange S (↑k LinearMap.id)

Over a surjection k → S, an S-module is its own base change: S ⊗[k] P ≅ P, by a ⊗ x ↦ a • x. Every a ∈ S lifts to k, so every tensor is of the form 1 ⊗ x.

theorem Module.algebraMap_quotient_one_sub_self {k : Type u} [CommRing k] {e : k} : (algebraMap k (k ⧸ Ideal.span {1 - e})) e = 1

In k ⧸ (1 - e) the element e becomes 1.

theorem Module.projective_quotient_one_sub {k : Type u} [CommRing k] {e : k} (he : IsIdempotentElem e) : Projective k (k ⧸ Ideal.span {1 - e})

The factor k ⧸ (1 - e) is a direct summand of k: the class of x ↦ e x splits the quotient map.

theorem Module.projective_of_isIdempotentElem {k : Type u} [CommRing k] {e : k} (he : IsIdempotentElem e) (P : Type w) [AddCommGroup P] [Module (k ⧸ Ideal.span {1 - e}) P] [Module k P] [IsScalarTower k (k ⧸ Ideal.span {1 - e}) P] [Projective (k ⧸ Ideal.span {1 - e}) P] : Projective k P

A projective module over the factor k ⧸ (1 - e) is projective over k.

theorem Module.finite_of_isIdempotentElem {k : Type u} [CommRing k] {e : k} (P : Type w) [AddCommGroup P] [Module (k ⧸ Ideal.span {1 - e}) P] [Module k P] [IsScalarTower k (k ⧸ Ideal.span {1 - e}) P] [Module.Finite (k ⧸ Ideal.span {1 - e}) P] : Module.Finite k P

A finitely generated module over the factor k ⧸ (1 - e) is finitely generated over k.

theorem Module.rankAtStalk_comap_of_isIdempotentElem {k : Type u} [CommRing k] {e : k} (he : IsIdempotentElem e) (P : Type w) [AddCommGroup P] [Module (k ⧸ Ideal.span {1 - e}) P] [Module k P] [IsScalarTower k (k ⧸ Ideal.span {1 - e}) P] [Module.Finite (k ⧸ Ideal.span {1 - e}) P] [Projective (k ⧸ Ideal.span {1 - e}) P] (q : PrimeSpectrum (k ⧸ Ideal.span {1 - e})) : rankAtStalk P (PrimeSpectrum.comap (algebraMap k (k ⧸ Ideal.span {1 - e})) q) = rankAtStalk P q

At a prime of k containing 1 - e, the rank of a finitely generated projective module over k ⧸ (1 - e) is its rank over the factor.

theorem Module.rankAtStalk_eq_zero_of_isIdempotentElem {k : Type u} [CommRing k] {e : k} (he : IsIdempotentElem e) (P : Type w) [AddCommGroup P] [Module (k ⧸ Ideal.span {1 - e}) P] [Module k P] [IsScalarTower k (k ⧸ Ideal.span {1 - e}) P] [Module.Finite (k ⧸ Ideal.span {1 - e}) P] [Projective (k ⧸ Ideal.span {1 - e}) P] (p : PrimeSpectrum k) (hp : 1 - e ∉ p.asIdeal) : rankAtStalk P p = 0

At a prime of k not containing 1 - e, a finitely generated projective module over k ⧸ (1 - e) has rank zero: 1 - e kills it and is a unit there.

theorem Module.free_of_forall_free_of_isIdempotentElem {k : Type u} [CommRing k] {e : k} (he : IsIdempotentElem e) (hfree : ∀ (N : Type (max u w)) [inst : AddCommGroup N] [inst_1 : Module k N] [Module.Finite k N] [Projective k N] (r : ℕ), (rankAtStalk N = fun (x : PrimeSpectrum k) => r) → Free k N) (P : Type (max u w)) [AddCommGroup P] [Module (k ⧸ Ideal.span {1 - e}) P] [Module.Finite (k ⧸ Ideal.span {1 - e}) P] [Projective (k ⧸ Ideal.span {1 - e}) P] (r : ℕ) (hP : rankAtStalk P = fun (x : PrimeSpectrum (k ⧸ Ideal.span {1 - e})) => r) : Free (k ⧸ Ideal.span {1 - e}) P

Freeness passes to idempotent factors. If every finitely generated projective k-module of constant rank is free, so is every finitely generated projective module of constant rank over the factor k ⧸ (1 - e).

A module P of constant rank r over k ⧸ (1 - e) is, as a k-module, of rank r on the primes containing 1 - e and of rank 0 on the others; adding the free module of rank r over the complementary factor k ⧸ (e) gives a k-module N of constant rank r. N is free by hypothesis, hence so is its base change to k ⧸ (1 - e), which is P.