The double coset law over a Dedekind base #
Let A be a domain with fraction field K, let M / K be a finite Galois extension with group
G = Gal(M/K), and let B be the integral closure of A in M. For a subgroup H of G, let
C be the integral closure of A in the fixed field M ^ H, an intermediate field that need not
be Galois over K. Fix a prime p of A and a prime Q of B above it, with decomposition
group D. The primes of C above p are indexed by the double cosets H \ G / D, the class of
σ corresponding to the contraction σ Q ∩ C.
This is the double coset law for an arbitrary integrally closed base, with no hypothesis on the
residue fields. Over a Dedekind base the local invariants of the prime 𝔮_σ = σ Q ∩ C are read
off the double coset:
e(𝔮_σ / p) · f(𝔮_σ / p) = [σDσ⁻¹ : H ∩ σDσ⁻¹], so thate · f · |H| = |HσD|;e(𝔮_σ / p) = [σIσ⁻¹ : H ∩ σIσ⁻¹]when the residue extension atQis separable, whereIis the inertia group ofQ;- the products
e · fsum, overH \ G / D, to[M ^ H : K].
Finite residue fields are never assumed. The statements specialize the invariant-ring double
coset law of TauCeti.NumberTheory.RamificationInertia.DoubleCoset.Invariant.Basic and
TauCeti.NumberTheory.RamificationInertia.DoubleCoset.Invariant.Inertia: the work here is to
recognize G and H as Galois groups of the integral closures, via
IsGaloisGroup.of_isIntegralClosure and IsGaloisGroup.of_isIntegralClosure_fixedField,
and to supply the finiteness and flatness that a Dedekind base provides, via
IsIntegralClosure.finite and TauCeti.IsIntegralClosure.flat. Rings of integers of
number fields are the case A = 𝓞 K, B = 𝓞 M, C = 𝓞 (M ^ H).
Main definitions #
Ideal.doubleCosetQuotientEquivPrimesOverOfIsIntegralClosure: the bijectionH \ G / D ≃ p.primesOver C.
Main results #
Ideal.doubleCosetQuotientEquivPrimesOverOfIsIntegralClosure_mk: the class ofσis sent toσ Q ∩ C.Ideal.ramificationIdx_mul_inertiaDeg_under_smul_eq_relIndex_of_isIntegralClosure:e · f = [σDσ⁻¹ : H ∩ σDσ⁻¹].Ideal.ramificationIdx_mul_inertiaDeg_under_smul_mul_card_of_isIntegralClosure:e · f · |H| = |HσD|.Ideal.ramificationIdx_under_smul_eq_relIndex_inertia_of_isIntegralClosure:e = [σIσ⁻¹ : H ∩ σIσ⁻¹]for a separable residue extension.Ideal.sum_ramificationIdx_mul_inertiaDeg_doubleCosetOfIsIntegralClosure_eq_finrank: the fundamental identityΣ e · f = [M ^ H : K]indexed by double cosets.
The same canonical API also includes naturality under enlarging the subgroup and equivariance under translating the chosen prime, together with the decomposition-group and inertia-group formulas evaluated directly on a double coset. Naturality and equivariance only require an integrally closed base; the local-invariant formulas require a Dedekind base.
References #
- [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, §9, page 55.
- G. J. Janusz, Algebraic Number Fields, Chapter I.
The double coset law over an integrally closed base. For M / K finite Galois with
group G, a subgroup H of G, the integral closures B and C of A in M and in M ^ H,
and a prime Q of B above p with decomposition group D, the primes of C above p are
indexed by the double cosets H \ G / D.
The class of σ corresponds to the contraction σ Q ∩ C, by
Ideal.doubleCosetQuotientEquivPrimesOverOfIsIntegralClosure_mk.
Instances For
The double coset law sends the class of σ to the contraction σ Q ∩ C.
The inverse of the double coset law sends a prime q to the class of σ exactly when q is
the contraction σ Q ∩ C.
Changing the chosen prime from Q to τ • Q agrees with right multiplication of
representatives by τ. The action on the integral closure may be any compatible action
commuting with the base ring, including the canonical restricted Galois action.
Enlarging the subgroup and contracting to its integral closure give the same prime under the integral-closure double-coset bijection.
The local degree of σ Q ∩ C is an index of decomposition groups:
e · f = [σDσ⁻¹ : H ∩ σDσ⁻¹], where D is the decomposition group of the maximal ideal Q.
No separability of the residue extension is needed.
The local degree of σ Q ∩ C counts the double coset HσD: e · f · |H| = |HσD|,
where D is the decomposition group of the maximal ideal Q.
The ramification index of σ Q ∩ C is an index of inertia groups:
e = [σIσ⁻¹ : H ∩ σIσ⁻¹], where I is the inertia group of the maximal ideal Q, provided the
residue extension of Q over p is separable. The residue fields need not be finite.
The fundamental identity in double-coset coordinates. The ramification indices times the
residue degrees of the primes of C above p, indexed by H \ G / D, sum to [M ^ H : K].
The local degree of the prime attached to a double coset is the relative index of its conjugate decomposition group. Residue separability is not required.
Under residue separability, the ramification index of the prime attached to a double coset is the relative index of its conjugate inertia group.