Ramification indices below an intermediate invariant ring

Let a finite group G act on a finite flat extension of domains B/A, with invariant ring A, and let C be the invariant ring of a subgroup H. Assume also that B/C is flat. At a maximal ideal P of B with separable residue extension over A, the ramification index of P ∩ C over A is [I(P) : I(P) ∩ H]. In particular that index is one exactly when I(P) ≤ H. This supplies the inertia part of the splitting dictionary for non-Galois intermediate rings.

The division-free tower formula needs only that H is the Galois group of B/C and that its residue extension is separable; the base ring need not be a domain. The index formula additionally uses the invariant extension B/A. Residue separability is essential: without it the inertia order is the ramification index times the inseparable residue degree. The general index formula below includes this inseparable residue degree and requires no residue separability. The translated formulas apply the same description throughout the group orbit of a selected prime, while requiring separability only at that prime.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §9, including Exercise 4.
• G. J. Janusz, Algebraic Number Fields, Chapter I.
• These results generalize Tau Ceti's NumberField.ramificationIdx_under_eq_one_iff_inertia_le in TauCeti/NumberTheory/NumberField/Inertia.lean to intermediate invariant rings.

theorem Ideal.ramificationIdx_under_mul_card_inertia_inf {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] (P : Ideal B) [P.IsMaximal] (H : Subgroup G) (C : Type u_4) [CommRing C] [IsDomain C] [IsDomain B] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsGaloisGroup (↥H) C B] [Module.Finite C B] [Module.Flat C B] [Algebra.IsSeparable (C ⧸ under C P) (B ⧸ P)] : (under C P).ramificationIdx A * Nat.card ↥(inertia G P ⊓ H) = P.ramificationIdx A

The ramification index below an intermediate invariant ring, multiplied by the order of the inertia subgroup fixing that ring, is the ramification index over the base. Only the residue extension above the intermediate ring needs to be separable.

theorem Ideal.ramificationIdx_under_eq_relIndex_inertia {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [IsDomain A] [IsDomain B] [IsGaloisGroup G A B] [Module.Finite A B] [Module.Flat A B] (P : Ideal B) [P.IsMaximal] (H : Subgroup G) (C : Type u_4) [CommRing C] [IsDomain C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsGaloisGroup (↥H) C B] [Module.Flat C B] [Algebra.IsSeparable (A ⧸ under A P) (B ⧸ P)] : (under C P).ramificationIdx A = H.relIndex (inertia G P)

The ramification index below an intermediate invariant ring is the relative index of its fixing subgroup in inertia. Separability is required only at the selected prime.

theorem Ideal.ramificationIdx_under_eq_one_iff_inertia_le {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [IsDomain A] [IsDomain B] [IsGaloisGroup G A B] [Module.Finite A B] [Module.Flat A B] (P : Ideal B) [P.IsMaximal] (H : Subgroup G) (C : Type u_4) [CommRing C] [IsDomain C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsGaloisGroup (↥H) C B] [Module.Flat C B] [Algebra.IsSeparable (A ⧸ under A P) (B ⧸ P)] : (under C P).ramificationIdx A = 1 ↔ inertia G P ≤ H

The prime below P in an intermediate invariant ring has ramification index one exactly when every inertia element fixes that ring.

theorem Ideal.ramificationIdx_under_smul_eq_relIndex_inertia {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [IsDomain A] [IsDomain B] [IsGaloisGroup G A B] [Module.Finite A B] [Module.Flat A B] [SMulCommClass G A B] (Q : Ideal B) [Q.IsMaximal] (H : Subgroup G) (C : Type u_4) [CommRing C] [IsDomain C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsGaloisGroup (↥H) C B] [Module.Flat C B] [Algebra.IsSeparable (A ⧸ under A Q) (B ⧸ Q)] (σ : G) : (under C (σ • Q)).ramificationIdx A = H.relIndex (MulAut.conj σ • inertia G Q)

The ramification index below a translate of Q is the relative index of the conjugate inertia group. Separability is required only for the selected residue extension at Q; the group action transports it to every translate.

theorem Ideal.ramificationIdx_under_smul_eq_one_iff_inertia_le {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [IsDomain A] [IsDomain B] [IsGaloisGroup G A B] [Module.Finite A B] [Module.Flat A B] [SMulCommClass G A B] (Q : Ideal B) [Q.IsMaximal] (H : Subgroup G) (C : Type u_4) [CommRing C] [IsDomain C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsGaloisGroup (↥H) C B] [Module.Flat C B] [Algebra.IsSeparable (A ⧸ under A Q) (B ⧸ Q)] (σ : G) : (under C (σ • Q)).ramificationIdx A = 1 ↔ MulAut.conj σ • inertia G Q ≤ H

The contraction of a translated prime has ramification index one exactly when its conjugate inertia group is contained in the subgroup fixing the intermediate ring.

theorem TauCeti.RamificationInertia.ramificationIdx_under_mul_finInsepDegree_eq_relIndex_inertia (A : Type u_1) (C : Type u_2) {B : Type u_3} {G : Type u_4} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [Group G] [MulSemiringAction G B] [IsGaloisGroup G A B] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] (H : Subgroup G) [IsGaloisGroup (↥H) C B] (p : Ideal A) [p.IsMaximal] {P : Ideal B} [P.IsMaximal] [P.LiesOver p] : have this := ⋯; (Ideal.under C P).ramificationIdx A * Field.finInsepDegree (A ⧸ p) (C ⧸ Ideal.under C P) = H.relIndex (Ideal.inertia G P)

The inertia index below an intermediate invariant ring is the ramification index times the inseparable residue degree. This holds even when the upper residue extension is inseparable.