Ramification and inertia in Galois extensions

This file records Galois consequences of the fundamental identity for primes in finite extensions of domains. First, in a Galois extension the number of primes above a prime ideal is maximal exactly when the common ramification index and inertia degree are both 1, and, by orbit–stabilizer alone, exactly when the decomposition group of one (equivalently, every) prime above it is trivial; neither criterion needs separability of the residue extensions. Second, the cardinality of the inertia subgroup of a prime P upstairs is the ramification index of P itself over the base, rather than the Ideal.ramificationIdxIn of the prime below it.

The rest of the file is about how unramifiedness and inertia subgroups vary with the prime. Translating a prime by σ preserves unramifiedness and conjugates its inertia subgroup by σ. Because the Galois group acts transitively on the primes above a fixed prime of the base, unramifiedness at one of them gives it at all of them, and when one of their inertia subgroups is normal (for instance when the Galois group is commutative) they all share that inertia subgroup. That uniformity is what lets a statement about ramification in an intermediate field be tested at a single prime upstairs.

The number-field specialization also compares the galRestrict action on primes over a base ideal with the pointwise ideal action on the ring of integers, including stabilizers and transitivity.

Main results

• TauCeti.coe_galRestrict_eq_toRingHom: restriction agrees with the canonical action.

• TauCeti.coe_smul_primesOver_ringOfIntegers and TauCeti.stabilizer_primesOver_ringOfIntegers: the primes-over action and its stabilizers agree with those on the underlying ideals.

• TauCeti.isPretransitive_primesOver_ringOfIntegers: transitivity for Galois extensions.

• TauCeti.primesAboveRingOfIntegersMulAction and TauCeti.sigmaPrimesOverEquivPrimesAbove_smul: the canonical primes-above action and its equivariant comparison with the fibre indexing.

• TauCeti.asIdeal_smul_primesAbove_ringOfIntegers: the induced action on underlying ideals.

• Ideal.ncard_primesOver_eq_natCard_iff_of_isGaloisGroup: the domain/flat Galois counting criterion.

• Ideal.ncard_primesOver_eq_natCard_iff_stabilizer_eq_bot, Ideal.ncard_primesOver_eq_natCard_iff_forall_stabilizer_eq_bot: the same count is maximal exactly when the decomposition groups above the prime are trivial.

• Ideal.stabilizer_eq_bot_iff_ramificationIdxIn_eq_one_and_inertiaDegIn_eq_one: a decomposition group is trivial exactly when e = f = 1.

• Ideal.card_inertia_eq_ramificationIdx: the un-In form of the inertia count.

• Ideal.isUnramifiedAt_pointwise_smul_iff: unramifiedness is invariant under translation by an algebra automorphism.

• Ideal.isUnramifiedAt_of_isUnramifiedAt_of_isGaloisGroup: unramifiedness transfers between primes above the same base prime in a Galois extension.

• Ideal.mem_inertia_pointwise_smul_iff: translation conjugates inertia subgroups.

• Ideal.inertia_pointwise_smul: translation leaves a normal inertia subgroup unchanged.

• Ideal.inertia_eq_of_liesOver: when one of them is normal, all the primes above a fixed prime of the base have the same inertia subgroup.

Provenance

Built directly on Mathlib's Galois fundamental identity (Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn), on its description of the primes above a prime as one orbit (Algebra.IsInvariant.orbit_eq_primesOver) together with orbit–stabilizer (MulAction.index_stabilizer), on its inertia count (Ideal.card_inertia_eq_ramificationIdxIn), on its conjugation formula for inertia subgroups (Ideal.inertia_smul) and on its transitivity statement (Ideal.exists_smul_eq_of_isGaloisGroup), together with the transport of unramifiedness along algebra isomorphisms AlgEquiv.isUnramifiedAt_of_eq_comap.

theorem Ideal.ncard_primesOver_eq_natCard_iff_of_isGaloisGroup {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.Finite A B] [Module.Flat A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (P : Ideal A) [P.IsPrime] : (P.primesOver B).ncard = Nat.card G ↔ P.ramificationIdxIn B = 1 ∧ P.inertiaDegIn B = 1

In a finite flat Galois extension of domains, the number of primes over a prime ideal equals the order of the Galois group iff the common ramification index and inertia degree are both 1.

theorem Ideal.ncard_primesOver_eq_natCard_iff_stabilizer_eq_bot {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] : (P.primesOver B).ncard = Nat.card G ↔ MulAction.stabilizer G Q = ⊥

Complete splitting through the decomposition group. If G acts on B with invariants A, then the number of primes of B over P equals the order of G exactly when the decomposition group stabilizer G Q of one prime Q over P is trivial. This is orbit–stabilizer for the transitive action of G on the primes over P; no hypothesis on the residue extensions is needed.

theorem Ideal.ncard_primesOver_eq_natCard_iff_forall_stabilizer_eq_bot {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] [Algebra.IsInvariant A B G] [FaithfulSMul A B] (P : Ideal A) [P.IsPrime] : (P.primesOver B).ncard = Nat.card G ↔ ∀ Q ∈ P.primesOver B, MulAction.stabilizer G Q = ⊥

Complete splitting through all decomposition groups. If G acts on B with invariants A, then the number of primes of B over a prime P of A equals the order of G exactly when the decomposition group of every prime over P is trivial.

theorem Ideal.stabilizer_eq_bot_iff_ramificationIdxIn_eq_one_and_inertiaDegIn_eq_one {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.Finite A B] [Module.Flat A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] (P : Ideal A) [P.IsPrime] (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] : MulAction.stabilizer G Q = ⊥ ↔ P.ramificationIdxIn B = 1 ∧ P.inertiaDegIn B = 1

The decomposition group is trivial exactly when e = f = 1. In a finite flat Galois extension of domains, the decomposition group of a prime Q over P is trivial exactly when the common ramification index and inertia degree over P are both 1. Unlike Ideal.card_stabilizer_eq, this needs no separability of the residue extension.

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

The cardinality of the inertia subgroup of P is the ramification index of P over R. This is Ideal.card_inertia_eq_ramificationIdxIn stated with the ramification index of P itself rather than with Ideal.ramificationIdxIn of the ideal below it.

@[simp]

theorem Ideal.isUnramifiedAt_pointwise_smul_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {G : Type u_3} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (Q : Ideal S) [Q.IsPrime] (g : G) : Algebra.IsUnramifiedAt R (g • Q) ↔ Algebra.IsUnramifiedAt R Q

Unramifiedness is invariant under algebra automorphisms. Translating a prime by an R-algebra action automorphism preserves unramifiedness over R.

theorem Ideal.isUnramifiedAt_of_isUnramifiedAt_of_isGaloisGroup {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P Q : Ideal B) [P.IsPrime] [P.LiesOver p] [Q.IsPrime] [Q.LiesOver p] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] [Algebra.IsUnramifiedAt A P] : Algebra.IsUnramifiedAt A Q

