Inverse-cyclotomic unramified extensions #
This file isolates the number-theoretic interface used in Mazur's prime-order
argument. It packages a cyclic degree-p extension of the p-th cyclotomic
field together with the inverse-cyclotomic conjugation law, expresses local
unramifiedness at actual finite places, and records the class-group quotient
that global class field theory must produce.
The pinned Mathlib supplies cyclotomic Galois theory, finite places,
ramification indices, ideal class groups, and the analytic class-number
formula. The local criteria and the finite-prime generation step are proved
below. The remaining global input is conductor-one principal Artin
reciprocity, isolated as PrincipalReciprocityPrinciple before the checked
assembly of ClassFieldTheoryPrinciple.
The p-th cyclotomic field over the rationals.
Instances For
A finite place in the ideal-theoretic ramification API: a nonzero prime ideal in the ring of integers.
Equations
Instances For
The unique finite prime of the prime cyclotomic field above p, written
as the ideal generated by ζ_p - 1.
Equations
Instances For
The inverse of the mod-p cyclotomic character on the Galois group of
the p-th cyclotomic field.
Equations
Instances For
For p > 2, the cyclotomic base is totally complex. Thus the intended
prime-order range has no real places requiring a narrow-class-group
correction.
A cyclic degree-p extension of ℚ(ζ_p) on which conjugation by
Gal(ℚ(ζ_p)/ℚ) acts through the inverse cyclotomic character.
The lifts and the conjugates are included as data, but both are tied to the
field operations by lift_algebraMap and conjugate_apply; in particular,
inverse_action is an assertion about actual conjugation in the field tower,
not an unrelated abstract action.
- isGalois : IsGalois (PrimeCyclotomicField p) L
Galoisness over the cyclotomic base.
Galoisness over the rationals, needed to lift cyclotomic automorphisms.
Identification of the relative Galois group with the cyclic group of order
p.- lift : Gal(PrimeCyclotomicField p/ℚ) → Gal(L/ℚ)
A lift to
Lof each automorphism of the cyclotomic base. - lift_algebraMap (σ : Gal(PrimeCyclotomicField p/ℚ)) (x : PrimeCyclotomicField p) : (self.lift σ) ((algebraMap (PrimeCyclotomicField p) L) x) = (algebraMap (PrimeCyclotomicField p) L) (σ x)
Each chosen lift restricts to the original cyclotomic automorphism.
- conjugate : Gal(PrimeCyclotomicField p/ℚ) → Gal(L/PrimeCyclotomicField p) → Gal(L/PrimeCyclotomicField p)
Conjugation of the relative Galois group by a chosen lift.
- conjugate_apply (σ : Gal(PrimeCyclotomicField p/ℚ)) (τ : Gal(L/PrimeCyclotomicField p)) (x : L) : (self.conjugate σ τ) x = (self.lift σ) (τ ((self.lift σ).symm x))
The packaged conjugation is the actual conjugation on field elements.
- inverse_action (σ : Gal(PrimeCyclotomicField p/ℚ)) (τ : Gal(L/PrimeCyclotomicField p)) : Multiplicative.toAdd (self.galEquiv (self.conjugate σ τ)) = ↑((inverseCharacter p) σ) * Multiplicative.toAdd (self.galEquiv τ)
Conjugation acts on the cyclic relative group through the inverse character.
Instances For
The roadmap-facing name for an inverse-cyclotomic extension.
Equations
Instances For
Unramifiedness of an inverse-cyclotomic extension at a finite place of the cyclotomic base field.
Equations
Instances For
Unramifiedness at every finite place of the cyclotomic base field.
Equations
Instances For
For rings of integers in a number-field extension, global algebraic unramifiedness is equivalent to unramifiedness at every nonzero prime of the base. The generic prime contributes no extra hypothesis in characteristic zero.
Mathlib's ramification-index criterion, specialized to an actual finite place of the cyclotomic field.
The simultaneous ramification-index-one condition at all finite places.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Everywhere finite-place unramifiedness is equivalent to ramification index one above every finite place.
The full number-ring extension is unramified exactly when every ramification index above every finite cyclotomic prime is one.
A chosen prime of L above the finite prime v of the cyclotomic base.
Equations
Instances For
The arithmetic Frobenius of an inverse-cyclotomic extension at a finite prime of the cyclotomic base.
Equations
Instances For
The selected Frobenius satisfies the defining residue-field congruence at
the selected prime above v.
Since the relative Galois group is cyclic, the selected Frobenius is
independent of the prime of L chosen above v.
At an unramified finite prime, the Frobenius congruence characterizes the Frobenius element at every prime above it.
The automorphism induced by a cyclotomic Galois element on the ring of integers of the cyclotomic field.
Equations
Instances For
The automorphism induced by the chosen lift on the ring of integers of the extension field.
Equations
Instances For
The two induced automorphisms of the rings of integers form a semilinear square over the chosen lift.
Extending the ring-of-integers action to the fraction field recovers the original cyclotomic Galois automorphism.
The action of a cyclotomic Galois element on finite primes.
Equations
Instances For
The ideal underlying the transported finite prime is the usual ideal map.
Every cyclotomic automorphism fixes the unique finite prime above p.
Actual conjugation by a chosen lift agrees with semilinear conjugation on the rings of integers.
Arithmetic Frobenius congruences are preserved by semilinear conjugation.
A canonical prime over the transported base prime, obtained by mapping the selected prime upstairs by the chosen lift.
Equations
- E.mappedPrimeAbove σ v = ⟨Ideal.map (E.liftIntegerEquiv σ) ↑(E.primeAbove v), ⋯⟩
Instances For
At unramified finite primes, Frobenius transforms by actual conjugation under the cyclotomic Galois action.
The local Artin symbol, expressed in the fixed cyclic coordinate
Multiplicative (ZMod p).
Equations
- E.artinSymbol v = E.galEquiv (E.frobeniusAt v)
Instances For
Multiplication by the inverse-cyclotomic character, viewed as an endomorphism of the additive cyclic coordinate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluation of the inverse-character action in the additive cyclic coordinate.
The finite-prime Artin symbol transforms by the inverse cyclotomic character.
The semilinear action of a cyclotomic Galois element on nonzero fractional ideals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The fractional-ideal action sends a prime ideal to the transported finite prime.
The ideal-theoretic Artin homomorphism obtained by extending the finite prime symbols multiplicatively to all nonzero fractional ideals.
Instances For
On a prime fractional ideal, fractionalArtin is the selected local
arithmetic Frobenius in the cyclic coordinate.
The fractional Artin map is inverse-cyclotomic equivariant.
Equivariance kills the Artin symbol of a finite prime fixed by a cyclotomic automorphism whose inverse character is nontrivial.
Equivariance kills any fractional ideal fixed by a cyclotomic automorphism whose inverse character is nontrivial.
Consequently, the fractional Artin map kills a principal ideal whose generator is fixed by such a cyclotomic automorphism. This is a checked fragment of principal reciprocity; an arbitrary generator need not have a nontrivial stabilizer.
Conductor-one principal reciprocity for the ideal Artin map: every principal fractional ideal maps trivially.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weak Chebotarev input needed here, stated exactly as generation of the cyclic relative Galois group by finite-prime Artin symbols.
Equations
Instances For
If the selected Frobenius is trivial at an unramified finite prime, that prime splits completely: the number of primes above it equals the relative degree.
The finite-prime Artin symbol at the unique prime above p is trivial in
an everywhere-unramified inverse-cyclotomic extension.
The unique prime above p splits completely in an everywhere-unramified
inverse-cyclotomic extension. This is stronger than merely saying that the
prime is unramified: the inverse-character action forces its decomposition
Frobenius to be trivial.
The weak global arithmetic input needed in the prime-degree case: at least one finite prime does not split completely.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every inverse extension has a nonsplit finite prime. The proof is the
Dedekind-zeta pole argument in NumberTheory.WeakChebotarev; the unramifiedness
hypothesis is retained here because this is the exact interface used by the
Artin-symbol construction.
For a relative Galois group of prime order, one nonsplit unramified finite prime already makes the Frobenius symbols generate the whole group.
Once principal reciprocity is known, the ideal Artin map descends to the ordinary ideal class group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The class-group Artin map agrees with the fractional-ideal Artin map on a represented ideal class.
The descended class-group Artin map is onto exactly when the finite-prime Frobenius symbols generate the cyclic target.
Frobenius generation makes the descended class-group Artin map surjective.
The strongest unconditional finite-place bridge currently supported by the pinned library: local ramification indices equal to one imply unramifiedness at every finite place.
The action of a cyclotomic Galois automorphism on the class group of the ring of integers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Formula for the cyclotomic action on an ideal-class representative.
The descended class-group Artin map is inverse-cyclotomic equivariant.
The quotient supplied by the unramified abelian correspondence, before recording its Galois eigenspace.
- quotient : ClassGroup (NumberField.RingOfIntegers (PrimeCyclotomicField p)) →* Multiplicative (ZMod p)
The cyclic order-
pquotient map from the ideal class group. - surjective : Function.Surjective ⇑self.quotient
The quotient map is onto.
Instances For
Divisibility of the cyclotomic class number by p produces an abstract
cyclic order-p quotient. No Galois character is asserted: selecting the
inverse-cyclotomic quotient is the additional reciprocity content below.
Equations
- NumberTheory.CyclotomicCharacter.UnramifiedClassGroupQuotient.ofPrimeDvdCard h = { quotient := ⋯.choose, surjective := ⋯ }
Instances For
An abstract cyclic order-p quotient of the class group exists exactly
when p divides the class number. This deliberately omits the
inverse-cyclotomic equivariance required by InverseClassGroupQuotient.
The assertion that a class-group quotient transforms through the inverse cyclotomic character.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A nonzero inverse-cyclotomic quotient of the ideal class group. Its existence is the precise class-group obstruction forced by a cyclic everywhere-unramified inverse-cyclotomic extension.
- surjective : Function.Surjective ⇑self.quotient
- inverseCyclotomic : self.IsInverseCyclotomic
The quotient transforms through the inverse cyclotomic character.
Instances For
Principal reciprocity and finite-prime Frobenius generation construct the required surjective inverse-cyclotomic quotient of the ordinary ideal class group.
Equations
- E.inverseClassGroupQuotient hunramified hprincipal hgenerate = { quotient := E.classGroupArtin hprincipal, surjective := ⋯, inverseCyclotomic := ⋯ }
Instances For
The missing class-field-theory statement: over a totally complex base, every everywhere-unramified inverse-cyclotomic extension produces the corresponding ordinary ideal-class-group quotient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exact conductor-one reciprocity input: over the totally complex cyclotomic base, the finite-prime Artin product kills every principal fractional ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exact weak-Chebotarev input in prime degree: an everywhere finite-place-unramified inverse extension has at least one finite prime that does not split completely.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weak nonsplitting input is a theorem: the zeta function of a nontrivial number-field extension cannot dominate the square of the base zeta function near its simple pole.
Principal reciprocity implies the required unramified inverse-character class-group quotient. Finite-prime nonsplitting, ideal-theoretic descent, surjectivity, and Galois equivariance in this assembly are all checked.
If global reciprocity produces the class-group quotient and the relevant inverse-cyclotomic quotient is known not to exist, then no such extension can be everywhere unramified.