Finite residue products for normalized cyclotomic pseudo-units

This file extends the direct prime power-residue symbol to a total family of local symbols and then to nonzero fractional ideals. The total symbol is defined to be one at primes dividing its numerator or the rational prime `p`; away from those primes it is the direct finite-field symbol.

For a normalized pseudo-unit `η` with `(η) = B ^ p`, the resulting product is trivial on `(η)`. For a principal denominator `(a)` coprime to both `η` and the cyclotomic prime, the Kummer--Frobenius product is identified with the product having numerator `η`. Thus the integral Kummer target is reduced, by checked equivalences, to equality of the two oppositely oriented finite residue products. No equality of those products is assumed here.

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

A total prime-level power-residue symbol. At primes where the usual symbol is undefined because the numerator or `p` vanishes, its value is set to one.

Equations

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

@[simp]

theorem NumberTheory.CyclotomicCharacter.InverseExtension.totalPthPowerResidueSymbolAtPrime_of_numerator_mem {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (v : FinitePrime (PrimeCyclotomicField p)) (hηv : η ∈ v.asIdeal) : totalPthPowerResidueSymbolAtPrime η v = 1

@[simp]

theorem NumberTheory.CyclotomicCharacter.InverseExtension.totalPthPowerResidueSymbolAtPrime_of_prime_mem {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∈ v.asIdeal) : totalPthPowerResidueSymbolAtPrime η v = 1

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

noncomputable def NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ →* ↥(rootsOfUnity p (PrimeCyclotomicField p))

The finite product of total prime power-residue symbols over a nonzero fractional ideal.

Equations

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

@[simp]

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_prime {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (v : FinitePrime (PrimeCyclotomicField p)) : (fractionalPthPowerResidueSymbol η) (UnramifiedArtin.primeFractionalIdealUnit v) = totalPthPowerResidueSymbolAtPrime η v

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_apply {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ) : (fractionalPthPowerResidueSymbol η) I = ((UnramifiedArtin.fractionalIdealDivisor (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Additive.ofMul I)).prod fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (n : ℤ) => totalPthPowerResidueSymbolAtPrime η v ^ n

Explicit finite-product formula for the total power-residue symbol.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_pow_eq_one {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ) : (fractionalPthPowerResidueSymbol η) I ^ p = 1

Every total residue product has exponent dividing `p`.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_ideal_pow_eq_one {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ) : (fractionalPthPowerResidueSymbol η) (I ^ p) = 1

Consequently the total residue product kills every `p`-th power of a nonzero fractional ideal.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_principal_eq_one_of_span_eq_pow {p : ℕ} [Fact (Nat.Prime p)] (ξ η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hη : η ≠ 0) (B : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (hspan : Ideal.span {η} = B ^ p) : (fractionalPthPowerResidueSymbol ξ) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η) ⋯)) = 1

If the principal ideal of `η` is a `p`-th power, every total residue product is trivial on `(η)`, independently of the numerator used in that product.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.fractionalKummerSymbol_integralPrincipal_eq_residueProduct {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) (η a : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (ha : a ≠ 0) (c : (PrimeCyclotomicField p)ˣ) (hη : (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η = P.radicand * ↑c ^ p) (hcoprimeηa : IsCoprime (Ideal.span {η}) (Ideal.span {a})) (hcoprimeaPrime : IsCoprime (Ideal.span {a}) (cyclotomicPrime p).asIdeal) : (fractionalKummerSymbol E P) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) a) ⋯)) = (fractionalPthPowerResidueSymbol η) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) a) ⋯))

On an integral principal ideal coprime to both the normalized numerator and the cyclotomic prime, the Kummer--Frobenius product is the finite power-residue product with that normalized numerator.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.integralProduct_eq_one_iff_twoSidedResidueProduct {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) (η a : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hηne : η ≠ 0) (ha : a ≠ 0) (c : (PrimeCyclotomicField p)ˣ) (hη : (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η = P.radicand * ↑c ^ p) (B : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (hspan : Ideal.span {η} = B ^ p) (hcoprimeηa : IsCoprime (Ideal.span {η}) (Ideal.span {a})) (hcoprimeaPrime : IsCoprime (Ideal.span {a}) (cyclotomicPrime p).asIdeal) : (fractionalKummerSymbol E P) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) a) ⋯)) = 1 ↔ (fractionalPthPowerResidueSymbol η) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) a) ⋯)) = (fractionalPthPowerResidueSymbol a) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η) ⋯))

For normalized data, the integral Kummer product target is equivalent to equality of the two oppositely oriented finite residue products. The reverse product is one because the principal ideal of the normalized numerator is a p-th power; no reciprocity equality is asserted.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.exists_normalization_integralProduct_eq_one_iff_twoSidedResidueProduct {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (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)ˣ) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (B : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (hηne : η ≠ 0), (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η = E.kummerPresentation.radicand * ↑c ^ p ∧ Ideal.span {η} = B ^ p ∧ IsCoprime (Ideal.span {η}) (Ideal.span {a}) ∧ IsCoprime (Ideal.span {η}) (cyclotomicPrime p).asIdeal ∧ (fractionalPthPowerResidueSymbol a) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η) ⋯)) = 1 ∧ ((KummerPresentation.fractionalKummerSymbol E E.kummerPresentation) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) a) ⋯)) = 1 ↔ (fractionalPthPowerResidueSymbol η) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) a) ⋯)) = (fractionalPthPowerResidueSymbol a) ((toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η) ⋯)))

A pseudo-unit normalization packages the integral Kummer target as the remaining two-sided finite residue-product identity. In particular, this theorem records a checked reduction, not an assumption or a proof of that identity.