The product formula for the explicit cyclotomic symbols

For m ≥ 1, the explicit local symbols of ℚ(μ_m)/ℚ are cyclotomicSymbol m ℓ : ℚ_ℓˣ →* (ℤ/m)ˣ at a prime ℓ, sending ℓ^k w with w ∈ ℤ_ℓˣ to the class that is w⁻¹ modulo the ℓ-primary part of m and ℓ^k modulo its prime-to-ℓ part, and the sign realCyclotomicSymbol m at the real place. This file proves their product formula: for a ∈ ℚˣ, the real symbol of a times the symbols of a at the primes dividing m · a is 1 (prod_cyclotomicSymbol).

Both sides are multiplicative in a once the set of primes is fixed, so the formula is proved for an arbitrary finite set T of primes containing those of m and of a (prod_cyclotomicSymbol_of_subset), and there it reduces to the generators -1 and the primes q ∈ T of the group of rationals supported on T. A unit of ℤ/m is determined by its reductions modulo the prime powers p ^ k ∣ m (ZMod.units_eq_of_forall_unitsMap_eq_of_prime_pow_dvd), and modulo p ^ k each generator has at most two nontrivial factors, which cancel:

• at a = -1, the real symbol is -1 and the symbol at p is (-1)⁻¹ = -1;
• at a = p, every factor is trivial;
• at a prime a = q ≠ p, the symbol at p is q⁻¹ and the symbol at q is q.

Main results

• TauCeti.prod_cyclotomicSymbol: the product formula.
• TauCeti.prod_cyclotomicSymbol_of_subset: the product formula over any finite set of primes containing the primes dividing m · a.
• TauCeti.cyclotomicSymbol_mem_of_forall_mem: for positive a, a subgroup containing the symbols of a at every prime other than p contains its symbol at p.

References

• J. S. Milne, Class Field Theory, Chapter VII, Example 8.2, with the values above taken as the definition of the local factors.

theorem TauCeti.prod_cyclotomicSymbol_of_subset (m : ℕ) [NeZero m] (T : Finset ℕ) (hT : ∀ ℓ ∈ T, Nat.Prime ℓ) (hm : m.primeFactors ⊆ T) (a : ℚˣ) (hnum : (↑a).num.natAbs.primeFactors ⊆ T) (hden : (↑a).den.primeFactors ⊆ T) : (realCyclotomicSymbol m) ((Units.map ↑(algebraMap ℚ ℝ)) a) * ∏ ℓ ∈ T.attach, (cyclotomicSymbol m ↑ℓ) ((Units.map ↑(algebraMap ℚ ℚ_[↑ℓ])) a) = 1

The product formula over a set of primes. If T is a finite set of primes containing the primes dividing m, the numerator and the denominator of a ∈ ℚˣ, then the real symbol of a times the symbols of a at the primes of T is 1.

theorem TauCeti.prod_cyclotomicSymbol (m : ℕ) [NeZero m] (a : ℚˣ) : (realCyclotomicSymbol m) ((Units.map ↑(algebraMap ℚ ℝ)) a) * ∏ ℓ ∈ (m * (↑a).num.natAbs * (↑a).den).primeFactors.attach, (cyclotomicSymbol m ↑ℓ) ((Units.map ↑(algebraMap ℚ ℚ_[↑ℓ])) a) = 1

The product formula for the explicit cyclotomic symbols (Milne VII Example 8.2, with these values as the definition of the local factors). For a ∈ ℚˣ, the real symbol times the symbols at the primes dividing m · a is 1: prod_cyclotomicSymbol_of_subset for those primes.

theorem TauCeti.cyclotomicSymbol_mem_of_forall_mem (m : ℕ) [NeZero m] (p : ℕ) [Fact (Nat.Prime p)] (H : Subgroup (ZMod m)ˣ) (a : ℚˣ) (ha : 0 < ↑a) (hdvd : ∀ (ℓ : ℕ) [inst : Fact (Nat.Prime ℓ)], ℓ ∣ m → ℓ ≠ p → (cyclotomicSymbol m ℓ) ((Units.map ↑(algebraMap ℚ ℚ_[ℓ])) a) = 1) (hcop : ∀ (ℓ : ℕ) [inst : Fact (Nat.Prime ℓ)], ¬ℓ ∣ m → (cyclotomicSymbol m ℓ) ((Units.map ↑(algebraMap ℚ ℚ_[ℓ])) a) ∈ H) : (cyclotomicSymbol m p) ((Units.map ↑(algebraMap ℚ ℚ_[p])) a) ∈ H

The product formula isolates the symbol at p. For a ∈ ℚˣ positive, if the symbols of a at the primes ℓ ≠ p dividing m are trivial and those at the primes not dividing m lie in a subgroup H, then so does the symbol of a at p.