Explicit local symbols for cyclotomic extensions of the rationals #

For a prime p and a positive modulus m, this file defines the explicit homomorphism

cyclotomicSymbol m p : ℚ_pˣ →* (ZMod m)ˣ.

Write m = p ^ j * d, with p ∤ d, and x = p ^ k w, with w ∈ ℤ_pˣ. The symbol is the unique residue class which is w⁻¹ modulo p ^ j and p ^ k modulo d. The two reduction theorems in this file characterize it without exposing its Chinese-remainder construction. The real symbol is the sign, viewed in (ZMod m)ˣ.

These are the local factors in the elementary product formula for cyclotomic extensions of ℚ. The normalization follows J. S. Milne, Class Field Theory, VII, Example 8.2.

Main definitions #

TauCeti.cyclotomicSymbol: the explicit symbol at a finite prime.
TauCeti.realCyclotomicSymbol: the explicit symbol at the real place.

Main results #

TauCeti.unitsMap_cyclotomicSymbol_primePow: on the p-primary part of the modulus, the symbol is the inverse of the unit part.
TauCeti.unitsMap_cyclotomicSymbol_of_coprime: on every divisor of the modulus coprime to p, the symbol is the valuation part p ^ k.
TauCeti.unitsMap_cyclotomicSymbol_primePow_of_eq_unit, TauCeti.unitsMap_cyclotomicSymbol_of_coprime_of_eq_unit, TauCeti.unitsMap_cyclotomicSymbol_self_primePow and TauCeti.unitsMap_cyclotomicSymbol_self_of_coprime: the two reductions at a p-adic unit and at p itself.
TauCeti.cyclotomicSymbol_of_coprime: at a prime not dividing the modulus, the symbol is p raised to the valuation.
TauCeti.cyclotomicSymbol_eq_one_of_norm_sub_one_lt and TauCeti.cyclotomicSymbol_eq_of_norm_sub_lt: the symbol is trivial near 1, hence locally constant.
TauCeti.realCyclotomicSymbol_of_pos and TauCeti.realCyclotomicSymbol_of_neg: the two values of the real symbol.

source

noncomputable def TauCeti.cyclotomicSymbol (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] :

ℚ_[p]ˣ →* (ZMod m)ˣ

The explicit local symbol of ℚ(μ_m)/ℚ at p. If m = p ^ j * d, with p ∤ d, and x = p ^ k w, with w ∈ ℤ_pˣ, then the symbol is the unique class in (ZMod m)ˣ which is w⁻¹ modulo p ^ j and p ^ k modulo d.

The two components are recorded by unitsMap_cyclotomicSymbol_primePow and unitsMap_cyclotomicSymbol_of_coprime.

Instances For

source

theorem TauCeti.unitsMap_cyclotomicSymbol_primePow (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] {j : ℕ} (hj : p ^ j ∣ m) (x : ℚ_[p]ˣ) (k : ℤ) (w : ℤ_[p]ˣ) (hx : ↑x = ↑p ^ k * ↑↑w) :

(ZMod.unitsMap hj) ((cyclotomicSymbol m p) x) = ((Units.map ↑(PadicInt.toZModPow j)) w)⁻¹

On a prime-power divisor p ^ j of the modulus, the explicit local cyclotomic symbol is the inverse of the reduction of the p-adic unit part.

source

theorem TauCeti.unitsMap_cyclotomicSymbol_of_coprime (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] {d : ℕ} (hd : d ∣ m) (hcop : p.Coprime d) (x : ℚ_[p]ˣ) (k : ℤ) (w : ℤ_[p]ˣ) (hx : ↑x = ↑p ^ k * ↑↑w) :

(ZMod.unitsMap hd) ((cyclotomicSymbol m p) x) = ZMod.unitOfCoprime p hcop ^ k

On a divisor d of the modulus coprime to p, the explicit local cyclotomic symbol is p ^ k, where k is the normalized valuation.

source

theorem TauCeti.unitsMap_cyclotomicSymbol_primePow_of_eq_unit (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] {j : ℕ} (hj : p ^ j ∣ m) {x : ℚ_[p]ˣ} {w : ℤ_[p]ˣ} (hx : ↑x = ↑↑w) :

(ZMod.unitsMap hj) ((cyclotomicSymbol m p) x) = ((Units.map ↑(PadicInt.toZModPow j)) w)⁻¹

Modulo a power of p dividing m, the symbol at p of a p-adic unit w is w⁻¹.

source

theorem TauCeti.unitsMap_cyclotomicSymbol_of_coprime_of_eq_unit (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] {d : ℕ} (hd : d ∣ m) (hcop : p.Coprime d) {x : ℚ_[p]ˣ} {w : ℤ_[p]ˣ} (hx : ↑x = ↑↑w) :

(ZMod.unitsMap hd) ((cyclotomicSymbol m p) x) = 1

Modulo a divisor of m prime to p, the symbol at p of a p-adic unit is trivial.

source

theorem TauCeti.unitsMap_cyclotomicSymbol_self_primePow (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] {j : ℕ} (hj : p ^ j ∣ m) {x : ℚ_[p]ˣ} (hx : ↑x = ↑p) :

(ZMod.unitsMap hj) ((cyclotomicSymbol m p) x) = 1

Modulo a power of p dividing m, the symbol of p at p is trivial.

source

theorem TauCeti.unitsMap_cyclotomicSymbol_self_of_coprime (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] {d : ℕ} (hd : d ∣ m) (hcop : p.Coprime d) {x : ℚ_[p]ˣ} (hx : ↑x = ↑p) :

(ZMod.unitsMap hd) ((cyclotomicSymbol m p) x) = ZMod.unitOfCoprime p hcop

Modulo a divisor of m prime to p, the symbol of p at p is the class of p.

source

theorem TauCeti.cyclotomicSymbol_of_coprime (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] (hcop : p.Coprime m) (x : ℚ_[p]ˣ) :

(cyclotomicSymbol m p) x = ZMod.unitOfCoprime p hcop ^ (↑x).valuation

At a prime p not dividing the modulus, the explicit local cyclotomic symbol is p raised to the p-adic valuation.

source

theorem TauCeti.eq_cyclotomicSymbol_of_cast_eq (p : ℕ) [Fact (Nat.Prime p)] {k : ℤ} {u : ℤ_[p]ˣ} {x : ℚ_[p]ˣ} (hx : ↑x = ↑p ^ k * ↑↑u) {n N : ℕ} (hpN : p.Coprime N) [NeZero (p ^ n * N)] {r : ZMod (p ^ n * N)} (hrP : r.cast = (PadicInt.toZModPow n) ↑u⁻¹) (hrN : r.cast = ↑(ZMod.unitOfCoprime p hpN ^ k)) :

r = ↑((cyclotomicSymbol (p ^ n * N) p) x)

If an element of ℤ/(pⁿ N)ℤ reduces modulo pⁿ to the inverse of u and modulo N to p ^ k, where N is coprime to p, then it is the explicit symbol of any x = p ^ k u.

source

theorem TauCeti.cyclotomicSymbol_eq_one_of_norm_sub_one_lt (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] (x : ℚ_[p]ˣ) (hx : ‖↑x - 1‖ < ‖↑m‖) :

(cyclotomicSymbol m p) x = 1

The explicit local cyclotomic symbol is trivial near 1: it kills every unit x with ‖x - 1‖ < ‖m‖, that is, every unit congruent to 1 modulo a higher power of p than the one dividing m.

source