Unramifiedness at one prime above p implies unramifiedness at every prime above p when the Galois group acts transitively on them.

theorem Ideal.mem_inertia_pointwise_smul_iff {S : Type u_1} [Ring S] {G : Type u_2} [Group G] [MulSemiringAction G S] {σ τ : G} {P : Ideal S} : τ ∈ inertia G (σ • P) ↔ σ⁻¹ * τ * σ ∈ inertia G P

Inertia is conjugated by the Galois action. An element τ lies in the inertia subgroup of the translated ideal σ • P exactly when its conjugate σ⁻¹ τ σ lies in the inertia subgroup of P.

@[simp]

theorem Ideal.inertia_pointwise_smul {S : Type u_1} [Ring S] {G : Type u_2} [Group G] [MulSemiringAction G S] (σ : G) (P : Ideal S) [(inertia G P).Normal] : inertia G (σ • P) = inertia G P

Translation leaves a normal inertia subgroup unchanged. This applies in particular to every inertia subgroup of a commutative group.

theorem Ideal.inertia_eq_of_liesOver {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P Q : Ideal B) [P.IsPrime] [P.LiesOver p] [Q.IsPrime] [Q.LiesOver p] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B] [(inertia G P).Normal] : inertia G P = inertia G Q

The primes over a fixed prime share a normal inertia subgroup. In a Galois extension, if the inertia subgroup of one prime P above p is normal (for instance when the Galois group is commutative), then every prime Q above p has the same inertia subgroup.

theorem TauCeti.coe_galRestrict_eq_toRingHom (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (σ : Gal(L/K)) : ↑((galRestrict (NumberField.RingOfIntegers K) K L (NumberField.RingOfIntegers L)) σ) = MulSemiringAction.toRingHom Gal(L/K) (NumberField.RingOfIntegers L) σ

Restriction to rings of integers agrees with the canonical Galois action.

@[simp]

theorem TauCeti.coe_smul_primesOver_ringOfIntegers (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] {p : Ideal (NumberField.RingOfIntegers K)} (σ : Gal(L/K)) (P : ↑(p.primesOver (NumberField.RingOfIntegers L))) : ↑(σ • P) = σ • ↑P

The action on primes above a base ideal agrees with the action on their underlying ideals.

@[simp]

theorem TauCeti.stabilizer_primesOver_ringOfIntegers (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] {p : Ideal (NumberField.RingOfIntegers K)} (P : ↑(p.primesOver (NumberField.RingOfIntegers L))) : MulAction.stabilizer Gal(L/K) P = MulAction.stabilizer Gal(L/K) ↑P

A prime above a base ideal has the same stabilizer as its underlying ideal.

instance TauCeti.isPretransitive_primesOver_ringOfIntegers (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] {p : Ideal (NumberField.RingOfIntegers K)} : MulAction.IsPretransitive Gal(L/K) ↑(p.primesOver (NumberField.RingOfIntegers L))

The Galois group acts transitively on primes above any fixed base ideal.

@[instance_reducible]

noncomputable instance TauCeti.primesAboveRingOfIntegersMulAction (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : MulAction Gal(L/K) ↑(IsDedekindDomain.HeightOneSpectrum.primesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) S)

The automorphism action on primes above a set, transported from the primes-over fibres.

Equations

• TauCeti.primesAboveRingOfIntegersMulAction K L S = Equiv.mulAction Gal(L/K) (TauCeti.sigmaPrimesOverEquivPrimesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) S).symm

@[simp]

theorem TauCeti.sigmaPrimesOverEquivPrimesAbove_smul (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (σ : Gal(L/K)) (p : (v : ↑S) × ↑((↑v).asIdeal.primesOver (NumberField.RingOfIntegers L))) : (sigmaPrimesOverEquivPrimesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) S) (σ • p) = σ • (sigmaPrimesOverEquivPrimesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) S) p

The canonical primes-above carrier and its fibre reindexing are equivariantly equivalent.

@[simp]

theorem TauCeti.asIdeal_smul_primesAbove_ringOfIntegers (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (σ : Gal(L/K)) (w : ↑(IsDedekindDomain.HeightOneSpectrum.primesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) S)) : (↑(σ • w)).asIdeal = σ • (↑w).asIdeal

On underlying ideals, the primes-above action is the canonical pointwise ideal action.