Galois covariance of cyclotomic power-residue symbols

This file proves that the direct p-th power-residue symbol is equivariant for the natural Galois actions on its numerator and finite prime. The same formula is then extended to the total prime symbol and to nonzero fractional ideals.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.baseIntegerEquiv_mem_mapFinitePrime_iff {p : ℕ} (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) : (baseIntegerEquiv sigma) eta ∈ ((mapFinitePrime sigma) v).asIdeal ↔ eta ∈ v.asIdeal

Membership in a finite prime is preserved by simultaneous Galois transport of the element and the prime.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.baseIntegerEquiv_not_mem_mapFinitePrime {p : ℕ} (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (heta : eta ∉ v.asIdeal) : (baseIntegerEquiv sigma) eta ∉ ((mapFinitePrime sigma) v).asIdeal

Nonmembership in a finite prime is preserved by simultaneous Galois transport of the element and the prime.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.prime_not_mem_mapFinitePrime {p : ℕ} (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) : ↑p ∉ ((mapFinitePrime sigma) v).asIdeal

The rational prime remains outside a transported finite prime whenever it was outside the original prime.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.pthPowerResidueSymbolAtPrime_mapFinitePrime {p : ℕ} [Fact (Nat.Prime p)] (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (heta : eta ∉ v.asIdeal) (hpv : ↑p ∉ v.asIdeal) : pthPowerResidueSymbolAtPrime ((mapFinitePrime sigma) v) ((baseIntegerEquiv sigma) eta) ⋯ ⋯ = pthPowerResidueSymbolAtPrime v eta heta hpv ^ (↑((directCharacter p) sigma)).val

The direct prime p-th power-residue symbol is Galois covariant when both its numerator and finite prime are transported.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.totalPthPowerResidueSymbolAtPrime_mapFinitePrime {p : ℕ} [Fact (Nat.Prime p)] (sigma : Gal(PrimeCyclotomicField p/ℚ)) (v : FinitePrime (PrimeCyclotomicField p)) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) : totalPthPowerResidueSymbolAtPrime ((baseIntegerEquiv sigma) eta) ((mapFinitePrime sigma) v) = totalPthPowerResidueSymbolAtPrime eta v ^ (↑((directCharacter p) sigma)).val

The total prime p-th power-residue symbol is Galois covariant. At primes dividing the numerator or p, both sides are one.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.fractionalPthPowerResidueSymbol_map {p : ℕ} [Fact (Nat.Prime p)] (sigma : Gal(PrimeCyclotomicField p/ℚ)) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (PrimeCyclotomicField p))ˣ) : (fractionalPthPowerResidueSymbol ((baseIntegerEquiv sigma) eta)) ((fractionalIdealEquiv sigma) I) = (fractionalPthPowerResidueSymbol eta) I ^ (↑((directCharacter p) sigma)).val

The fractional p-th power-residue symbol is Galois covariant under simultaneous transport of its integral numerator and fractional ideal.