ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousNthRootsCharacterEquiv_conjugation_invariant_of_power_action
A power eigenclass whose exponent matches the actual cyclotomic action gives a Kummer character fixed by Galois conjugation.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [CharZero K]Lean source · statement
theorem absoluteKummerContinuousNthRootsCharacterEquiv_conjugation_invariant_of_power_action
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
(τ : K ≃+* K) (u : Kˣ) (a : ℕ) (ha : a.Coprime (n : ℕ))
(hu : ((Units.map τ.toMonoidHom u : Kˣ) :
Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) =
(u : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) ^ a)
(hτ : ∀ ζ : K, ζ ^ (n : ℕ) = 1 → τ ζ = ζ ^ a)
(σ : Gal(AlgebraicClosure K/K)) :
absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
(u : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
(absoluteGaloisConjugate τ σ) =
absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
(u : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) σ