Reduction of the cyclotomic Kummer product to a faithful Jacobi leaf

For an orbit-coprime integral normalization eta, every prime in the denominator has direct-character-square residue weight. A nonfaithful cyclotomic orbit therefore has trivial residue symbol. On a faithful orbit, the checked factorization of the conjugate diagonal Jacobi sum identifies its principal ideal with the corrected Stickelberger-two prime ideal. The Stickelberger scalar calculation then reduces triviality at the base prime to one explicit value of the residue-symbol homomorphism.

The last value is retained below as a pointwise theorem hypothesis. Thus this file is a reduction of the integral Kummer product, not a reciprocity theorem.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.integralPrincipalProduct_eq_one_of_faithfulJacobi {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (hp5 : 5 ≤ p) (E : InverseExtension p L) (P : E.KummerPresentation) (eta a : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (ha : a ≠ 0) (c : (PrimeCyclotomicField p)ˣ) (hnormalization : (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) eta = P.radicand * ↑c ^ p) (hcoprimeEtaA : IsCoprime (Ideal.span {eta}) (Ideal.span {a})) (hcoprimeAPrime : IsCoprime (Ideal.span {a}) (cyclotomicPrime p).asIdeal) (horbit : ∀ (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)), v.asIdeal ∣ Ideal.span {a} → eta ∉ ((mapFinitePrime sigma) v).asIdeal) (hfaithfulJacobi : ∀ (v : FinitePrime (PrimeCyclotomicField p)), v.asIdeal ∣ Ideal.span {a} → ∀ (hpv : ↑p ∉ v.asIdeal), (Function.Injective fun (b : (ZMod p)ˣ) => (mapFinitePrime (galoisOfDirectCharacter b)) v) → (fractionalPthPowerResidueSymbol eta) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) ((cyclotomicIntegerComplexConj p ⋯) (cyclotomicJacobiSumTwo v hpv))) ⋯)) = 1) : (fractionalKummerSymbol E P) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) a) ⋯)) = 1

For fixed orbit-coprime normalized data, the integral Kummer product is trivial if the residue symbol of eta is trivial on the principal conjugate diagonal Jacobi sum at every faithful denominator prime away from p.

The final argument is deliberately a pointwise hypothesis. It is the sole reciprocity input left by this reduction.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.exists_orbitCoprime_normalization_reducing_to_faithfulJacobi {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (hp5 : 5 ≤ p) (E : InverseExtension p L) (hdiv : ∀ (v : FinitePrime (PrimeCyclotomicField p)), ↑p ∣ FractionalIdeal.count (PrimeCyclotomicField p) v (FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) E.kummerPresentation.radicand)) (a : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (ha : a ≠ 0) (haPrime : a ∉ (cyclotomicPrime p).asIdeal) : ∃ (c : (PrimeCyclotomicField p)ˣ) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (B : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))), eta ≠ 0 ∧ (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) eta = E.kummerPresentation.radicand * ↑c ^ p ∧ Ideal.span {eta} = B ^ p ∧ IsCoprime (Ideal.span {eta}) (galoisOrbitIdealProduct (Ideal.span {a})) ∧ IsCoprime (Ideal.span {eta}) (cyclotomicPrime p).asIdeal ∧ (∀ (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)), v.asIdeal ∣ Ideal.span {a} → eta ∉ ((mapFinitePrime sigma) v).asIdeal) ∧ ((∀ (v : FinitePrime (PrimeCyclotomicField p)), v.asIdeal ∣ Ideal.span {a} → ∀ (hpv : ↑p ∉ v.asIdeal), (Function.Injective fun (b : (ZMod p)ˣ) => (mapFinitePrime (galoisOfDirectCharacter b)) v) → (fractionalPthPowerResidueSymbol eta) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) ((cyclotomicIntegerComplexConj p ⋯) (cyclotomicJacobiSumTwo v hpv))) ⋯)) = 1) → (fractionalKummerSymbol E E.kummerPresentation) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) a) ⋯)) = 1)

Every nonzero denominator away from the cyclotomic prime admits an orbit-coprime pseudo-unit normalization for which the integral Kummer product is reduced to the faithful-prime Jacobi-symbol values displayed explicitly in the implication below.