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.
Dedekind--Kummer prime factorisation
Statement
Let be a finite extension of number fields, let with , and let be its monic minimal polynomial over . Let be a nonzero prime ideal of , not dividing the index of this power order (the index is under the stated monogeneity hypothesis). If with distinct monic irreducibles over , then Here are any monic lifts of , and the last denotes the residue degree from Primes above and residue degree.
Proof
Given: monogeneity, the index hypothesis, and the displayed factorisation.
Put , and . Monic division by shows that the kernel of , , is : a remainder of degree less than vanishing at is zero by minimality over . Monogeneity gives surjectivity, hence .
The maximal ideals of this quotient are exactly those generated by the ; their inverse images in are . They are independent of the chosen lifts. Their residue fields are , of degree , and their contractions are . Thus they are exactly the primes above .
The local factorisation theorem Integral ideal factorisation in a number field, in ZF writes . In the DVR used in that theorem's proof, the maximal ideal of has nilpotency index exactly . On the polynomial side of step 1.1, localisation at gives , whose maximal ideal has nilpotency index exactly : its -th power vanishes and its -st power does not. Thus , proving the ideal factorisation and the stated ramification and residue degrees.
Depends on
Used by
- An Eisenstein prime is totally ramified Corollary
- Dedekind--Kummer without the index hypothesis Counterexample
- Dedekind--Kummer in a cubic field Example
Dependency tree · two levels
10 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
- J. S. Milne, Algebraic Number Theory, Theorem 3.41 (standard reference, not scraped)