Complete splitting is trivial ramification and inertia

This file records the non-Galois counting criterion for primes in finite flat extensions of domains: a prime has as many primes above it as the degree allows exactly when every one of them is unramified with trivial residue extension.

The Galois form, where the count is compared with the order of the Galois group, is in TauCeti/NumberTheory/RamificationInertia/Galois.lean. No Galois hypothesis is needed here: the fundamental identity alone forces each summand e * f down to 1.

Main results

• ramificationIdx_eq_one_and_inertiaDeg_eq_one_of_ncard_primesOver_eq_finrank — a maximal count of primes above P makes e = f = 1 at each of them.
• Ideal.ncard_primesOver_eq_finrank_iff_forall_ramificationIdx_eq_one_and_inertiaDeg_eq_one — conversely, e = f = 1 at every prime above P makes the count maximal.
• bijective_algebraMap_quotient_of_ncard_primesOver_eq_finrank — for P maximal, the same count makes the residue map R ⧸ P → S ⧸ Q bijective.

Provenance

Built directly on Mathlib's fundamental identity for finite flat extensions of domains (Ideal.sum_ramification_inertia_eq_finrank). The residue-field consequence additionally uses Mathlib's identification of the inertia degree with the rank of the residue extension (Ideal.inertiaDeg'_algebraMap) and its characterisation of rank-one algebras over a field (Algebra.finrank_eq_one_iff_bijective_algebraMap).

theorem TauCeti.RamificationInertia.ramificationIdx_eq_one_and_inertiaDeg_eq_one_of_ncard_primesOver_eq_finrank {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] (P : Ideal R) [P.IsPrime] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver P] (hsplit : (P.primesOver S).ncard = Module.finrank R S) : Q.ramificationIdx R = 1 ∧ Q.inertiaDeg R = 1

A maximal count of primes above P forces e = f = 1. If the number of primes of S lying over a prime P of R equals the rank of S over R, then each such prime is unramified over P and has trivial inertia degree. No Galois hypothesis is needed.

theorem Ideal.ncard_primesOver_eq_finrank_iff_forall_ramificationIdx_eq_one_and_inertiaDeg_eq_one {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] (P : Ideal R) [P.IsPrime] : (P.primesOver S).ncard = Module.finrank R S ↔ ∀ Q ∈ P.primesOver S, Q.ramificationIdx R = 1 ∧ Q.inertiaDeg R = 1

The count criterion for complete splitting. The number of primes of S lying over a prime P of R equals the rank of S over R exactly when every one of them has ramification index and inertia degree 1. No Galois hypothesis is needed: both directions are the fundamental identity ∑ e * f = [S : R], a sum of positive terms indexed by those primes.

theorem TauCeti.RamificationInertia.bijective_algebraMap_quotient_of_ncard_primesOver_eq_finrank {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] (P : Ideal R) [P.IsMaximal] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver P] (hsplit : (P.primesOver S).ncard = Module.finrank R S) : Function.Bijective ⇑(algebraMap (R ⧸ P) (S ⧸ Q))

A maximal count of primes above P makes the residue extension trivial. If P is maximal and the number of primes of S lying over P equals the rank of S over R, then the residue map R ⧸ P → S ⧸ Q is bijective. No Galois hypothesis is needed.