NYLL
Module

RootKummerInvariantCharacter.lean

Nyll.GaloisCohomology.Kummer.Concrete.RootKummerInvariantCharacter
2 declarations indexed from sourceView source ↗

Module documentation

Roots give invariant Kummer characters

An automorphism has the same actual power action on a root and on the Kummer coefficient roots. Their cyclotomic actions cancel. The resulting constant-coefficient Kummer character is fixed by the true left action.

Imports7
Imported by2

Declarations

theorem

absoluteKummerContinuousNthRootsCharacterEquiv_conjugation_invariant_of_root

L31 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousNthRootsCharacterEquiv_conjugation_invariant_of_root
Documentation

A unit which is an n-th root of unity has an invariant Kummer character under every field automorphism.

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_root
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : Kˣ) (hu : (u : K) ^ (n : ℕ) = 1) (τ : K ≃+* K)
    (σ : 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) σ
theorem

absoluteContinuousCharacterAction_kummer_root

L51 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteContinuousCharacterAction_kummer_root
Documentation

The root's constant-coefficient Kummer character is fixed by the inverse-conjugation left action, with the original Kummer coordinate.

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 absoluteContinuousCharacterAction_kummer_root
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : Kˣ) (hu : (u : K) ^ (n : ℕ) = 1) (τ : K ≃+* K) :
    absoluteContinuousCharacterAction (K := K) (A := Multiplicative (ZMod (n : ℕ))) τ
        (absoluteKummerContinuousZModCharacterEquiv K n hmu
          (u : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)) =
      absoluteKummerContinuousZModCharacterEquiv K n hmu
        (u : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.