Prime power-residue coordinates for cyclotomic Kummer extensions

This file defines the prime-level p-th power-residue coordinate directly from reduction modulo a finite prime of the prime cyclotomic field. It then compares that coordinate with arithmetic Frobenius on an adjusted integral Kummer radical. No global reciprocity law is asserted here.

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.integralRootsOfUnityEquiv (p : ℕ) [Fact (Nat.Prime p)] : ↥(rootsOfUnity p (NumberField.RingOfIntegers (PrimeCyclotomicField p))) ≃* ↥(rootsOfUnity p (PrimeCyclotomicField p))

The `p`-th roots of unity in the cyclotomic field are already integral. This is the canonical equivalence induced by the inclusion of its ring of integers.

Equations

• NumberTheory.CyclotomicCharacter.InverseExtension.integralRootsOfUnityEquiv p = rootsOfUnityEquivOfPrimitiveRoots ⋯ ⋯

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.rootsOfUnityReductionAt {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) : ↥(rootsOfUnity p (PrimeCyclotomicField p)) →* (NumberField.RingOfIntegers (PrimeCyclotomicField p) ⧸ v.asIdeal)ˣ

Reduction of cyclotomic `p`-th roots of unity at a finite prime.

Equations

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

theorem NumberTheory.CyclotomicCharacter.InverseExtension.rootsOfUnityReductionAt_injective {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : Function.Injective ⇑(rootsOfUnityReductionAt v)

Away from `p`, reduction is injective on the `p`-th roots of unity.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.prime_dvd_absNorm_sub_one {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : p ∣ Ideal.absNorm v.asIdeal - 1

The residue-field cardinality minus one is divisible by `p` at every finite prime away from `p`.

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.residueUnitAt {p : ℕ} (v : FinitePrime (PrimeCyclotomicField p)) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hηv : η ∉ v.asIdeal) : (NumberField.RingOfIntegers (PrimeCyclotomicField p) ⧸ v.asIdeal)ˣ

The nonzero residue class of an integral element at a prime which does not divide it.

Equations

• NumberTheory.CyclotomicCharacter.InverseExtension.residueUnitAt v η hηv = Units.mk0 ((Ideal.Quotient.mk v.asIdeal) η) ⋯

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.residuePowerRootAt {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hηv : η ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : ↥(rootsOfUnity p (NumberField.RingOfIntegers (PrimeCyclotomicField p) ⧸ v.asIdeal))

The finite-field `p`-th power-residue root of a nonzero integral element. Its underlying residue unit is `η ^ ((N v - 1) / p)`.

Equations

• NumberTheory.CyclotomicCharacter.InverseExtension.residuePowerRootAt v η hηv hpv = ⟨NumberTheory.CyclotomicCharacter.InverseExtension.residueUnitAt v η hηv ^ ((Ideal.absNorm v.asIdeal - 1) / p), ⋯⟩

@[simp]

theorem NumberTheory.CyclotomicCharacter.InverseExtension.residuePowerRootAt_coe {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hηv : η ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : ↑(residuePowerRootAt v η hηv hpv) = residueUnitAt v η hηv ^ ((Ideal.absNorm v.asIdeal - 1) / p)

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.pthPowerResidueSymbolAtPrime {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hηv : η ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : ↥(rootsOfUnity p (PrimeCyclotomicField p))

The roots-of-unity-valued prime `p`-th power-residue symbol. It is characterized without choosing a discrete logarithm: its reduction is the finite-field root `η ^ ((N v - 1) / p)`.

Equations

• NumberTheory.CyclotomicCharacter.InverseExtension.pthPowerResidueSymbolAtPrime v η hηv hpv = Classical.choose ⋯

theorem NumberTheory.CyclotomicCharacter.InverseExtension.rootsOfUnityReductionAt_pthPowerResidueSymbolAtPrime {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hηv : η ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : (rootsOfUnityReductionAt v) (pthPowerResidueSymbolAtPrime v η hηv hpv) = ↑(residuePowerRootAt v η hηv hpv)

Defining reduction formula for the prime power-residue symbol.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.pairing_frobeniusAt_eq_pthPowerResidueSymbolAtPrime {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) (v : FinitePrime (PrimeCyclotomicField p)) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (c : (PrimeCyclotomicField p)ˣ) (hη : (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η = P.radicand * ↑c ^ p) (hηv : η ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : (pairing E P) (E.frobeniusAt v) = pthPowerResidueSymbolAtPrime v η hηv hpv

Arithmetic Frobenius in a Kummer presentation is the prime power-residue symbol of any integral representative of the radicand modulo a `p`-th power. The prime is required to divide neither that representative nor `p`.