Nyll.GaloisCohomology.Kummer.Concrete.InvariantKummerPowerWitness

Module documentation

Actual power witnesses from invariant Kummer characters

Kummer naturality and invariance identify the transformed unit class with the power prescribed by the action on roots. Injectivity of the Kummer equivalence gives a witness in the original field unit group. This direction does not require the power exponent to be coprime to the coefficient modulus.

theorem

exists_power_witness_of_invariant_absoluteKummerCharacter

L29 ↗

ClassFieldTower.Martinet.Shafarevich.exists_power_witness_of_invariant_absoluteKummerCharacter

Documentation

An invariant Kummer character and the actual power action on roots produce a power witness in the base field. No coprimality is needed.

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 exists_power_witness_of_invariant_absoluteKummerCharacter
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (u : Kˣ) (a : ℕ)
    (hτ : ∀ ζ : K, ζ ^ (n : ℕ) = 1 → τ ζ = ζ ^ a)
    (hinv : ∀ σ : 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) σ) :
    ∃ y : Kˣ, Units.map τ.toMonoidHom u / u ^ a = y ^ (n : ℕ)

Module documentation

Actual power witnesses from invariant Kummer characters

Declarations

exists_power_witness_of_invariant_absoluteKummerCharacter