Kummer coordinates for the finite-prime Artin product

This file rewrites the ideal-theoretic Artin map of an inverse-cyclotomic extension in the Kummer pairing attached to a chosen radical. The resulting principal product formula is proved equivalent, without an arithmetic assumption, to conductor-one principal reciprocity for the original Artin map. The genuinely global assertion is then isolated as a named principle.

def NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.SatisfiesPrincipalProductFormula {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) : Prop

The exact principal product formula in Kummer coordinates: the finite product of local Kummer/Frobenius symbols attached to every principal fractional ideal is one.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.satisfiesPrincipalProductFormula_iff_kills {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) : SatisfiesPrincipalProductFormula E P ↔ UnramifiedArtin.KillsPrincipalIdeals (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p) (fractionalKummerSymbol E P)

The explicit product formula is the statement that the fractional Kummer-symbol homomorphism kills principal ideals.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.killsPrincipalKummerSymbols_iff_reciprocity {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) : UnramifiedArtin.KillsPrincipalIdeals (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p) (fractionalKummerSymbol E P) ↔ E.SatisfiesPrincipalReciprocity

Changing from cyclic coordinates to Kummer coordinates preserves and reflects the property of killing all principal fractional ideals.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.satisfiesPrincipalProductFormula_iff_reciprocity {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) : SatisfiesPrincipalProductFormula E P ↔ E.SatisfiesPrincipalReciprocity

The Kummer principal product formula is an exact reformulation of conductor-one principal reciprocity for the ideal Artin map.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.rationalPrincipalProductFormula {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (hp : 2 < p) (E : InverseExtension p L) (P : E.KummerPresentation) (hunramified : E.IsUnramifiedAtFinitePlaces) (a : ℚˣ) : (((UnramifiedArtin.fractionalIdealDivisor (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Additive.ofMul ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) ((Units.map ↑(algebraMap ℚ (PrimeCyclotomicField p))) a)))).prod fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (n : ℤ) => localKummerFrobeniusSymbol E P v ^ n) = 1

The explicit Kummer product formula holds on principal ideals generated by rational units. Thus the integer-denominator part of cyclotomic reciprocity is already forced by inverse-character equivariance; the missing arithmetic input concerns genuinely cyclotomic generators.

def NumberTheory.CyclotomicCharacter.InverseExtension.SatisfiesPrimeToCyclotomicPrincipalReciprocity {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) : Prop

Principal reciprocity away from the unique cyclotomic prime. The count condition says exactly that the principal fractional ideal has no factor at the prime generated by ζ_p - 1.

Equations

• One or more equations did not get rendered due to their size.

def NumberTheory.CyclotomicCharacter.InverseExtension.SatisfiesIntegralPrimeToCyclotomicPrincipalReciprocity {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) : Prop

Integral principal reciprocity away from the cyclotomic prime. The checked denominator-clearing theorem below shows that this integral condition already controls every prime-to-cyclotomic field unit.

Equations

• One or more equations did not get rendered due to their size.

def NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.SatisfiesIntegralPrimeToCyclotomicProductFormula {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) : Prop

Integral prime-to-cyclotomic principal reciprocity in the canonical Kummer/Frobenius coordinate.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.satisfiesIntegralPrimeToCyclotomicProductFormula_iff {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) : SatisfiesIntegralPrimeToCyclotomicProductFormula E P ↔ E.SatisfiesIntegralPrimeToCyclotomicPrincipalReciprocity

The integral Kummer product formula is exactly integral Artin reciprocity after the already-checked change of cyclic coordinate.

def NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.HasPDivisibleFiniteDivisor {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) : Prop

The pseudo-unit divisor condition on a Kummer radicand: every finite prime exponent of its principal fractional ideal is divisible by p.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.fractionalKummerSymbol_principalRadicand_eq_one {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (hdiv : HasPDivisibleFiniteDivisor E E.kummerPresentation) : (fractionalKummerSymbol E E.kummerPresentation) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 E.kummerPresentation.radicand ⋯)) = 1

The pseudo-unit divisor hypothesis already kills the principal ideal of the radicand itself under the canonical Kummer symbol. One-sided reciprocity is the additional assertion for an arbitrary principal denominator.

def NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.IsPthPowerAtCyclotomicPrime {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) : Prop

