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.

noncomputable def RingHom.finrank {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (x : PrimeSpectrum R) : ℕ

The rank of a ring homomorphism f : R →+* S at a prime x of R is the rank of S as an R-module at the stalk of x.

Equations

• f.finrank x = Module.rankAtStalk S x

@[simp]

theorem RingHom.finrank_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).finrank = Module.rankAtStalk S

theorem Algebra.rankAtStalk_eq_of_isPushout (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] (R' : Type u_5) (S' : Type u_6) [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] [Module.Flat R S] [Module.Finite R S] (x : PrimeSpectrum R') : Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)

theorem RingHom.finrank_comp_left_of_bijective {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (hf : Function.Bijective ⇑g) (h1 : f.Finite) (h2 : f.Flat) (x : PrimeSpectrum R) : (g.comp f).finrank x = f.finrank x

theorem RingHom.finrank_comp_right_of_bijective {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (hg : Function.Bijective ⇑f) (h1 : g.Finite) (h2 : g.Flat) (y : PrimeSpectrum R) (x : PrimeSpectrum S) (hy : y = PrimeSpectrum.comap f x) : (g.comp f).finrank y = g.finrank x

theorem CommRingCat.finrank_eq_of_isPushout {R S T P : CommRingCat} {f : R ⟶ S} {g : R ⟶ T} {inl : S ⟶ P} {inr : T ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) (hf : (Hom.hom f).Flat) (hfin : (Hom.hom f).Finite) (x : PrimeSpectrum ↑T) : (Hom.hom inr).finrank x = (Hom.hom f).finrank (PrimeSpectrum.comap (Hom.hom g) x)