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 group and completion

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let L/K be finite Galois and $P ∣ p$ nonzero primes. Then $L_{P} / K_{p}$ is finite Galois of degree $e (P / p) f (P / p)$ . Continuous extension gives a canonical isomorphism $D (P / p) ≅ Gal (L_{P} / K_{p}),$ whose inverse restricts an automorphism to the embedded copy of L.

Facts & Assumptions

Given: The Axiom of Choice and the data and hypotheses of the statement.

[A1]

AC has the meaning fixed in The Axiom of Choice.

[F1]

Decomposition group of a prime: For finite Galois L/K and a chosen nonzero prime $P ∣ p$ , the decomposition group is the stabilizer $D (P / p) = {σ \in Gal (L / K) : σ (P) = P} .$ It is a subgroup: identity stabilizes P and stabilizers are closed under composition and inverse. The prime P, not just p, is part of the data.

[F2]

Number field completions as local polynomial factors: Let L/K be a finite separable extension of number fields, $L = K (α)$ with monic minimal polynomial F, and p a finite prime of K. Factor F over $K_{p}$ into distinct monic irreducibles $F_{i}$ . Then $L \otimes_{K} K_{p} ≅ \prod_{i} K_{p} [T] / (F_{i}) ≅ \prod_{P ∣ p} L_{P}, \sum_{P ∣ p} [L_{P} : K_{p}] = [L : K] .$ Use extending absolute values on each factor; their positive powers give the normalized number-field completions. Under this product, local multiplication matrices give $N_{L / K} (x) = \prod_{P ∣ p} N_{L_{P} / K_{p}} (x)$ and ${Tr}_{L / K} (x) = \sum_{P ∣ p} {Tr}_{L_{P} / K_{p}} (x)$ , with values embedded in $K_{p}$ .

[F3]

Galois prime decomposition efg: For a finite Galois extension L/K and nonzero prime p, every P above p has the same ramification index e and residue degree f. If there are g such primes, then $e f g = [L : K]$ .

[F4]

Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection: Let $G$ act on $X$ and let $x \in X$ . The rule $Φ : G / G_{x} ⟶ G \cdot x, Φ (g G_{x}) = g \cdot x,$ is well-defined and bijective. Thus every orbit is naturally in bijection with the left cosets of its stabilizer.

[F5]

Galois action on primes above a prime is transitive: In a finite Galois extension of number fields, the Galois group acts transitively on the primes above a fixed nonzero prime of the base.

Proof

1.1A1F1

Under [A1], every element of D preserves ${ord}_{P}$ , so preserves the absolute value at P and extends uniquely to the completion. It fixes $K_{p}$ by density of K. Extension is an injective homomorphism since L embeds in its completion.

1.2A1F2

Under [A1], write $L = K (α)$ . The local factor description gives $L_{P} = K_{p} (α)$ and a separable minimal polynomial over $K_{p}$ dividing the global minimal polynomial. Since L/K is normal, all global roots already lie in L. Thus the local polynomial splits in $L_{P}$ , which proves that this finite extension is Galois.

2.1F2F3F4F5step 1.1step 1.2

For each prime Q above p the injection in the first step gives $∣ D (Q / p) ∣ \leq [L_{Q} : K_{p}]$ . Transitivity identifies all stabilizer orders with $∣ G ∣ / g$ by orbit-stabilizer. Summing these inequalities over the g primes gives $∣ G ∣ \leq \sum_{Q} [L_{Q} : K_{p}] = [L : K] = ∣ G ∣$ . Thus every inequality is equality. In particular the injection at P accounts for every local automorphism, since the local extension is Galois. Each is consequently the continuous extension of a unique element of D; its restriction is that element.

3.1F3F4step 1.1step 2.1∎

Orbit-stabilizer on the transitive prime set gives $∣ D ∣ = ∣ G ∣ / g$ . Since $e f g = [L : K] = ∣ G ∣$ , this order, and therefore the local Galois degree, is ef. If L=K the maps and groups are identities.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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.10, p.139 (standard reference, not scraped)