The local-primary condition used by one-sided Kummer reciprocity: the radicand is a p-th power in the cyclotomic-prime completion.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.isFinitePrimaryAtCyclotomicPrime_of_normalization_coprime {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) (hlocal : IsPthPowerAtCyclotomicPrime E P) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (c : (PrimeCyclotomicField p)ˣ) (hη : (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η = P.radicand * ↑c ^ p) (hcoprimeηPrime : IsCoprime (Ideal.span {η}) (cyclotomicPrime p).asIdeal) : IsFinitePrimaryAtCyclotomicPrime η

A normalized integral numerator produced from a locally primary Kummer radicand is finite-primary whenever the normalization is coprime to the cyclotomic prime. This is the form in which the local congruence enters the one-sided reciprocity argument.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.satisfiesPrimeToCyclotomicPrincipalReciprocity_of_integral {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (hintegral : E.SatisfiesIntegralPrimeToCyclotomicPrincipalReciprocity) : E.SatisfiesPrimeToCyclotomicPrincipalReciprocity

Mathlib's prime-complement denominator theorem clears a prime-to-cyclotomic fractional generator using integral numerator and denominator that both avoid the cyclotomic prime.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.satisfiesPrincipalReciprocity_of_primeToCyclotomic {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (hp : 2 < p) (E : InverseExtension p L) (hunramified : E.IsUnramifiedAtFinitePlaces) (haway : E.SatisfiesPrimeToCyclotomicPrincipalReciprocity) : E.SatisfiesPrincipalReciprocity

Since the cyclotomic prime itself has trivial Artin symbol, reciprocity for principal ideals prime to that prime already implies reciprocity for all principal fractional ideals.

def NumberTheory.CyclotomicCharacter.PrimeToCyclotomicPrincipalReciprocityPrinciple (p : ℕ) [Fact (Nat.Prime p)] : Prop

The exact prime-to-p reciprocity input left after removing the unique cyclotomic-prime factor from every principal fractional ideal.

Equations

• One or more equations did not get rendered due to their size.

def NumberTheory.CyclotomicCharacter.LocallyPrimaryPseudoUnitKummerReciprocityPrinciple (p : ℕ) [Fact (Nat.Prime p)] : Prop

The exact one-sided Kummer reciprocity kernel after separating all checked local and normalization inputs. It assumes only the pseudo-unit divisor condition and local p-th-power condition for the canonical radicand, and asks for integral principal Kummer-symbol vanishing away from the cyclotomic prime.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberTheory.CyclotomicCharacter.primeToCyclotomicPrincipalReciprocityPrinciple_of_locallyPrimaryPseudoUnit {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (hreciprocity : LocallyPrimaryPseudoUnitKummerReciprocityPrinciple p) : PrimeToCyclotomicPrincipalReciprocityPrinciple p

One-sided Kummer reciprocity for locally-primary pseudo-units supplies prime-to-cyclotomic principal Artin reciprocity. The Kummer/Frobenius comparison, both arithmetic hypotheses, and fractional denominator clearing in this reduction are checked.

def NumberTheory.CyclotomicCharacter.KummerArtinProductFormulaPrinciple (p : ℕ) [Fact (Nat.Prime p)] : Prop

The missing global product formula, stated in the canonical Kummer presentation of every everywhere-finite-unramified inverse extension.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberTheory.CyclotomicCharacter.kummerArtinProductFormulaPrinciple_of_primeToCyclotomic {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (haway : PrimeToCyclotomicPrincipalReciprocityPrinciple p) : KummerArtinProductFormulaPrinciple p

Prime-to-cyclotomic principal reciprocity implies the full Kummer product formula. The omitted cyclotomic-prime factor contributes trivially because its Artin symbol is one.

theorem NumberTheory.CyclotomicCharacter.principalReciprocityPrinciple_of_kummerArtinProductFormula {p : ℕ} [Fact (Nat.Prime p)] (hproduct : KummerArtinProductFormulaPrinciple p) : PrincipalReciprocityPrinciple p

The global Kummer product formula supplies conductor-one principal reciprocity for every relevant inverse extension.

theorem NumberTheory.CyclotomicCharacter.classFieldTheoryPrinciple_of_kummerArtinProductFormula {p : ℕ} [Fact (Nat.Prime p)] (hproduct : KummerArtinProductFormulaPrinciple p) : ClassFieldTheoryPrinciple p

Consequently, the global Kummer product formula gives the class-group quotient required by the cyclotomic obstruction.