The corrected Stickelberger-two residue product

This file is the algebraic consumer of the corrected b = 2 coefficients. For one finite prime v of ℚ(ζ_p), it forms the nonzero fractional ideal

∏ a, σₐ⁻¹(v) ^ stickelbergerTwoCoefficient p a.

The Kummer class of the intended numerator has direct-character weight two. Combining that weight with Galois covariance of the residue symbol predicts

(η / σ(v)) = (η / v) ^ directCharacter(σ)⁻¹.

Field-valued witnesses for the equality of Kummer classes can carry denominators. Accordingly, HasDirectCharacterSquareResidueWeightAt records exactly this symbol-level consequence, without asserting a reciprocity law or a Jacobi-sum factorization. A later Jacobi module is the named downstream producer of this interface; jacobiStickelbergerTwoResidueConsumer is its checked consumer.

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.directCharacterEquiv (p : ℕ) [Fact (Nat.Prime p)] : Gal(PrimeCyclotomicField p/ℚ) ≃* (ZMod p)ˣ

The direct cyclotomic character, packaged as the standard equivalence. This is used only to choose the automorphism with prescribed character.

Equations

• NumberTheory.CyclotomicCharacter.InverseExtension.directCharacterEquiv p = IsCyclotomicExtension.autEquivPow (NumberTheory.CyclotomicCharacter.PrimeCyclotomicField p) ⋯

@[simp]

theorem NumberTheory.CyclotomicCharacter.InverseExtension.directCharacterEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] (sigma : Gal(PrimeCyclotomicField p/ℚ)) : (directCharacterEquiv p) sigma = (directCharacter p) sigma

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.galoisOfDirectCharacter {p : ℕ} [Fact (Nat.Prime p)] (a : (ZMod p)ˣ) : Gal(PrimeCyclotomicField p/ℚ)

The automorphism whose direct cyclotomic character is a.

Equations

• NumberTheory.CyclotomicCharacter.InverseExtension.galoisOfDirectCharacter a = (NumberTheory.CyclotomicCharacter.InverseExtension.directCharacterEquiv p).symm a

@[simp]

