The second cyclotomic Jacobi sum

This file specializes Mathlib's Jacobi-sum API to the canonical cyclotomic power-residue character. It records Galois covariance, complex conjugation, the elementary absolute-value identity, semiprimary congruence, and the exact two-character Gauss-sum relation. These are the narrow Jacobi-sum inputs intended for the cyclotomic reciprocity consumer in KummerArtinProduct.

The Jacobi-sum definition and general identities come from Mathlib.NumberTheory.JacobiSum.Basic, by Michael Stoll (2024), released under Apache-2.0 and following Ireland--Rosen, A Classical Introduction to Modern Number Theory, Section 8.3. No Jacobi ideal factorization, Artin reciprocity, or cyclotomic reciprocity theorem is asserted here.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.instNeZeroNat_1 {p : ℕ} [Fact (Nat.Prime p)] : NeZero p

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicIntegerComplexConj (p : ℕ) [Fact (Nat.Prime p)] (hp : 2 < p) : NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p ≃+* NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p

Complex conjugation on the integers of the prime cyclotomic field.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicPowerResidueChar_ringHomComp_complexConj {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : (cyclotomicPowerResidueChar v hpv).ringHomComp (cyclotomicIntegerComplexConj p hp).toRingHom = (cyclotomicPowerResidueChar v hpv)⁻¹

Complex conjugation sends the canonical power-residue character to its inverse.

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicJacobiSumTwo {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p

The canonical diagonal Jacobi sum J(χ_v, χ_v) at a finite prime away from p.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicJacobiSumTwo_galois {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) (σ : Gal(PrimeCyclotomicField p/ℚ)) : (baseIntegerEquiv σ) (cyclotomicJacobiSumTwo v hpv) = jacobiSum (cyclotomicPowerResidueChar v hpv ^ (↑((directCharacter p) σ)).val) (cyclotomicPowerResidueChar v hpv ^ (↑((directCharacter p) σ)).val)

Cyclotomic Galois action carries J(χ_v, χ_v) to the Jacobi sum of the corresponding powers of χ_v.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicJacobiSumTwo_complexConj {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : (cyclotomicIntegerComplexConj p hp) (cyclotomicJacobiSumTwo v hpv) = jacobiSum (cyclotomicPowerResidueChar v hpv)⁻¹ (cyclotomicPowerResidueChar v hpv)⁻¹

Complex conjugation of J(χ_v, χ_v) is J(χ_v⁻¹, χ_v⁻¹).

theorem NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicJacobiSumTwo_mul_complexConj {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : cyclotomicJacobiSumTwo v hpv * (cyclotomicIntegerComplexConj p hp) (cyclotomicJacobiSumTwo v hpv) = ↑(Ideal.absNorm v.asIdeal)

The elementary absolute-value identity J(χ_v,χ_v) * conj(J(χ_v,χ_v)) = N(v).

theorem NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicJacobiSumTwo_ne_zero {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : cyclotomicJacobiSumTwo v hpv ≠ 0

The canonical diagonal cyclotomic Jacobi sum is nonzero.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.gaussSum_mul_cyclotomicJacobiSumTwo {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) (ψ : AddChar (NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p ⧸ v.asIdeal) (NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p)) : gaussSum (cyclotomicPowerResidueChar v hpv * cyclotomicPowerResidueChar v hpv) ψ * cyclotomicJacobiSumTwo v hpv = gaussSum (cyclotomicPowerResidueChar v hpv) ψ * gaussSum (cyclotomicPowerResidueChar v hpv) ψ

The Jacobi sum satisfies the exact two-character Gauss-sum relation.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicJacobiSumTwo_semiprimary {p : ℕ} [Fact (Nat.Prime p)] (hp : 2 < p) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : ∃ z ∈ ℤ[↑(integralCyclotomicZetaUnit p)], cyclotomicJacobiSumTwo v hpv = -1 + z * (↑(integralCyclotomicZetaUnit p) - 1) ^ 2

The canonical diagonal cyclotomic Jacobi sum is semiprimary: J(χ_v,χ_v) = -1 modulo (ζ_p - 1)^2.