The double-coset splitting law over invariant rings

Let a finite group G act on a commutative ring B with invariant ring A, and let C be an intermediate ring of invariants for a subgroup H of G. For a prime Q of B above p in A, contraction identifies the primes of C above p with the double cosets H \ G / D, where D is the stabilizer of Q. The class of σ corresponds to (σ • Q).under C.

This formulation applies to integral closures over an arbitrary Dedekind base, once IsGaloisGroup.of_isIntegralClosure and IsGaloisGroup.of_isIntegralClosure_fixedField supply the invariance, and directly, through instances, to the rings of integers 𝓞 K, 𝓞 M and 𝓞 (M ^ H) of number fields. The bijection itself needs neither a Dedekind hypothesis nor residue-field separability: transitivity on prime fibres and lying over are supplied by Mathlib's invariant-ring theory. The intermediate ring is an explicit parameter, so the same construction works for any realization of the fixed ring, including FixedPoints.subalgebra A B H.

Main definitions

• Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant: the contraction bijection over an invariant ring.

Main results

• Ideal.under_smul_eq_iff_doubleCosetMk_eq: the fibres of translated contraction are exactly the double cosets.
• Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant_mk: the value at a double-coset representative.
• Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant_symm_apply_eq_mk_iff: characterization of the inverse.
• Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant_smul_mk: compatibility with the action of G, moving the base prime Q to τ • Q.
• Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant_natural: enlarging the subgroup agrees with contracting primes to the smaller invariant ring.
• Ideal.ramificationIdx_mul_inertiaDeg_under_eq_relIndex: the local degree below Q is [D(Q) : H ∩ D(Q)], including inseparable residue extensions.
• Ideal.ramificationIdx_under_eq_one_of_stabilizer_le and Ideal.inertiaDeg_under_eq_one_of_stabilizer_le: if D(Q) ≤ H, then Q ∩ C has e = f = 1 over A.
• Ideal.sum_ramificationIdx_mul_inertiaDeg_doubleCosetOfIsInvariant_eq_index: the local degrees indexed by double cosets sum to [G : H].
• Ideal.sum_ramificationIdx_mul_inertiaDeg_doubleCosetOfIsInvariant_eq_finrank: the same sum is the rank of the intermediate invariant ring over the base.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §9, page 55.
• G. J. Janusz, Algebraic Number Fields, Chapter I.

The construction uses Mathlib's Algebra.IsInvariant.exists_smul_of_under_eq and Algebra.IsInvariant.orbit_eq_primesOver, and the rank identity is reindexed from Mathlib's Ideal.sum_ramification_inertia_eq_finrank.

theorem Ideal.under_smul_eq_iff_doubleCosetMk_eq {B : Type u_2} {G : Type u_3} [CommRing B] [Group G] [MulSemiringAction G B] (Q : Ideal B) [Q.IsPrime] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra C B] [Finite ↥H] [Algebra.IsInvariant C B ↥H] [SMulCommClass (↥H) C B] (σ τ : G) : under C (σ • Q) = under C (τ • Q) ↔ DoubleCoset.mk H (MulAction.stabilizer G Q) σ = DoubleCoset.mk H (MulAction.stabilizer G Q) τ

Two translates of a prime contract to the same prime of the H-invariant ring exactly when their translating elements belong to the same H-decomposition double coset.

noncomputable def Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [hAB : Algebra.IsInvariant A B G] [SMulCommClass G A B] (Q : Ideal B) [Q.IsPrime] (p : Ideal A) [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [hCB : FaithfulSMul C B] [Algebra.IsInvariant C B ↥H] [SMulCommClass (↥H) C B] : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer G Q) ≃ ↑(p.primesOver C)

The double-coset splitting law over invariant rings. The primes of the intermediate H-invariant ring C above p are indexed by H \ G / stabilizer G Q. The class of σ is sent to the contraction of σ • Q, without any residue-field hypothesis.

@[simp]

theorem Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant_mk {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [hAB : Algebra.IsInvariant A B G] [SMulCommClass G A B] (Q : Ideal B) [Q.IsPrime] (p : Ideal A) [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [hCB : FaithfulSMul C B] [Algebra.IsInvariant C B ↥H] [SMulCommClass (↥H) C B] (σ : G) : ↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) (DoubleCoset.mk H (MulAction.stabilizer G Q) σ)) = under C (σ • Q)

