ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousNthRootsCharacterEquiv_apply_of_pow_eq
The absolute Kummer character of a unit class is computed from any n-th root of that unit in the algebraic closure.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K] [CharZero K]Lean source · statement
theorem absoluteKummerContinuousNthRootsCharacterEquiv_apply_of_pow_eq
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
(a : Kˣ) (β : (AlgebraicClosure K)ˣ)
(hβ : β ^ (n : ℕ) =
Units.map (algebraMap K (AlgebraicClosure K)).toMonoidHom a)
(σ : Field.absoluteGaloisGroup K) :
((absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
(a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) σ :
DiscreteNthRootsSubgroup (AlgebraicClosure K) (n : ℕ)) :
(AlgebraicClosure K)ˣ) =
rootQuotient (K := K) (L := AlgebraicClosure K) β σ