Kummer classes of inverse-cyclotomic extensions #
This file extracts a Kummer presentation of an inverse-cyclotomic extension
and proves its finite-place consequence. When the extension is everywhere
unramified, every valuation of the Kummer radicand is divisible by p.
Consequently the radicand gives a nontrivial element of the empty-support
p-Selmer group of the cyclotomic field.
The resulting Selmer class is not identified here with an inverse-character class-group quotient. That passage is the global reciprocity/reflection step, and keeping it separate avoids silently replacing class field theory by a different eigenspace assertion.
The exponent of a principal fractional ideal is the negative logarithm of the corresponding normalized finite-place valuation. This reconciles the factorization and valuation APIs used by the Kummer local condition.
The relative degree of an inverse extension is the prime p.
The prime cyclotomic field contains a primitive p-th root of unity.
A simple Kummer presentation L = K(α) with α ^ p = a.
- radical : L
A Kummer generator of the extension.
- radicand : PrimeCyclotomicField p
The base-field radicand.
The defining Kummer equation.
The radical generates the whole extension.
Instances For
Every inverse extension has a Kummer presentation over the cyclotomic base.
Equations
- E.kummerPresentation = { radical := Classical.choose ⋯, radicand := Classical.choose ⋯, pow_radical := ⋯, adjoin_radical := ⋯ }
Instances For
The Kummer polynomial attached to a presentation is irreducible.
A Kummer presentation of a nontrivial prime-degree extension has a nonzero radicand.
Regard the selected prime above v as a finite prime of the extension.
Equations
- E.finitePrimeAbove v = { asIdeal := ↑(E.primeAbove v), isPrime := ⋯, ne_bot := ⋯ }
Instances For
The canonical map between finite completions at primes lying over one another. Mathlib supplies uniform continuity of the global field embedding; the universal property of completion then supplies this map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The finite-completion map extends the original global field embedding.
The algebra structure on completions induced by a prime lying over a
base prime. Its algebra map is definitionally finiteCompletionMap. The
instance is scoped because the self-extension case creates a non-definitional
instance diamond.
Equations
Instances For
The canonical map between finite completions is continuous.
Ramification index one identifies every pair of corresponding prime powers under contraction.
When both local invariants are one, the map on every prime-power quotient of rings of integers is onto.
Every target integer can be approximated modulo an arbitrary prime power by an integer from the base field.
Prime-power congruence bounds the norm of the corresponding global integer by the expected geometric term.
Under trivial ramification and residue degree, every global target integer belongs to the closure of the finite-completion map.
Under trivial local invariants, the embedded global target field lies in the closure of the finite-completion map.
Trivial ramification and inertia invariants make the canonical map of finite completions have dense range.
On embedded base-field elements, the finite-completion map preserves the normalized norm when both local invariants are one.
Trivial ramification and residue degree make the canonical map between finite completions an isometry.
The canonical map of finite completions is onto whenever its ramification index and inertia degree are both one.
A degree-one map of finite completions is onto. This isolates the linear-algebraic end of the local splitting argument: the remaining arithmetic step is to identify this degree with the global ramification index times inertia degree.
Surjectivity of the canonical local completion map makes the Kummer
radicand a p-th power in the base completion.
Local degree one is already enough to make the Kummer radicand a
p-th power in the base completion.
Complete splitting forces both ideal-theoretic local invariants to be one. These are the inputs to the checked finite-completion surjectivity theorem above.
Complete splitting at the cyclotomic prime turns the canonical Kummer
radicand into a p-th power in the cyclotomic-prime completion.
At every unramified finite prime, the valuation of a Kummer radicand is
a p-th power in the multiplicative value group.
Additively, every finite-prime exponent of an unramified Kummer
radicand is a multiple of p.
Divisibility form of valuationLog_radicand_eq_prime_mul.
Equivalently, the Kummer radicand satisfies the empty-support Selmer local condition at every finite prime.
An everywhere-unramified Kummer radicand defines an element of the
empty-support p-Selmer group of the cyclotomic field.
The radicand class is nontrivial modulo p-th powers; otherwise its
Kummer polynomial could not be irreducible.
The everywhere-unramified Kummer radicand as an actual element of the
empty-support p-Selmer group.
Instances For
The Selmer class supplied by a Kummer presentation is nontrivial.
The canonical nontrivial empty-support Selmer class attached to an everywhere-unramified inverse extension.
Equations
- E.unramifiedRadicandSelmerClass hunramified = E.radicandSelmerClass E.kummerPresentation hunramified
Instances For
The canonical empty-support Selmer class attached to an inverse extension is nontrivial.
Every exponent of the canonical Kummer radicand's principal ideal is
divisible by p when the extension is everywhere unramified.
Divide the canonical radicand divisor by p, prime by prime.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical divisor root is nonzero.
The canonical divisor root has p-th power equal to the radicand's
principal fractional ideal.
The nonzero canonical divisor root, packaged as a unit fractional ideal so that it maps to the class group.
Equations
Instances For
The unit fractional ideal still satisfies the defining p-th power
identity.
The canonical ideal root defines a p-torsion class.
If the canonical root ideal has trivial class, the Kummer radicand is a
global unit times a p-th power.
The exact elementary output of the unramified Kummer construction:
either its canonical p-torsion ideal class is nontrivial, or the radicand
comes from a global unit modulo p-th powers.
Semilinearly transport a Kummer presentation by a chosen lift of a cyclotomic automorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Kummer pairing attached to a presentation, with values in the
p-th roots of unity of the cyclotomic base.
Equations
Instances For
Evaluation formula for the presentation's Kummer pairing.
The Kummer pairing is covariant under semilinear transport: conjugating the relative automorphism and transporting the radical applies the cyclotomic automorphism to the root-of-unity value.
The ordinary cyclotomic character is the inverse of inverseCharacter:
it gives the power by which a cyclotomic automorphism acts on every
p-th root of unity.
Actual conjugation is the power map prescribed by the inverse cyclotomic character.
The canonical primitive root used to coordinatize the Kummer character.
Equations
Instances For
The canonical cyclotomic root is primitive.
The chosen Kummer radical is nonzero.
The relative automorphism whose Kummer eigenvalue is the canonical cyclotomic root of unity.
Equations
Instances For
The Kummer generator acts on the radical by the canonical cyclotomic root.
Every power of the Kummer generator acts through the matching power of the canonical cyclotomic root.
The direct mod-p cyclotomic character, inverse to the character used
in the packaged conjugation law.
Equations
Instances For
A cyclotomic automorphism acts on the canonical primitive root through the direct character.
The Kummer generator is nontrivial.
The Kummer generator generates the relative prime-order Galois group.
It is enough to check invariance under the Kummer generator.
Conjugating the direct-character power of the Kummer generator gives back the generator. This is the inverse-action law in generator coordinates.
The lifted radical is an eigenvector for the Kummer generator with eigenvalue given by the square of the direct cyclotomic character.
Dividing the lifted radical by the direct-character-square power of the original radical gives an element fixed by the Kummer generator.
The lift of a Kummer radical is a base scalar times its direct-character-square power.
The Kummer radicand transforms by the square of the direct cyclotomic
character, up to a p-th power in the base field.
Quotient-group form of the Kummer-line character theorem: the radicand class transforms through the square of the direct cyclotomic character.
Exact character-valued version: the exponent is the canonical natural representative of the square of the direct cyclotomic character.
Canonical-presentation consumer of the square-character theorem.