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 Inertia and Frobenius — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Absolute Values Completions and P Adic Numbers
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Analyticity of Holomorphic Functions; Liouville and Morera
- Arc Length and Rectifiable Curves
- Artinian Rings and Length
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Variation and the Riemann–Stieltjes Integral
- Chain Conditions, Semisimple Modules and the Wedderburn–Artin Theorem
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Differentiability and the Cauchy–Riemann Equations
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Contour Integration
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Decomposition Inertia and Frobenius
- Dedekind Domains and Ideal Classes
- Determinants of Matrices over a Commutative Ring
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Fields and Cyclotomic Extensions
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fundamental Trigonometric Identities
- Goursat's Theorem and Cauchy's Theorem in a Convex Domain
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Integral Extensions and Going Up
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Line Integrals and the Gradient Theorem
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Modules over a Principal Ideal Domain and the Canonical Forms
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Noetherian Rings and Hilbert Basis
- Normal Subgroups and Quotient Groups
- Number Fields Rings of Integers and Discriminants
- Order, Zorn's Lemma, and the Axiom of Choice
- Partitions of Unity and Paracompactness
- pi: the Equivalent Characterizations
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Prime Ideal Decomposition Ramification and the Different
- Prime Spectra and Radicals
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Solvability by Radicals and Kummer Theory
- Splitting Fields
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Symmetric Polynomials and the Fundamental Theorem of Symmetric Functions
- Tensor Products of Modules
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Field of Fractions and Localisation
- The Fundamental Theorem of Finite Abelian Groups
- The Fundamental Theorems of Calculus
- The Galois Correspondence
- The Logarithm and General Powers
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Valuation Rings and Discrete Valuation Rings
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
Quadratic fields display all three possibilities. Gaussian and Eisenstein integers make the exceptional ramified primes explicit; the fifth-root field and its real quadratic subfield give a concrete tower. The splitting field of shows why a nonabelian base prime determines a conjugacy class.
Two counterexamples isolate the hypotheses: ramified residue data admits multiple Frobenius lifts, and the bad generator at 2 has repeated reduction even though the field is unramified and inert. The integral generator recovers the correct cycle data.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Decomposition inertia in a quadratic field
Example
In a quadratic Galois extension of number fields, let . For any nonzero base prime the three possibilities are: split: , , Frobenius identity; inert: , , , Frobenius the nonidentity element; ramified: , , arithmetic Frobenius coset identity in D/I.
Facts & Assumptions
Given: The data and hypotheses of the statement.
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 .
Orders of decomposition and inertia groups: For finite Galois L/K and nonzero , writing e and f for its ramification index and residue degree, The prime P is unramified over p if and only if its inertia group is trivial.
Frobenius order is residue degree: For finite Galois L/K and nonzero , the arithmetic Frobenius coset has order in D/I. If P is unramified, has the same order in D.
Verification
Positive integers e,f,g with efg=2 have exactly the three displayed triples: the single factor 2 occurs in exactly one coordinate. These correspond respectively to split, inert, and ramified ideal factorizations.
The formulas and determine the subgroups, since has only its identity subgroup and itself. For e=1 the Frobenius order is f, giving identity in the split case and the unique element of order two in the inert case. In the ramified case D/I has order f=1, so the residue coset is identity; there is no assertion of a unique lift.
Gaussian and eisenstein frobenius
Example
In , an odd prime p splits if and is inert if ; arithmetic Frobenius sends . The prime 2 ramifies. In , a prime splits if and is inert if ; arithmetic Frobenius sends . The prime 3 ramifies.
Facts & Assumptions
Given: The data and hypotheses of the statement.
Frobenius cycle type and prime splitting: Let be monic separable with splitting field L, and let p be a rational prime not dividing . Then p is unramified in L and is squarefree. The degrees of its monic irreducible factors, with each distinct factor counted once, are exactly the cycle lengths of arithmetic Frobenius on the roots of F.
Decomposition inertia in a quadratic field: In a quadratic Galois extension of number fields, let . For any nonzero base prime the three possibilities are: split: , , Frobenius identity; inert: , , , Frobenius the nonidentity element; ramified: , , arithmetic Frobenius coset identity in D/I.
The multiplicative group of a finite field is cyclic: The multiplicative group of every finite field is cyclic.
Integers in a quadratic field: For squarefree , if , and otherwise.
Verification
The quadratic integral-basis theorem gives and , since . The polynomials are and , with discriminants -4 and -3. At the stated nonexceptional primes they have good reduction.
For odd p, roots of are elements of order four in . Cyclicity says they exist exactly when . For , roots of are elements of order three, since and T=1 is not a root unless p=3. Cyclicity gives roots exactly when . A quadratic without a root is irreducible. Thus the cycle types are two fixed points or a transposition, giving split or inert cases in the quadratic table.
In good reduction the two roots are distinct. The Frobenius congruence sends each chosen root to its p-th power modulo P; that power is itself a root, so injectivity on the two root reductions forces equality in the number field. This gives both claimed formulas.
In the Gaussian ring, and by substituting i=-1. Thus (1+i) is prime and as ideals. In the Eisenstein ring, and the quotient by is by substituting . Hence as ideals. Both exceptional primes ramify.
Frobenius in a small cyclotomic field
Example
Let be a primitive fifth root of unity and . Then by . For every prime , p is unramified and its arithmetic Frobenius is . In particular 2 is inert, with .
Facts & Assumptions
Given: The data and hypotheses of the statement.
Frobenius cycle type and prime splitting: Let be monic separable with splitting field L, and let p be a rational prime not dividing . Then p is unramified in L and is squarefree. The degrees of its monic irreducible factors, with each distinct factor counted once, are exactly the cycle lengths of arithmetic Frobenius on the roots of F.
Frobenius order is residue degree: For finite Galois L/K and nonzero , the arithmetic Frobenius coset has order in D/I. If P is unramified, has the same order in D.
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 .
Eisenstein criterion over the integers: Let be primitive with . If there is a prime such that then is irreducible in .
The discriminant of a monic polynomial as the coefficient expression of : By prop-vandermonde-square-is-symmetric and thm-fundamental-theorem-of-symmetric-polynomials, there is a unique polynomial such that For a monic polynomial over a commutative ring, its discriminant is Equivalently, in any algebra in which splits with roots , this coefficient expression evaluates to . The definition therefore depends only on the coefficients and not on a choice or ordering of roots. For a monic constant polynomial, .
Verification
The polynomial satisfies , Eisenstein at 5. Translation preserves reducibility, so Phi is irreducible. Its four roots for a=1,2,3,4 already lie in L. They give four automorphisms, with composition multiplying exponents modulo 5. The element 2 has successive powers 2,4,3,1, hence generates this group.
At a root r of Phi, differentiating gives . The product over its four roots is : the root product is 1, and . Pairing opposite root differences shows . Hence its discriminant is .
For the good-reduction theorem gives unramifiedness and distinct root reductions. Frobenius sends the residue of zeta to its p-th power; since is another root, distinctness forces . At p=2 that automorphism has order four, so f=4; e=1 and efg=4 then give g=1, namely inertness.
Nonabelian frobenius conjugacy class
Example
The splitting field of over has Galois group . At p=5 its Frobenius conjugacy class consists of all three transpositions: distinct choices of prime can give distinct elements.
Facts & Assumptions
Given: The data and hypotheses of the statement.
Frobenius cycle type and prime splitting: Let be monic separable with splitting field L, and let p be a rational prime not dividing . Then p is unramified in L and is squarefree. The degrees of its monic irreducible factors, with each distinct factor counted once, are exactly the cycle lengths of arithmetic Frobenius on the roots of F.
Frobenius elements above a prime are conjugate: In a finite Galois extension L/K let the nonzero prime p be unramified. If above p, then Thus p determines one conjugacy class. If the Galois group is abelian, the element is independent of P.
Eisenstein criterion over the integers: Let be primitive with . If there is a prime such that then is irreducible in .
Verification
Eisenstein at 2 proves irreducible. Let a be its positive real root. The real cubic field does not contain the nonreal cube root of unity . Its quadratic polynomial remains irreducible over that real field, so has degree six and contains all roots. The faithful permutation action on its three roots embeds its order-six Galois group into , hence is an isomorphism.
For roots r of , the derivative is . Their product is 2, so . Pairing differences contributes , giving discriminant -108. Thus 5 is a good prime. Modulo 5, direct multiplication gives ; the quadratic discriminant is modulo 5, which is not among the squares 0,1,4. Its degrees are therefore 1 and 2.
The Frobenius cycle theorem gives cycle type (1,2), a transposition. The Frobenius elements above 5 constitute its entire conjugacy class. Conjugating a transposition in yields each of the three transpositions and no other permutation. Thus the class contains three distinct elements.
Decomposition groups in a tower
Example
Let , , and . At p=2 there is a unique prime in each field above p. All ramification indices are one, and the residue degrees are four in M/K and two in each step. The decomposition sequence is and all inertia groups are trivial. The relative Frobenius for M/L is the square of the Frobenius for M/K.
Facts & Assumptions
Given: The data and hypotheses of the statement.
Frobenius in a small cyclotomic field: Let be a primitive fifth root of unity and . Then by . For every prime , p is unramified and its arithmetic Frobenius is . In particular 2 is inert, with .
Decomposition and inertia in towers: Let M/L/K be a tower of number fields with M/K and L/K finite Galois, and fix nonzero primes . With , Restriction gives exact sequences The intersection identities also hold without L/K Galois; the displayed quotient assertions use that hypothesis.
Frobenius compatibility in finite towers: Let M/L/K have M/K and L/K finite Galois, and let be nonzero primes with Q unramified over p. Then If with both finite Galois and Q unramified over p, the Frobenius elements at its two contractions determine uniquely by restriction.
Verification
Put . Expanding and using gives . This polynomial has discriminant 5, not a rational square, so has degree two. Exponent 2 sends t to , while exponent 4 fixes t. Thus restriction has kernel the order-two subgroup generated by exponent 4.
At 2, M/K is unramified and inert with degree four, so there is one prime Q, D(Q/p)=C4 and I(Q/p)=1. Every prime of L above p has a prime of M above it by integral prime factorization, so it is the contraction P of Q. The tower exact sequences now give D(Q/P)=C2 and D(P/p)=C2 with all inertia groups trivial. In the unramified residue isomorphisms these group orders are the residue degrees, giving two in each step.
Compatibility says that the absolute exponent-2 Frobenius restricts to the nonidentity automorphism of L, and the relative Frobenius is its power, namely exponent 4. This realizes the displayed exact sequence.
Ramified frobenius has no canonical lift
Statement refuted
The residue Frobenius congruence does not determine a unique element of D at a ramified prime. At 2 in , with , one has and . Identity and complex conjugation are distinct lifts of the same arithmetic Frobenius coset in D/I.
Facts & Assumptions
Given: The data and hypotheses of the statement.
Gaussian and eisenstein frobenius: In , an odd prime p splits if and is inert if ; arithmetic Frobenius sends . The prime 2 ramifies. In , a prime splits if and is inert if ; arithmetic Frobenius sends . The prime 3 ramifies.
Arithmetic frobenius coset: For finite Galois L/K and nonzero , the arithmetic Frobenius coset is the unique element of corresponding under the residue isomorphism to on , where . It is defined also when P is ramified. Its inverse is called geometric Frobenius. The quotient element is distinguished; a representative in D need not be unique.
Counterexample
The Gaussian calculation gives and residue field F2. There is only one prime above 2, so both automorphisms stabilize it. Modulo P, i=-1=1, and conjugation also sends i to -i=1. As every integral element is a+bi, both automorphisms act identically on every residue.
Thus D=I=C2 and D/I is trivial. The arithmetic map on F2 is x squared, which is identity on its two elements 0 and 1. Both identity and conjugation satisfy its congruence, but they differ on i in the number field. This refutes uniqueness from residue data; it does not preclude an additional external convention from selecting a representative.
Frobenius cycle type needs good reduction
Statement refuted
Factor multiplicities from an arbitrary integral generator need not encode Frobenius cycles. For at p=2, , yet is unramified and inert at 2, with Frobenius a transposition. The integral generator has minimal polynomial , whose reduction is irreducible over .
Facts & Assumptions
Given: The data and hypotheses of the statement.
Frobenius cycle type and prime splitting: Let be monic separable with splitting field L, and let p be a rational prime not dividing . Then p is unramified in L and is squarefree. The degrees of its monic irreducible factors, with each distinct factor counted once, are exactly the cycle lengths of arithmetic Frobenius on the roots of F.
Dedekind--Kummer prime factorisation: 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 def-prime-above-and-residue-degree.
Ramification is detected by the number-field discriminant: A rational prime ramifies in if and only if .
Integers in a quadratic field: For squarefree , if , and otherwise.
Power-basis and polynomial discriminants: Let . If is the degree- monic minimal polynomial of , then
Counterexample
The quadratic integral-basis theorem gives . Direct substitution gives G(omega)=0, and its discriminant 5 is not a rational square, so it is the minimal polynomial. The power-basis discriminant formula gives . Therefore 2 is unramified by the field-discriminant criterion.
Modulo 2, G is , taking value 1 at both 0 and 1. It is irreducible. Dedekind-Kummer applies to the full ring and gives a single prime of e=1 and f=2. Alternatively the good-reduction cycle theorem for G gives the transposition Frobenius.
For the other generator, , so has index 2 in , as the change-of-basis matrix has determinant 2. Its polynomial discriminant is 20 and its reduction is . The two characteristic-zero roots reduce to the same root, so this reduction is not a bijection of root sets. It cannot supply the cycle comparison; in particular reading its multiplicity as ramification would contradict e=1. The full-ring hypothesis of the cited Dedekind-Kummer statement fails for this generator.