Naturality of the cyclotomic character and of the cyclotomic orientation

For a field extension L/K, Mathlib's map Field.absoluteGaloisGroup.mapOfAlgebra K L : G_L → G_K restricts automorphisms along an embedding Kᵃˡᵍ → Lᵃˡᵍ of algebraic closures. The embedding identifies the p-power roots of unity of Kᵃˡᵍ with those of Lᵃˡᵍ, so the cyclotomic character is natural:

χ_K (mapOfAlgebra K L g) = χ_L g.

If K contains a primitive pth root of unity, so does L, and both maximal pro-p Galois groups carry the cyclotomic orientation cyclotomicOrientation. A continuous homomorphism f : G_L → G_K compatible with the two cyclotomic characters induces maximalProPQuotient.map f : G_L(p) → G_K(p), and the orientation of G_K(p) pulls back to that of G_L(p) along it. This applies to mapOfAlgebra K L for an arbitrary extension, and to the embedding absoluteGaloisGroupExtend K L σ : G_L → G_K of a finite extension.

For an isomorphism of fields e : K ≃+* L, the map of absolute Galois groups is an isomorphism absoluteGaloisGroupMapEquiv e : G_L ≃ₜ* G_K, hence so is the induced map maximalProPQuotient.congr (absoluteGaloisGroupMapEquiv e) : G_L(p) ≃ₜ* G_K(p), and it carries the cyclotomic orientation of G_L(p) to that of G_K(p). A marked presentation of G_K(p), that is, an isomorphism m : G_K(p) ≃ₜ* P onto a presented group together with the values cyclotomicOrientation p K hmu (m.symm x) on its generators, therefore transports to the marked presentation (maximalProPQuotient.congr (absoluteGaloisGroupMapEquiv e)).trans m of G_L(p) with the same values (cyclotomicOrientation_maximalProPQuotient_congr_symm). When e is an isomorphism of finite extensions of ℚ_p, the degree and the number of p-power roots of unity, which determine the relator, are also preserved (LinearEquiv.finrank_eq, localRootOfUnityOrder_eq_of_ringEquiv).

Main results

• TauCeti.cyclotomicCharacter_absoluteGaloisGroupMap: the cyclotomic character of G_L is that of G_K read through the map absoluteGaloisGroupMap τ of absolute Galois groups defined by an embedding of separable closures.
• TauCeti.cyclotomicOrientation_maximalProPQuotient_map: the cyclotomic orientation is natural along any continuous homomorphism of absolute Galois groups compatible with the cyclotomic characters.
• TauCeti.cyclotomicOrientation_maximalProPQuotient_map_mapOfAlgebra, TauCeti.cyclotomicOrientation_maximalProPQuotient_map_absoluteGaloisGroupExtend: its instances along an arbitrary extension and along a finite extension.
• TauCeti.cyclotomicOrientation_maximalProPQuotient_congr, TauCeti.cyclotomicOrientation_maximalProPQuotient_congr_symm: an isomorphism of fields induces an isomorphism of maximal pro-p Galois groups preserving the cyclotomic orientation.

theorem TauCeti.cyclotomicCharacter_absoluteGaloisGroupMap (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (g : AbsoluteGaloisGroup L) : (cyclotomicCharacter (SeparableClosure K) p) ((absoluteGaloisGroupMap τ) g).toRingEquiv = (cyclotomicCharacter (SeparableClosure L) p) g.toRingEquiv

The cyclotomic character along a map of absolute Galois groups. For a K-embedding τ : Kˢ →ₐ[K] Lˢ of separable closures, the cyclotomic character of g ∈ Gal(Lˢ/L) is that of its image absoluteGaloisGroupMap τ g in Gal(Kˢ/K).

The cyclotomic orientation

theorem TauCeti.cyclotomicOrientation_maximalProPQuotient_map (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} {L : Type u_2} [Field K] [Field L] (hmuK : ∃ (ζ : K), IsPrimitiveRoot ζ p) (hmuL : ∃ (ζ : L), IsPrimitiveRoot ζ p) (f : Field.absoluteGaloisGroup L →* Field.absoluteGaloisGroup K) (hf : Continuous ⇑f) (hχ : ∀ (g : Field.absoluteGaloisGroup L), (localCyclotomicCharacter p K) (f g) = (localCyclotomicCharacter p L) g) (x : absoluteGaloisGroupProP p L) : (cyclotomicOrientation p K hmuK) ((maximalProPQuotient.map f hf) x) = (cyclotomicOrientation p L hmuL) x

Naturality of the cyclotomic orientation. If a continuous homomorphism f : G_L → G_K intertwines the cyclotomic characters, then the cyclotomic orientation of G_K(p) pulls back along the induced map G_L(p) → G_K(p) to the cyclotomic orientation of G_L(p).

@[simp]

theorem TauCeti.cyclotomicOrientation_maximalProPQuotient_congr (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) (x : absoluteGaloisGroupProP p L) : (cyclotomicOrientation p K hmu) ((maximalProPQuotient.congr (absoluteGaloisGroupMapEquiv e)) x) = (cyclotomicOrientation p L ⋯) x

The cyclotomic orientation is preserved by an isomorphism of fields e : K ≃+* L: the induced isomorphism G_L(p) ≃ₜ* G_K(p) carries the cyclotomic orientation of G_L(p) to that of G_K(p).

@[simp]

theorem TauCeti.cyclotomicOrientation_maximalProPQuotient_congr_symm (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (hmu : ∃ (ζ : L), IsPrimitiveRoot ζ p) (x : absoluteGaloisGroupProP p K) : (cyclotomicOrientation p L hmu) ((maximalProPQuotient.congr (absoluteGaloisGroupMapEquiv e)).symm x) = (cyclotomicOrientation p K ⋯) x

The cyclotomic orientation is preserved by an isomorphism of fields, read through the inverse of the induced isomorphism G_L(p) ≃ₜ* G_K(p). This is the form in which the values of the orientation on the generators of a marked presentation of G_K(p) transport to G_L(p).

@[simp]

theorem TauCeti.cyclotomicOrientation_maximalProPQuotient_map_mapOfAlgebra (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra (AlgebraicClosure K) (AlgebraicClosure L)] [IsScalarTower K (AlgebraicClosure K) (AlgebraicClosure L)] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) (x : absoluteGaloisGroupProP p L) : (cyclotomicOrientation p K hmu) ((maximalProPQuotient.map ↑(Field.absoluteGaloisGroup.mapOfAlgebra K L) ⋯) x) = (cyclotomicOrientation p L ⋯) x

The cyclotomic orientation along a field extension: it pulls back along the map G_L(p) → G_K(p) induced by Field.absoluteGaloisGroup.mapOfAlgebra K L.

@[simp]

theorem TauCeti.cyclotomicOrientation_maximalProPQuotient_map_absoluteGaloisGroupExtend (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) (x : absoluteGaloisGroupProP p L) : (cyclotomicOrientation p K hmu) ((maximalProPQuotient.map (absoluteGaloisGroupExtend K L σ) ⋯) x) = (cyclotomicOrientation p L ⋯) x

The cyclotomic orientation along a finite extension: for L/K finite embedded in Kˢ by σ, it pulls back along the map G_L(p) → G_K(p) induced by the embedding absoluteGaloisGroupExtend K L σ of G_L into G_K.