Alphabeta Math
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 in towers

Statement

Let M/L/K be a tower of number fields with M/K and L/K finite Galois, and fix nonzero primes Q∣P∣p. With H=Gal⁡(M/L), D(Q/P)=D(Q/p)∩H,I(Q/P)=I(Q/p)∩H. Restriction gives exact sequences 1→D(Q/P)→D(Q/p)→D(P/p)→1, 1→I(Q/P)→I(Q/p)→I(P/p)→1. The intersection identities also hold without L/K Galois; the displayed quotient assertions use that hypothesis.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Conjugacy of decomposition and inertia groups: In finite Galois L/K, if σP=P′ above a nonzero p, then D(P′/p)=σD(P/p)σ−1,I(P′/p)=σI(P/p)σ−1. The residue actions correspond under κ(P)→κ(P′), aˉ↦σa‾.

[F2]

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 OK. Then G=Gal⁡(L/K) acts transitively on the primes P above p.

[F3]

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)∣=ef,∣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.

[F4]

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).

[F5]

Normal subgroups, conjugate fields, and quotient groups in the Galois correspondence: Let K/F be finite Galois, let G=Gal⁡(K/F), let H≤G, and put E=KH. For every σ∈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→Gal⁡(E/F) with kernel H, and hence Gal⁡(E/F)≅G/H.

Proof

1.1F1

Within H, fixing Q is exactly the decomposition condition over either base. Acting trivially on κ(Q) is likewise independent of which base is named. These prove both intersections. Restriction from D lands in D(P/p), and restriction from I lands in I(P/p), since integral elements of L are integral elements of M.

2.1F2F5step 1.1

Given τ∈D(P/p), normality of L/K gives a lift σ∈Gal⁡(M/K). Both σQ and Q lie over P. Transitivity for the Galois extension M/L gives h∈H with hσQ=Q. Then hσ lies in D(Q/p) and restricts to tau. Its restriction kernel is the first intersection, proving the first exact sequence.

3.1F3F4step 1.1∎

The restriction image of I(Q/p) has order ∣I(Q/p)∣/∣I(Q/P)∣=e(Q/p)/e(Q/P)=e(P/p). This uses multiplicativity and positive ramification indices. The target I(P/p) has exactly that order, so the image equals the target. Together with the second intersection this proves the second exact sequence.

Depends on

Used by

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