TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Decomposition and inertia fixed fields

Statement

In finite Galois L/K fix nonzero $P ∣ p$ , put $D = D (P / p)$ , $I = I (P / p)$ , $E = L^{D}$ , $U = L^{I}$ , and let $p_{E}, p_{U}$ be the contractions of P. Write $e = e (P / p)$ and $f = f (P / p)$ . Then P is the only prime over $p_{E}$ , and $e (p_{E} / p) = f (p_{E} / p) = 1$ . The extension U/E is cyclic of degree f and is unramified at $p_{U} ∣ p_{E}$ with residue degree f. The extension L/U is totally ramified at $P ∣ p_{U}$ of degree e. If D is normal in $Gal (L / K)$ , p splits completely in E/K. For nonnormal D only the distinguished prime is asserted to have e=f=1. Moreover E is the smallest intermediate field F such that P is the only prime above $P \cap O_{F}$ .

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Decomposition inertia exact sequence: For finite Galois L/K and fixed nonzero $P ∣ p$ , reduction gives the exact sequence $1 ⟶ I (P / p) ⟶ D (P / p) ⟶ Gal (κ (P) / κ (p)) ⟶ 1.$ In particular $D (P / p) / I (P / p)$ is canonically the residue Galois group.

[F2]

Orders of decomposition and inertia groups: For finite Galois L/K and nonzero $P ∣ p$ , writing e and f for its ramification index and residue degree, $∣ D (P / p) ∣ = e f, ∣ I (P / p) ∣ = e, ∣ D (P / p) / I (P / p) ∣ = f .$ The prime P is unramified over p if and only if its inertia group is trivial.

[F3]

Ramification and residue degrees in towers: For $M / L / K$ and $Q ∣ P ∣ p$ , $e (Q / p) = e (Q / P) e (P / p), f (Q / p) = f (Q / P) f (P / p) .$

[F4]

Normal subgroups, conjugate fields, and quotient groups in the Galois correspondence: Let $K / F$ be finite Galois, let $G = Gal (K / F)$ , let $H \leq G$ , and put $E = K^{H}$ . For every $σ \in G$ , $Gal (K / σ (E)) = σ H σ^{- 1} .$ An intermediate field $E / F$ is Galois exactly when its corresponding subgroup is normal. In that case restriction gives a surjective homomorphism $G \to Gal (E / F)$ with kernel $H$ , and hence $Gal (E / F) ≅ G / H .$

[F5]

Galois action on primes above a prime is transitive: Let L/K be a finite Galois extension of number fields and p a nonzero prime of $O_{K}$ . Then $G = Gal (L / K)$ acts transitively on the primes P above p.

Proof

1.1F2F3F5

The group of L/E is D. It acts transitively on primes above $p_{E}$ and fixes P, so P is the unique such prime. For L/E its decomposition group is D and its inertia group is I, directly from their definitions. The order formulas give $e (P / p_{E}) = ∣ I ∣ = e$ and $f (P / p_{E}) = ∣ D ∣ / ∣ I ∣ = f$ . Multiplicativity then gives $e (p_{E} / p) = f (p_{E} / p) = 1$ .

2.1F1F2F3F4F5step 1.1

Since I is normal in D, U/E is Galois with group $D / I$ , cyclic of order f by the residue exact sequence. The group of L/U is I, which fixes P and acts trivially on its residue field. Thus P is unique over $p_{U}$ , $e (P / p_{U}) = ∣ I ∣ = e$ and $f (P / p_{U}) = 1$ . Multiplicativity now gives $e (p_{U} / p_{E}) = 1$ and $f (p_{U} / p_{E}) = f$ . This proves both the unramified middle step and total ramification in the top step.

2.2F4F5step 1.1

If D is normal in G, E/K is Galois. Its group transports $p_{E}$ to every prime above p; such transportation preserves ideal exponents and residue degrees. Each therefore has e=f=1, which is complete splitting. Without normality this transportation conclusion is not used.

3.1F4step 1.1∎

For any intermediate F with uniqueness of P above its contraction, every automorphism in $Gal (L / F)$ fixes P, hence this subgroup lies in D. Taking fixed fields gives $E \subseteq F$ . Conversely E itself has the uniqueness property proved above. Thus it is the smallest such intermediate field.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Chapter 8, Proposition 8.11, p.140; Stein Propositions 9.3.3–9.3.4, pp.104–105 (standard reference, not scraped)