The class of σ is sent to the contraction of σ • Q.

@[simp]

theorem Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant_symm_apply_eq_mk_iff {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [hAB : Algebra.IsInvariant A B G] [SMulCommClass G A B] (Q : Ideal B) [Q.IsPrime] (p : Ideal A) [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [hCB : FaithfulSMul C B] [Algebra.IsInvariant C B ↥H] [SMulCommClass (↥H) C B] (q : ↑(p.primesOver C)) (σ : G) : (Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C).symm q = DoubleCoset.mk H (MulAction.stabilizer G Q) σ ↔ ↑q = under C (σ • Q)

The inverse sends a prime q to the class of σ exactly when q is the contraction of σ • Q. This characterizes the inverse without exposing the choice of a prime above q.

theorem Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant_smul_mk {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [hAB : Algebra.IsInvariant A B G] [SMulCommClass G A B] (Q : Ideal B) [Q.IsPrime] (p : Ideal A) [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [hCB : FaithfulSMul C B] [Algebra.IsInvariant C B ↥H] [SMulCommClass (↥H) C B] (τ σ : G) : ((τ • Q).doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) (DoubleCoset.mk H (MulAction.stabilizer G (τ • Q)) σ) = (Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) (DoubleCoset.mk H (MulAction.stabilizer G Q) (σ * τ))

The double-coset law is compatible with the action of G. Indexing the primes of C above p through the translate τ • Q instead of Q sends the class of σ to the prime that the indexing through Q attaches to the class of σ * τ.

theorem Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant_natural {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [hAB : Algebra.IsInvariant A B G] [SMulCommClass G A B] (Q : Ideal B) [Q.IsPrime] (p : Ideal A) [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [hCB : FaithfulSMul C B] [Algebra.IsInvariant C B ↥H] [SMulCommClass (↥H) C B] {H' : Subgroup G} (h : H ≤ H') (C' : Type u_5) [CommRing C'] [Algebra A C'] [Algebra C' C] [Algebra C' B] [IsScalarTower A C' B] [IsScalarTower C' C B] [FaithfulSMul C' B] [Algebra.IsInvariant C' B ↥H'] [SMulCommClass (↥H') C' B] (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer G Q)) : ↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H' C') (DoubleCoset.quotientMapOfLELeft h (MulAction.stabilizer G Q) q)) = under C' ↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)

Enlarging the subgroup and contracting to its invariant ring give the same prime under the double-coset splitting bijection. The scalar towers express the two inclusions of C' into B through A and C.

theorem Ideal.ramificationIdx_mul_inertiaDeg_under_eq_relIndex {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] (Q : Ideal B) [Q.IsMaximal] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsDomain A] [IsDomain B] [IsDomain C] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] [IsGaloisGroup G A B] [IsGaloisGroup (↥H) C B] : (under C Q).ramificationIdx A * (under C Q).inertiaDeg A = H.relIndex (MulAction.stabilizer G Q)

The local-degree index formula over invariant rings. The ramification index times residue degree of the contraction to an intermediate H-invariant ring is the index of H ∩ D(Q) in D(Q). No separability hypothesis on the residue extension is needed.

theorem Ideal.ramificationIdx_mul_inertiaDeg_under_smul_eq_relIndex {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] (Q : Ideal B) [Q.IsMaximal] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsDomain A] [IsDomain B] [IsDomain C] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] [IsGaloisGroup G A B] [IsGaloisGroup (↥H) C B] (sigma : G) : (under C (sigma • Q)).ramificationIdx A * (under C (sigma • Q)).inertiaDeg A = H.relIndex (MulAut.conj sigma • MulAction.stabilizer G Q)

The local degree below a translate of Q is the relative index of the conjugate decomposition group.

theorem Ideal.ramificationIdx_under_eq_one_of_stabilizer_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] (Q : Ideal B) [Q.IsMaximal] {H : Subgroup G} (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsDomain A] [IsDomain B] [IsDomain C] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] [IsGaloisGroup G A B] [IsGaloisGroup (↥H) C B] (hH : MulAction.stabilizer G Q ≤ H) : (under C Q).ramificationIdx A = 1