theorem NumberTheory.CyclotomicCharacter.InverseExtension.directCharacter_galoisOfDirectCharacter {p : ℕ} [Fact (Nat.Prime p)] (a : (ZMod p)ˣ) : (directCharacter p) (galoisOfDirectCharacter a) = a

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.stickelbergerTwoPrimeIdeal {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ

The corrected b = 2 product of the Galois conjugates of one finite prime. The inverse in galoisOfDirectCharacter a⁻¹ matches the coefficient of σₐ⁻¹ in the corrected Stickelberger element.

Equations

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

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.stickelbergerTwoResidueProduct {p : ℕ} [Fact (Nat.Prime p)] (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (v : FinitePrime (PrimeCyclotomicField p)) : ↥(rootsOfUnity p (PrimeCyclotomicField p))

The corresponding product of total prime residue symbols.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_stickelbergerTwoPrimeIdeal {p : ℕ} [Fact (Nat.Prime p)] (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (v : FinitePrime (PrimeCyclotomicField p)) : (fractionalPthPowerResidueSymbol eta) (stickelbergerTwoPrimeIdeal v) = stickelbergerTwoResidueProduct eta v

Evaluation of the fractional residue symbol on the corrected ideal is definitionally the corrected product of total prime symbols.

def NumberTheory.CyclotomicCharacter.InverseExtension.HasDirectCharacterSquareResidueWeightAt {p : ℕ} [Fact (Nat.Prime p)] (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (v : FinitePrime (PrimeCyclotomicField p)) : Prop

The exact symbol-level consequence of direct-character-square Kummer covariance at v.

For an integral Kummer representative, this is what simultaneous Galois covariance and an equality σ(η) = η ^ directCharacter(σ)^2 * b^p give after all denominators have been cleared away from the relevant primes. Keeping that arithmetic clearance explicit prevents this algebraic module from assuming either reciprocity or a Jacobi factorization.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.HasDirectCharacterSquareResidueWeightAt.of_integral_pthPower_witnesses {p : ℕ} [Fact (Nat.Prime p)] (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (v : FinitePrime (PrimeCyclotomicField p)) (heta : eta ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) (hwitness : ∀ (sigma : Gal(PrimeCyclotomicField p/ℚ)), ∃ (b : NumberField.RingOfIntegers (PrimeCyclotomicField p)), (baseIntegerEquiv sigma) eta = eta ^ (↑((directCharacter p) sigma ^ 2)).val * b ^ p) : HasDirectCharacterSquareResidueWeightAt eta v

Integral-witness producer for the symbol-level square-weight interface.

The only support hypotheses are that the base prime avoids eta and p. For every cyclotomic automorphism, the witness b is integral and satisfies

σ(eta) = eta ^ directCharacter(σ)^2 * b^p.

The equality itself forces both eta and b to avoid σ(v), so no redundant orbitwise nonmembership hypotheses are required.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.HasDirectCharacterSquareResidueWeightAt.at_inverse {p : ℕ} [Fact (Nat.Prime p)] {eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)} {v : FinitePrime (PrimeCyclotomicField p)} (hweight : HasDirectCharacterSquareResidueWeightAt eta v) (a : (ZMod p)ˣ) : totalPthPowerResidueSymbolAtPrime eta ((mapFinitePrime (galoisOfDirectCharacter a⁻¹)) v) = totalPthPowerResidueSymbolAtPrime eta v ^ (↑a).val

The weight-two interface at the inverse-character representative indexed by a has exponent a.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.stickelbergerTwoResidueProduct_eq_weightedScalar {p : ℕ} [Fact (Nat.Prime p)] {eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)} {v : FinitePrime (PrimeCyclotomicField p)} (hweight : HasDirectCharacterSquareResidueWeightAt eta v) : stickelbergerTwoResidueProduct eta v = totalPthPowerResidueSymbolAtPrime eta v ^ (stickelbergerTwoWeightedScalar p).val

The corrected residue product acts through the elementary Stickelberger-two weighted scalar.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_stickelbergerTwoPrimeIdeal_eq_weightedScalar {p : ℕ} [Fact (Nat.Prime p)] {eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)} {v : FinitePrime (PrimeCyclotomicField p)} (hweight : HasDirectCharacterSquareResidueWeightAt eta v) : (fractionalPthPowerResidueSymbol eta) (stickelbergerTwoPrimeIdeal v) = totalPthPowerResidueSymbolAtPrime eta v ^ (stickelbergerTwoWeightedScalar p).val

Fractional-ideal form of the corrected weighted-scalar identity.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.totalPthPowerResidueSymbolAtPrime_eq_one_of_stickelbergerTwoResidueProduct_eq_one {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) {eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)} {v : FinitePrime (PrimeCyclotomicField p)} (hweight : HasDirectCharacterSquareResidueWeightAt eta v) (hzero : stickelbergerTwoResidueProduct eta v = 1) : totalPthPowerResidueSymbolAtPrime eta v = 1

A vanishing corrected residue product forces vanishing at its base prime for every prime p ≥ 5.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.jacobiStickelbergerTwoResidueConsumer {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) {eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)} {v : FinitePrime (PrimeCyclotomicField p)} (hweight : HasDirectCharacterSquareResidueWeightAt eta v) (hzero : (fractionalPthPowerResidueSymbol eta) (stickelbergerTwoPrimeIdeal v) = 1) : totalPthPowerResidueSymbolAtPrime eta v = 1

Named downstream consumer for a future Jacobi factorization module. It assumes only the explicit symbol-weight interface and vanishing of the fractional symbol on the corrected ideal; it does not assume that this ideal is principal or generated by a Jacobi sum.