Decomposition-group orbits on cosets and the primes of an invariant ring

Let a finite group G act on a commutative ring B with invariant ring A, let H be a subgroup of G with invariant ring C between A and B, and let Q be a prime of B above a prime p of A, with decomposition group D. The double coset law Ideal.doubleCosetQuotientEquivPrimesOverOfIsInvariant indexes the primes of C above p by H \ G / D. This file reads the same law on the left cosets G ⧸ H, where D acts by translation: the coset τ H is attached to the prime τ⁻¹ Q ∩ C (Ideal.primesOverOfCoset), two cosets are attached to the same prime exactly when they lie in one D-orbit, and every prime arises. When Q is maximal, B is a finite flat A-algebra and a flat C-algebra, and G and H are Galois groups of the domain B over A and over C, the D-orbit of τ H has e · f elements, where e and f are the ramification index and the residue degree of the attached prime over p. Altogether, the multiset of the sizes of the D-orbits on G ⧸ H is the multiset of the local degrees e · f over the primes of C above p. No hypothesis on the residue fields is needed.

This is the form of the double coset law that Dedekind's theorem uses: when M / K is a finite Galois extension and C is the integral closure of the base in M ^ H = K(α), for a root α of an irreducible polynomial, G ⧸ H is the set of roots. If moreover p is unramified in C, so that every e is 1, and D is generated by a Frobenius element, then the orbit sizes of that Frobenius on the roots are the residue degrees of the primes of C above p. Rings of integers of number fields are the case A = 𝓞 K, B = 𝓞 M, C = 𝓞 (M ^ H), where every algebraic hypothesis below is found by instance search.

Main definitions

• Ideal.primesOverOfCoset: the prime τ⁻¹ Q ∩ C attached to the coset τ H.
• Ideal.orbitQuotientEquivPrimesOver: the orbits of the decomposition group on G ⧸ H are the primes of C above p.

Main results

• Ideal.primesOverOfCoset_eq_iff: the fibres of primesOverOfCoset are the orbits of the decomposition group of Q.
• Ideal.primesOverOfCoset_surjective: every prime of C above p is attached to a coset.
• Ideal.card_orbit_stabilizer_coset: the orbit of a coset under the decomposition group has e · f elements, for the prime attached to the coset.
• Ideal.map_card_orbit_stabilizer_eq_map_ramificationIdx_mul_inertiaDeg: the multiset of orbit sizes is the multiset of local degrees over the primes of C above p.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, §9.
• G. J. Janusz, Algebraic Number Fields, Chapter I.

noncomputable def Ideal.primesOverOfCoset {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [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] [SMulCommClass (↥H) C B] : G ⧸ H → ↑(p.primesOver C)

The prime of the H-invariant ring C above p attached to a coset τ H: the contraction τ⁻¹ Q ∩ C. It does not depend on the representative τ, because H acts C-linearly and so does not move contractions to C.

@[simp]

theorem Ideal.coe_primesOverOfCoset_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] [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] [SMulCommClass (↥H) C B] (τ : G) : ↑(p.primesOverOfCoset Q H C ↑τ) = under C (τ⁻¹ • Q)

The prime attached to the coset of τ is the contraction of τ⁻¹ Q.

theorem Ideal.primesOverOfCoset_eq_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] [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] [SMulCommClass (↥H) C B] [Finite ↥H] [Algebra.IsInvariant C B ↥H] (x y : G ⧸ H) : p.primesOverOfCoset Q H C x = p.primesOverOfCoset Q H C y ↔ x ∈ MulAction.orbit (↥(MulAction.stabilizer G Q)) y

The fibres are the orbits of the decomposition group. Two cosets are attached to the same prime of C exactly when one is a translate of the other by the decomposition group of Q.

theorem Ideal.primesOverOfCoset_surjective {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [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] [SMulCommClass (↥H) C B] [Finite G] [Algebra.IsInvariant A B G] [FaithfulSMul C B] : Function.Surjective (p.primesOverOfCoset Q H C)

Every prime of C above p is attached to a coset.

noncomputable def Ideal.orbitQuotientEquivPrimesOver {A : Type u_1} {B : Type u_2} {G : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [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] [SMulCommClass (↥H) C B] [Finite G] [Algebra.IsInvariant A B G] [FaithfulSMul C B] [Algebra.IsInvariant C B ↥H] : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer G Q)) (G ⧸ H) ≃ ↑(p.primesOver C)

The orbits of the decomposition group on G ⧸ H are the primes of C above p: the map primesOverOfCoset, which is constant on the orbits of the decomposition group of Q and identifies exactly them, descends to a bijection from the orbit quotient.

@[simp]

theorem Ideal.orbitQuotientEquivPrimesOver_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] [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] [SMulCommClass (↥H) C B] [Finite G] [Algebra.IsInvariant A B G] [FaithfulSMul C B] [Algebra.IsInvariant C B ↥H] (x : G ⧸ H) : (p.orbitQuotientEquivPrimesOver Q H C) (Quotient.mk'' x) = p.primesOverOfCoset Q H C x

The orbit of a coset is sent to the prime attached to the coset.

theorem Ideal.card_orbit_stabilizer_coset {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] [Module.Finite A B] [Module.Flat A B] [IsGaloisGroup G A B] (p : Ideal A) (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [IsDomain C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [Module.Flat C B] [IsGaloisGroup (↥H) C B] (x : G ⧸ H) : Nat.card ↑(MulAction.orbit (↥(MulAction.stabilizer G Q)) x) = (↑(p.primesOverOfCoset Q H C x)).ramificationIdx A * (↑(p.primesOverOfCoset Q H C x)).inertiaDeg A

Orbit sizes are local degrees. The orbit of a coset under the decomposition group of Q has as many elements as the ramification index times the residue degree of the prime of C attached to the coset. No hypothesis on the residue fields is needed.

theorem Ideal.map_card_orbit_stabilizer_eq_map_ramificationIdx_mul_inertiaDeg {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] [Module.Finite A B] [Module.Flat A B] [IsGaloisGroup G A B] (p : Ideal A) (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver p] (H : Subgroup G) (C : Type u_4) [CommRing C] [IsDomain C] [Algebra A C] [Algebra C B] [IsScalarTower A C B] [Module.Flat C B] [IsGaloisGroup (↥H) C B] [FaithfulSMul C B] [Fintype (MulAction.orbitRel.Quotient (↥(MulAction.stabilizer G Q)) (G ⧸ H))] [Fintype ↑(p.primesOver C)] : Multiset.map (fun (ω : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer G Q)) (G ⧸ H)) => Nat.card ↑ω.orbit) Finset.univ.val = Multiset.map (fun (𝔮 : ↑(p.primesOver C)) => (↑𝔮).ramificationIdx A * (↑𝔮).inertiaDeg A) Finset.univ.val

The multiset of orbit sizes is the multiset of local degrees. The sizes of the orbits of the decomposition group of Q on G ⧸ H are, as a multiset, the products e · f of the ramification index and the residue degree over the primes of C above p.