Nyll.Yamaguchi26AbfaithfulGalois.Kummer.TrivialAction

Module documentation

Kummer criterion for a trivial mod-n action

Equation eq:kummer-trivial in Section 3. The left side says that conjugation is trivial on G_Kᵃᵇ/n, using its exact character-dual description: every continuous ZMod n-valued character is fixed. The right side says τ(x)/x^a is an n-th power for every unit x.

theorem

kummer_trivial_action_criterion

L32 ↗

Yamaguchi26AbfaithfulGalois.kummer_trivial_action_criterion

Documentation

If τ acts by the a-th power on μ_n, its action on the mod-n abelianization is trivial exactly when τ(x)/x^a is an n-th power for every nonzero x.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open KummerTheory
universe u

Lean source · statement

theorem kummer_trivial_action_criterion
    (K : Type u) [Field K]
    (n : ℕ+) [NeZero ((n : ℕ) : K)]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (a : ℕ)
    (hpower : ∀ ξ : K, ξ ^ (n : ℕ) = 1 → τ ξ = ξ ^ a) :
    (∀ (χ : Gal(AlgebraicClosure K/K) →ₜ*
          Multiplicative (ZMod (n : ℕ)))
        (σ : Gal(AlgebraicClosure K/K)),
        χ (absoluteGaloisConjugate τ σ) = χ σ) ↔
      ∀ x : Kˣ,
        ((Units.map τ.toMonoidHom x : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) =
          (x : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) ^ a

Module documentation

Kummer criterion for a trivial mod-n action

Declarations

kummer_trivial_action_criterion