The cyclotomic power-residue character

This file packages the elementary finite-field power-residue construction as a MulChar, then specializes it to the canonical primitive root in the ring of integers of the prime cyclotomic field. It proves the reduction formula, the exact order of the character, and its covariance under cyclotomic Galois automorphisms. The final lemma is the finite-field binomial sum vanishing needed by the later Jacobi-sum calculation.

The finite-field exponent and MulChar bridge are adapted from AINT, BernoulliRegular.Reflection.ResidueSymbol.Basic and BernoulliRegular.Reflection.ResidueSymbol.Furtwaengler.Character, commit 1c1c74664e40071c2c2165bc55ca2616a67ccd6b (Chris Birkbeck, 2026-07-31), released under Apache-2.0. The specialization and its consumers are new to this project. No Jacobi ideal factorization or reciprocity theorem is asserted here.

def NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueUnit {k : Type u_1} [Field k] [Fintype k] {p : ℕ} (_hdiv : p ∣ Fintype.card k - 1) (x : kˣ) : kˣ

The finite-field value x ^ ((#k - 1) / p) underlying the p-th power-residue character.

Equations

• NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueUnit _hdiv x = x ^ ((Fintype.card k - 1) / p)

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueUnit_pow_eq_one {k : Type u_1} [Field k] [Fintype k] {p : ℕ} (hdiv : p ∣ Fintype.card k - 1) (x : kˣ) : finiteFieldPowerResidueUnit hdiv x ^ p = 1

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueUnit_mem_zpowers {k : Type u_1} [Field k] [Fintype k] {p : ℕ} [NeZero p] {zeta : kˣ} (hzeta : IsPrimitiveRoot zeta p) (hdiv : p ∣ Fintype.card k - 1) (x : kˣ) : finiteFieldPowerResidueUnit hdiv x ∈ Subgroup.zpowers zeta

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueExponent {k : Type u_1} [Field k] [Fintype k] {p : ℕ} [NeZero p] (zeta : kˣ) (hzeta : IsPrimitiveRoot zeta p) (hdiv : p ∣ Fintype.card k - 1) (x : kˣ) : ZMod p

The discrete-log coordinate of the finite-field power-residue value with respect to a chosen primitive p-th root.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.zeta_pow_finiteFieldPowerResidueExponent_val {k : Type u_1} [Field k] [Fintype k] {p : ℕ} [NeZero p] {zeta : kˣ} (hzeta : IsPrimitiveRoot zeta p) (hdiv : p ∣ Fintype.card k - 1) (x : kˣ) : zeta ^ (finiteFieldPowerResidueExponent zeta hzeta hdiv x).val = finiteFieldPowerResidueUnit hdiv x

The exponent coordinate recovers the concrete finite-field power.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueUnit_mul {k : Type u_1} [Field k] [Fintype k] {p : ℕ} (hdiv : p ∣ Fintype.card k - 1) (x y : kˣ) : finiteFieldPowerResidueUnit hdiv (x * y) = finiteFieldPowerResidueUnit hdiv x * finiteFieldPowerResidueUnit hdiv y

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueUnit_one {k : Type u_1} [Field k] [Fintype k] {p : ℕ} (hdiv : p ∣ Fintype.card k - 1) : finiteFieldPowerResidueUnit hdiv 1 = 1

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueExponent_mul {k : Type u_1} [Field k] [Fintype k] {p : ℕ} [NeZero p] (zeta : kˣ) (hzeta : IsPrimitiveRoot zeta p) (hdiv : p ∣ Fintype.card k - 1) (x y : kˣ) : finiteFieldPowerResidueExponent zeta hzeta hdiv (x * y) = finiteFieldPowerResidueExponent zeta hzeta hdiv x + finiteFieldPowerResidueExponent zeta hzeta hdiv y

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueExponent_one {k : Type u_1} [Field k] [Fintype k] {p : ℕ} [NeZero p] (zeta : kˣ) (hzeta : IsPrimitiveRoot zeta p) (hdiv : p ∣ Fintype.card k - 1) : finiteFieldPowerResidueExponent zeta hzeta hdiv 1 = 0

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueUnitHom {k : Type u_1} [Field k] [Fintype k] {R' : Type u_2} [CommMonoidWithZero R'] {p : ℕ} [NeZero p] (zeta_q : kˣ) (hzeta_q : IsPrimitiveRoot zeta_q p) (hdiv : p ∣ Fintype.card k - 1) (zeta_R : R'ˣ) (hzeta_R : IsPrimitiveRoot zeta_R p) : kˣ →* R'ˣ

The unit-group homomorphism underlying the power-residue character.

Equations

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

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueMulChar {k : Type u_1} [Field k] [Fintype k] {R' : Type u_2} [CommMonoidWithZero R'] {p : ℕ} [NeZero p] (zeta_q : kˣ) (hzeta_q : IsPrimitiveRoot zeta_q p) (hdiv : p ∣ Fintype.card k - 1) (zeta_R : R'ˣ) (hzeta_R : IsPrimitiveRoot zeta_R p) : MulChar k R'

The finite-field p-th power-residue character with values in any ring containing a chosen primitive p-th root.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueMulChar_apply_unit {k : Type u_1} [Field k] [Fintype k] {R' : Type u_2} [CommMonoidWithZero R'] {p : ℕ} [NeZero p] (zeta_q : kˣ) (hzeta_q : IsPrimitiveRoot zeta_q p) (hdiv : p ∣ Fintype.card k - 1) (zeta_R : R'ˣ) (hzeta_R : IsPrimitiveRoot zeta_R p) (x : kˣ) : (finiteFieldPowerResidueMulChar zeta_q hzeta_q hdiv zeta_R hzeta_R) ↑x = ↑zeta_R ^ (finiteFieldPowerResidueExponent zeta_q hzeta_q hdiv x).val

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueMulChar_apply_unit_pow_eq_one {k : Type u_1} [Field k] [Fintype k] {R' : Type u_2} [CommMonoidWithZero R'] {p : ℕ} [NeZero p] (zeta_q : kˣ) (hzeta_q : IsPrimitiveRoot zeta_q p) (hdiv : p ∣ Fintype.card k - 1) (zeta_R : R'ˣ) (hzeta_R : IsPrimitiveRoot zeta_R p) (x : kˣ) : (finiteFieldPowerResidueMulChar zeta_q hzeta_q hdiv zeta_R hzeta_R) ↑x ^ p = 1

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueMulChar_pow_eq_one {k : Type u_1} [Field k] [Fintype k] {R' : Type u_2} [CommMonoidWithZero R'] {p : ℕ} [NeZero p] (zeta_q : kˣ) (hzeta_q : IsPrimitiveRoot zeta_q p) (hdiv : p ∣ Fintype.card k - 1) (zeta_R : R'ˣ) (hzeta_R : IsPrimitiveRoot zeta_R p) : finiteFieldPowerResidueMulChar zeta_q hzeta_q hdiv zeta_R hzeta_R ^ p = 1

theorem NumberTheory.CyclotomicCharacter.InverseExtension.orderOf_finiteFieldPowerResidueMulChar {k : Type u_1} [Field k] [Fintype k] {p : ℕ} {R' : Type u_3} [CommRing R'] [IsDomain R'] [Fact (Nat.Prime p)] (zeta_q : kˣ) (hzeta_q : IsPrimitiveRoot zeta_q p) (hdiv : p ∣ Fintype.card k - 1) (zeta_R : R'ˣ) (hzeta_R : IsPrimitiveRoot zeta_R p) : orderOf (finiteFieldPowerResidueMulChar zeta_q hzeta_q hdiv zeta_R hzeta_R) = p

The power-residue character has exact order p when p is prime.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.finiteFieldPowerResidueMulChar_ringHomComp_pow_eq {k : Type u_1} [Field k] [Fintype k] {p : ℕ} {R' : Type u_3} [CommRing R'] [NeZero p] (zeta_q : kˣ) (hzeta_q : IsPrimitiveRoot zeta_q p) (hdiv : p ∣ Fintype.card k - 1) (zeta_R : R'ˣ) (hzeta_R : IsPrimitiveRoot zeta_R p) (σ : R' →+* R') (a : ℕ) (hσ : σ ↑zeta_R = ↑zeta_R ^ a) : (finiteFieldPowerResidueMulChar zeta_q hzeta_q hdiv zeta_R hzeta_R).ringHomComp σ = finiteFieldPowerResidueMulChar zeta_q hzeta_q hdiv zeta_R hzeta_R ^ a

Postcomposition by a map carrying the target primitive root to its a-th power carries the residue character to its a-th power.

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

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.integralCyclotomicZetaUnit (p : ℕ) [Fact (Nat.Prime p)] : (NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p)ˣ

The canonical primitive cyclotomic root, regarded as a unit in the ring of integers.

Equations

• NumberTheory.CyclotomicCharacter.InverseExtension.integralCyclotomicZetaUnit p = ↑((NumberTheory.CyclotomicCharacter.InverseExtension.integralRootsOfUnityEquiv p).symm ⋯.toRootsOfUnity)

theorem NumberTheory.CyclotomicCharacter.InverseExtension.integralCyclotomicZetaUnit_isPrimitiveRoot {p : ℕ} [Fact (Nat.Prime p)] : IsPrimitiveRoot (integralCyclotomicZetaUnit p) p

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicResidueZeta {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) : (NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p ⧸ v.asIdeal)ˣ

Reduction of the canonical integral cyclotomic root at a finite prime.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.cyclotomicResidueZeta_isPrimitiveRoot {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : IsPrimitiveRoot (cyclotomicResidueZeta v) p

theorem NumberTheory.CyclotomicCharacter.InverseExtension.residueField_card_eq_absNorm {p : ℕ} (v : FinitePrime (PrimeCyclotomicField p)) : Nat.card (NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p ⧸ v.asIdeal) = Ideal.absNorm v.asIdeal

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

The canonical p-th power-residue character at a finite prime away from p, valued in the cyclotomic integer ring.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.quotientMap_cyclotomicPowerResidueChar_apply_unit {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) (x : (NumberTheory.CyclotomicCharacter.InverseExtension.CyclotomicIntegerRing✝ p ⧸ v.asIdeal)ˣ) : (Ideal.Quotient.mk v.asIdeal) ((cyclotomicPowerResidueChar v hpv) ↑x) = ↑x ^ ((Ideal.absNorm v.asIdeal - 1) / p)

Reduction of the character value recovers x ^ ((N v - 1) / p) in the residue field.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.orderOf_cyclotomicPowerResidueChar {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : orderOf (cyclotomicPowerResidueChar v hpv) = p

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

Cyclotomic Galois automorphisms postcompose the canonical character by the corresponding direct-character power.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.sum_pow_mul_one_sub_pow_eq_zero (F : Type u_1) [Field F] [Fintype F] (d : ℕ) (hd : 2 * d < Fintype.card F - 1) : ∑ x : F, x ^ d * (1 - x) ^ d = 0

A binomial power sum over a finite field vanishes while every monomial in its expansion has degree strictly below the size of the unit group.