Algebra of cyclotomic power-residue symbols

This file proves multiplication and p-th-power formulas in the numerator of the direct power-residue symbol. Total-symbol multiplication is stated only away from both numerators and p: the total symbol is deliberately set to one at bad primes, so an unconditional multiplication formula would be false. The corresponding fractional formula therefore carries explicit support-avoidance hypotheses.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.pthPowerResidueSymbolAtPrime_mul {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (eta xi : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (heta : eta ∉ v.asIdeal) (hxi : xi ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : pthPowerResidueSymbolAtPrime v (eta * xi) ⋯ hpv = pthPowerResidueSymbolAtPrime v eta heta hpv * pthPowerResidueSymbolAtPrime v xi hxi hpv

Away from both numerators and p, the direct prime power-residue symbol is multiplicative in its numerator.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.pthPowerResidueSymbolAtPrime_pow_prime_eq_one {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (heta : eta ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : pthPowerResidueSymbolAtPrime v (eta ^ p) ⋯ hpv = 1

Away from its numerator and p, the direct symbol of a p-th-power numerator is one.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.totalPthPowerResidueSymbolAtPrime_mul_of_not_mem {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (eta xi : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (heta : eta ∉ v.asIdeal) (hxi : xi ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : totalPthPowerResidueSymbolAtPrime (eta * xi) v = totalPthPowerResidueSymbolAtPrime eta v * totalPthPowerResidueSymbolAtPrime xi v

The total prime symbol is multiplicative in the numerator provided the prime avoids both numerators and p.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.totalPthPowerResidueSymbolAtPrime_pow_prime_eq_one {p : ℕ} [Fact (Nat.Prime p)] (v : FinitePrime (PrimeCyclotomicField p)) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) : totalPthPowerResidueSymbolAtPrime (eta ^ p) v = 1

The total symbol of a p-th-power numerator is one at every finite prime, including the primes where the direct symbol is not defined.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_mul_of_support {p : ℕ} [Fact (Nat.Prime p)] (eta xi : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ) (heta : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers (PrimeCyclotomicField p))), ((UnramifiedArtin.fractionalIdealDivisor (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Additive.ofMul I)) v ≠ 0 → eta ∉ v.asIdeal) (hxi : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers (PrimeCyclotomicField p))), ((UnramifiedArtin.fractionalIdealDivisor (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Additive.ofMul I)) v ≠ 0 → xi ∉ v.asIdeal) (hp : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers (PrimeCyclotomicField p))), ((UnramifiedArtin.fractionalIdealDivisor (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Additive.ofMul I)) v ≠ 0 → ↑p ∉ v.asIdeal) : (fractionalPthPowerResidueSymbol (eta * xi)) I = (fractionalPthPowerResidueSymbol eta) I * (fractionalPthPowerResidueSymbol xi) I

On a fractional ideal whose divisor support avoids both numerators and p, the fractional residue product is multiplicative in the numerator.

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

A p-th-power numerator has trivial residue product on every nonzero fractional ideal.