Ramification index and inertia degree

This file proves that the sum of ramification times inertia equals the degree of the extension.

Typically this is only stated for extensions of Dedekind domains, but we prove it for any finite flat extension of an integral domain.

Main results

• Ideal.sum_ramification_inertia_eq_finrank: Let R be an integral domain, let S be a finite flat R-algebra, and let p be a prime ideal of R. Then the sum over all prime ideals q of S lying over p of the ramification index of q times the inertia degree of q equals the rank of S as an R-module.
• Ideal.sum_ramification_inertia_eq_card: Let S/R be a finite flat extension of domains, and let p be prime ideal of R. Assume that R is the invariant subring of a finite group G acting on S. Then the sum over all prime ideals q of S lying over p of the ramification index of q times the inertia degree of q equals the cardinality of G.

theorem Ideal.sum_ramification_inertia_eq_finrank_fiber {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] (S : Type u_2) [CommRing S] [Algebra R S] [Algebra.QuasiFinite R S] [Module.Flat R S] [Fintype ↑(p.primesOver S)] : ∑ q : ↑(p.primesOver S), (↑q).ramificationIdx' R * (↑q).inertiaDeg' R = Module.finrank p.ResidueField (p.Fiber S)

theorem Ideal.sum_ramification_inertia_eq_finrank {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] (S : Type u_2) [CommRing S] [Algebra R S] [IsDomain R] [Module.Finite R S] [Module.Flat R S] [Fintype ↑(p.primesOver S)] : ∑ q : ↑(p.primesOver S), (↑q).ramificationIdx' R * (↑q).inertiaDeg' R = Module.finrank R S

Let R be an integral domain, let S be a finite flat R-algebra, and let p be a prime ideal of R. Then the sum over all prime ideals q of S lying over p of the ramification index of q times the inertia degree of q equals the rank of S as an R-module.

theorem Ideal.sum_ramification_inertia_eq_card {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] (S : Type u_2) [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S] [Fintype ↑(p.primesOver S)] {G : Type u_3} [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] : ∑ q : ↑(p.primesOver S), (↑q).ramificationIdx' R * (↑q).inertiaDeg' R = Nat.card G

Let S/R be a finite flat extension of integral domains, and let p be prime ideal of R. Assume that R is the invariant subring of a finite group G acting on S. Then the sum over all prime ideals q of S lying over p of the ramification index of q times the inertia degree of q equals the cardinality of G.