Above the decomposition group the ramification index is one. If H contains the decomposition group D(Q), then the prime Q ∩ C of the H-invariant ring C has ramification index one over A. No hypothesis on the residue extension is needed.

theorem Ideal.inertiaDeg_under_eq_one_of_stabilizer_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] (Q : Ideal B) [Q.IsMaximal] {H : Subgroup G} (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [IsDomain A] [IsDomain B] [IsDomain C] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] [IsGaloisGroup G A B] [IsGaloisGroup (↥H) C B] (hH : MulAction.stabilizer G Q ≤ H) : (under C Q).inertiaDeg A = 1

Above the decomposition group the residue degree is one. If H contains the decomposition group D(Q), then the prime Q ∩ C of the H-invariant ring C has residue degree one over A. No hypothesis on the residue extension is needed.

theorem Ideal.ramificationIdx_mul_inertiaDeg_under_smul_mul_card {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] (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] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] [IsGaloisGroup G A B] [IsGaloisGroup (↥H) C B] (sigma : G) : (under C (sigma • Q)).ramificationIdx A * (under C (sigma • Q)).inertiaDeg A * Nat.card ↥H = Nat.card ↑(DoubleCoset.doubleCoset sigma ↑H ↑(MulAction.stabilizer G Q))

The local degree below a translate, multiplied by |H|, is the cardinality of its double coset.

theorem Ideal.ramificationIdx_mul_inertiaDeg_doubleCosetQuotientEquivPrimesOverOfIsInvariant_mul_card {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [IsDomain A] [IsDomain B] (p : Ideal A) (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] [IsGaloisGroup G A B] [IsGaloisGroup (↥H) C B] [FaithfulSMul C B] (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer G Q)) : (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).ramificationIdx A * (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).inertiaDeg A * Nat.card ↥H = Nat.card ↑(DoubleCoset.quotToDoubleCoset H (MulAction.stabilizer G Q) q)

The local degree of the prime attached to a double coset, multiplied by |H|, is the cardinality of that double coset.

theorem Ideal.ramificationIdx_mul_inertiaDeg_doubleCosetQuotientEquivPrimesOverOfIsInvariant_eq_card_div {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [IsDomain A] [IsDomain B] (p : Ideal A) (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] [IsGaloisGroup G A B] [IsGaloisGroup (↥H) C B] [FaithfulSMul C B] (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer G Q)) : (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).ramificationIdx A * (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).inertiaDeg A = Nat.card ↑(DoubleCoset.quotToDoubleCoset H (MulAction.stabilizer G Q) q) / Nat.card ↥H

The local degree of the prime attached to a double coset is its cardinality divided by the order of H.

theorem Ideal.sum_ramificationIdx_mul_inertiaDeg_doubleCosetOfIsInvariant_eq_index {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [IsDomain A] [IsDomain B] (p : Ideal A) (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [Module.Finite A B] [Module.Flat A B] [Module.Flat C B] [IsGaloisGroup G A B] [IsGaloisGroup (↥H) C B] [FaithfulSMul C B] : ∑ᶠ (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer G Q)), (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).ramificationIdx A * (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).inertiaDeg A = H.index

The local degrees indexed by the invariant-ring double-coset law sum to the index of H in G.

theorem Ideal.sum_ramificationIdx_mul_inertiaDeg_doubleCosetOfIsInvariant_eq_finrank {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Finite G] [Algebra.IsInvariant A B G] [SMulCommClass G A B] (p : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [FaithfulSMul C B] [Algebra.IsInvariant C B ↥H] [SMulCommClass (↥H) C B] [IsDomain A] [Module.Finite A C] [Module.Flat A C] : ∑ᶠ (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer G Q)), (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).ramificationIdx A * (↑((Q.doubleCosetQuotientEquivPrimesOverOfIsInvariant p H C) q)).inertiaDeg A = Module.finrank A C

The fundamental identity in invariant-ring double-coset coordinates. The local degrees of the primes of C above p sum to the rank of C over A.