Separable and inseparable residue degrees in Hilbert theory

For a prime P of a finite Galois extension lying over p, the quotient of the decomposition group by inertia acts faithfully on the residue field. The residue extension is normal but need not be separable, so the order of this quotient is its separable degree rather than its full degree. Consequently the inertia group has order e * fᵢ, where fᵢ is the inseparable residue degree.

These formulas are the form of the decomposition and inertia cardinalities that remains valid over an imperfect residue field. When the residue extension is separable, fᵢ = 1 and they specialize to the familiar identities |I| = e and |D| = e * f.

Main results

• Ideal.card_stabilizer_quotient_inertia_eq_finSepDegree: the decomposition quotient has order equal to the separable residue degree.
• Ideal.card_stabilizer_eq_card_inertia_mul_finSepDegree: the decomposition group has order |I| * fₛ.
• Ideal.card_stabilizer_eq_ramificationIdxIn_mul_inertiaDegIn: the decomposition group has order e * f without a residue-separability hypothesis.
• Ideal.card_stabilizer_eq_ramificationIdx_mul_inertiaDeg: the same formula in terms of the ramification index and inertia degree of the upstairs ideal.
• Ideal.card_inertia_eq_ramificationIdxIn_mul_finInsepDegree: the inertia group has order e * fᵢ.
• Ideal.card_inertia_eq_ramificationIdx_mul_finInsepDegree: the same formula in terms of the ramification index of the upstairs ideal.
• Ideal.card_inertia_eq_ramificationIdxIn_of_isSeparable: for a separable residue extension, the familiar identity |I| = e holds without assuming the base residue field is perfect.
• Ideal.card_inertia_eq_ramificationIdx_of_isSeparable: the corresponding upstairs-ideal form.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §9.

These results are the ideal-theoretic analogues of the function-field place cardinality formulas in TauCeti.FieldTheory.FunctionField.Place.Extension.Inertia.

theorem Ideal.card_residueFieldAut_eq_finSepDegree {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] (p : Ideal R) [p.IsMaximal] (P : Ideal S) [P.LiesOver p] [P.IsMaximal] : Nat.card ((S ⧸ P) ≃ₐ[R ⧸ p] S ⧸ P) = Field.finSepDegree (R ⧸ p) (S ⧸ P)

The automorphism group of a residue extension in a finite invariant extension has order its separable degree. The residue extension is normal, but it need not be separable.

theorem Ideal.card_stabilizer_quotient_inertia_eq_finSepDegree {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] (p : Ideal R) [p.IsMaximal] (P : Ideal S) [P.LiesOver p] [P.IsMaximal] : Nat.card (↥(MulAction.stabilizer G P) ⧸ inertia (↥(MulAction.stabilizer G P)) P) = Field.finSepDegree (R ⧸ p) (S ⧸ P)

The quotient of the decomposition group by inertia has order equal to the separable residue degree.

theorem Ideal.card_stabilizer_eq_card_inertia_mul_finSepDegree {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] (p : Ideal R) [p.IsMaximal] (P : Ideal S) [P.LiesOver p] [P.IsMaximal] : Nat.card ↥(MulAction.stabilizer G P) = Nat.card ↥(inertia G P) * Field.finSepDegree (R ⧸ p) (S ⧸ P)

The order of the decomposition group is the order of inertia times the separable residue degree.

theorem Ideal.card_stabilizer_eq_ramificationIdxIn_mul_inertiaDegIn {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S] (p : Ideal R) [p.IsMaximal] (P : Ideal S) [P.LiesOver p] [P.IsMaximal] : Nat.card ↥(MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S

The order of the decomposition group is e * f, without a separability hypothesis on the residue extension.

theorem Ideal.card_stabilizer_eq_ramificationIdx_mul_inertiaDeg {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S] (P : Ideal S) [P.IsMaximal] : Nat.card ↥(MulAction.stabilizer G P) = P.ramificationIdx R * P.inertiaDeg R

The order of the decomposition group is the product of the ramification index and inertia degree of the upstairs ideal.

theorem Ideal.card_inertia_eq_ramificationIdxIn_mul_finInsepDegree {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S] (p : Ideal R) [p.IsMaximal] (P : Ideal S) [P.LiesOver p] [P.IsMaximal] : Nat.card ↥(inertia G P) = p.ramificationIdxIn S * Field.finInsepDegree (R ⧸ p) (S ⧸ P)

Over an imperfect residue field, the inertia group has order e * fᵢ, where fᵢ is the inseparable residue degree.

theorem Ideal.card_inertia_eq_ramificationIdx_mul_finInsepDegree {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S] (P : Ideal S) [P.IsMaximal] : Nat.card ↥(inertia G P) = P.ramificationIdx R * Field.finInsepDegree (R ⧸ under R P) (S ⧸ P)

Over an imperfect residue field, the inertia group has order e * fᵢ, stated using the ramification index of the upstairs ideal.

theorem Ideal.card_inertia_eq_ramificationIdxIn_of_isSeparable {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S] (p : Ideal R) [p.IsMaximal] (P : Ideal S) [P.LiesOver p] [P.IsMaximal] [Algebra.IsSeparable (R ⧸ p) (S ⧸ P)] : Nat.card ↥(inertia G P) = p.ramificationIdxIn S

If the residue extension is separable, the inertia group has order equal to the ramification index. Unlike the standard perfect-residue-field form, this assumes separability only for the one residue extension in the statement.

theorem Ideal.card_inertia_eq_ramificationIdx_of_isSeparable {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] [IsDomain R] [IsDomain S] [Module.Finite R S] [Module.Flat R S] (P : Ideal S) [P.IsMaximal] [Algebra.IsSeparable (R ⧸ under R P) (S ⧸ P)] : Nat.card ↥(inertia G P) = P.ramificationIdx R

If the residue extension is separable, the inertia group has order equal to the ramification index of the upstairs ideal.