The cyclotomic character along a finite extension

Let L/K be a finite extension embedded in a separable closure Kˢ by σ. The absolute Galois group G_L is identified with the open subgroup of G_K fixing σ(L), and absoluteGaloisGroupExtend K L σ : G_L →* G_K is the resulting embedding. Since G_L acts on the roots of unity of Lˢ = Kˢ through this embedding, the p-adic cyclotomic character of G_L is the restriction of that of G_K:

χ_K (absoluteGaloisGroupExtend K L σ τ) = χ_L τ.

This is the comparison through which a statement about the cyclotomic character of G_K, such as its value on the image of a local Artin symbol, passes to finite extensions of K by norm functoriality.

The characters localCyclotomicCharacter p K are defined on Mathlib's absolute Galois group, at the algebraic closure, while absoluteGaloisGroupExtend is built from separable closures. The comparison therefore first computes the character at the separable closure (cyclotomicCharacter_absoluteGaloisGroupRestrictEquiv). Both steps are instances of the naturality of the cyclotomic character, TauCeti.cyclotomicCharacter_eq_of_injective. No hypothesis on the characteristic is needed: when p is the characteristic, all characters involved are trivial.

Main results

• TauCeti.cyclotomicCharacter_absoluteGaloisGroupRestrictEquiv: the cyclotomic character of G_K may be computed on the separable closure.
• TauCeti.localCyclotomicCharacter_absoluteGaloisGroupExtend, TauCeti.localCyclotomicCharacter_comp_absoluteGaloisGroupExtend: the cyclotomic character of G_L is that of G_K read through absoluteGaloisGroupExtend K L σ.

@[simp]

theorem TauCeti.cyclotomicCharacter_absoluteGaloisGroupRestrictEquiv (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (g : Field.absoluteGaloisGroup K) : (cyclotomicCharacter (SeparableClosure K) p) ((absoluteGaloisGroupRestrictEquiv K) g).toRingEquiv = (localCyclotomicCharacter p K) g

The cyclotomic character at the separable closure. The cyclotomic character of g ∈ Gal(AlgebraicClosure K/K) is that of its restriction to the separable closure.

theorem TauCeti.localCyclotomicCharacter_absoluteGaloisGroupExtend (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (τ : Field.absoluteGaloisGroup L) : (localCyclotomicCharacter p K) ((absoluteGaloisGroupExtend K L σ) τ) = (localCyclotomicCharacter p L) τ

The cyclotomic character along a finite extension. For L/K finite embedded in Kˢ by σ, the cyclotomic character of τ ∈ G_L is that of its image in G_K.

@[simp]

theorem TauCeti.localCyclotomicCharacter_comp_absoluteGaloisGroupExtend (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : (localCyclotomicCharacter p K).comp (absoluteGaloisGroupExtend K L σ) = localCyclotomicCharacter p L

The cyclotomic character of G_L is that of G_K read through absoluteGaloisGroupExtend K L σ.