Norms from subfields of a cyclotomic field at primes not dividing the level

Let K be a subfield of the n-th cyclotomic field F over ℚ and p a prime not dividing n. The automorphism ζ ↦ ζ ^ p of F is an arithmetic Frobenius at every prime above p, so its f-th power fixes K, where f is the residue degree of a prime of K above p. The p-adic valuation of the absolute norm of an ideal of K, and hence of the norm N_{K/ℚ}(x) of an element of K, is a sum of such residue degrees. So ζ ↦ ζ ^ (p ^ v_p(N_{K/ℚ} x)) fixes K.

This is the contribution of the primes not dividing n to the product formula for the explicit cyclotomic symbols, applied to the norm of an element of K.

Main results

• TauCeti.NumberField.galEquivZMod_symm_pow_inertiaDeg_mem_fixingSubgroup: ζ ↦ ζ ^ (p ^ f) fixes K, for f the residue degree of a prime of K above p.
• TauCeti.NumberField.galEquivZMod_symm_pow_padicValNat_absNorm_mem_fixingSubgroup: the same for the exponent p ^ v_p(𝔑 I), for an ideal I of K.
• TauCeti.NumberField.galEquivZMod_symm_zpow_padicValRat_norm_mem_fixingSubgroup: the same for the exponent p ^ v_p(N_{K/ℚ} x), for x ∈ K.

theorem TauCeti.NumberField.galEquivZMod_symm_pow_inertiaDeg_mem_fixingSubgroup {n : ℕ} [NeZero n] {F : Type u_1} [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] {p : ℕ} [Fact (Nat.Prime p)] (hp : p.Coprime n) (K : IntermediateField ℚ F) (P : Ideal (NumberField.RingOfIntegers ↥K)) [P.IsPrime] [P.LiesOver (Ideal.span {↑p})] : (IsCyclotomicExtension.Rat.galEquivZMod n F).symm (ZMod.unitOfCoprime p hp ^ P.inertiaDeg ℤ) ∈ K.fixingSubgroup

A residue-degree power of p fixes the subfield. Let K be a subfield of the n-th cyclotomic field F and P a prime of K above p ∤ n. Raising roots of unity to the power p ^ f(P/p) fixes K.

theorem TauCeti.NumberField.galEquivZMod_symm_pow_padicValNat_absNorm_mem_fixingSubgroup {n : ℕ} [NeZero n] {F : Type u_1} [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] {p : ℕ} [Fact (Nat.Prime p)] (hp : p.Coprime n) (K : IntermediateField ℚ F) (I : Ideal (NumberField.RingOfIntegers ↥K)) : (IsCyclotomicExtension.Rat.galEquivZMod n F).symm (ZMod.unitOfCoprime p hp ^ padicValNat p (Ideal.absNorm I)) ∈ K.fixingSubgroup

Raising roots of unity to the power p ^ v_p(𝔑 I) fixes K, for every ideal I of a subfield K of the n-th cyclotomic field and p ∤ n.

theorem TauCeti.NumberField.galEquivZMod_symm_zpow_padicValRat_norm_mem_fixingSubgroup {n : ℕ} [NeZero n] {F : Type u_1} [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] {p : ℕ} [Fact (Nat.Prime p)] (hp : p.Coprime n) (K : IntermediateField ℚ F) (x : ↥K) : (IsCyclotomicExtension.Rat.galEquivZMod n F).symm (ZMod.unitOfCoprime p hp ^ padicValRat p ((Algebra.norm ℚ) x)) ∈ K.fixingSubgroup

Norms from a cyclotomic subfield at a prime not dividing the level. For K a subfield of the n-th cyclotomic field, x ∈ K and p ∤ n, raising roots of unity to the power p ^ v_p(N_{K/ℚ} x) fixes K.