Results for the rank of a finite flat algebra

In this file we study a finite, flat R-algebra S and relate injectivity and bijectivity of R → S with the rank of S over R.

Main results

• PrimeSpectrum.comap_surjective_iff_injective_of_finite: Spec S → Spec R is surjective if and only if R → S is injective.
• Module.Flat.tfae_algebraMap_surjective: R → S is surjective iff S ⊗[R] S → S is an isomorphism iff the rank of S is at most 1 at all primes.
• Module.algebraMap_bijective_iff_rankAtStalk: S is of constant R-rank 1 if and only if S is isomorphic to R.

theorem PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [Module.Finite R S] (p : PrimeSpectrum R) : 0 < Module.rankAtStalk S p ↔ p ∈ Set.range (comap (algebraMap R S))

theorem PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [Module.Finite R S] : (∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p) ↔ Function.Surjective (comap (algebraMap R S))

The rank is positive at all stalks if and only if the induced map on prime spectra is surjective.

theorem PrimeSpectrum.comap_surjective_iff_injective_of_finite {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [Module.Finite R S] : Function.Surjective (comap (algebraMap R S)) ↔ Function.Injective ⇑(algebraMap R S)

theorem Module.rankAtStalk_pos_iff_algebraMap_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Flat R S] [Module.Finite R S] : (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔ Function.Injective ⇑(algebraMap R S)

theorem Module.algebraMap_surjective_of_rankAtStalk_le_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Flat R S] [Module.Finite R S] (h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1) : Function.Surjective ⇑(algebraMap R S)

theorem Module.Flat.tfae_algebraMap_surjective (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Flat R S] [Module.Finite R S] : [Function.Surjective ⇑(algebraMap R S), Function.Bijective ⇑(LinearMap.mul' R S), ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1].TFAE

If S is a finite and flat R-algebra, R → S is surjective iff S ⊗[R] S → S is an isomorphism iff the rank of S is at most 1 at all primes.

theorem Module.rankAtStalk_le_one_iff_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Flat R S] [Module.Finite R S] : (∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1) ↔ Function.Surjective ⇑(algebraMap R S)

theorem Module.algebraMap_bijective_iff_rankAtStalk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Flat R S] [Module.Finite R S] : rankAtStalk S = 1 ↔ Function.Bijective ⇑(algebraMap R S)

If S is a finite, flat R-algebra, S is of constant rank 1 if and only if S is isomorphic to R.

theorem Module.algebraMap_bijective_of_rankAtStalk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Flat R S] [Module.Finite R S] : rankAtStalk S = 1 → Function.Bijective ⇑(algebraMap R S)

Alias of the forward direction of Module.algebraMap_bijective_iff_rankAtStalk.

---

If S is a finite, flat R-algebra, S is of constant rank 1 if and only if S is isomorphic to R.