Module

AbsoluteKummerNaturality.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteKummerNaturality

3 declarations indexed from sourceView source ↗

Module documentation

Naturality of absolute Kummer characters

The Kummer character of a transformed unit, evaluated at the conjugated Galois automorphism, is the transformed original character value. When the base automorphism fixes the roots of unity, the coefficient value is unchanged.

Imports3

Imported by5

theorem

absoluteKummerContinuousNthRootsCharacterEquiv_naturality

L29 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousNthRootsCharacterEquiv_naturality

Documentation

Absolute Kummer characters commute pointwise with the chosen extension of a base-field automorphism and its conjugation on the Galois group.

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_naturality
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (a : Kˣ) (σ : Gal(AlgebraicClosure K/K)) :
    ((absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
        ((Units.map τ.toMonoidHom a : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
        (absoluteGaloisConjugate τ σ) :
      DiscreteNthRootsSubgroup (AlgebraicClosure K) (n : ℕ)) :
        (AlgebraicClosure K)ˣ) =
      Units.map (IsAlgClosure.equivOfEquiv (AlgebraicClosure K)
        (AlgebraicClosure K) τ).toMonoidHom
        ((absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
            (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) σ :
          DiscreteNthRootsSubgroup (AlgebraicClosure K) (n : ℕ)) :
            (AlgebraicClosure K)ˣ)

theorem

absoluteKummerContinuousNthRootsCharacterEquiv_naturality_of_fixes_roots

L70 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousNthRootsCharacterEquiv_naturality_of_fixes_roots

Documentation

When the base-field automorphism fixes the n-th roots of unity, Kummer naturality has constant coefficients.

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_naturality_of_fixes_roots
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K)
    (hτ : ∀ ζ : K, ζ ^ (n : ℕ) = 1 → τ ζ = ζ)
    (a : Kˣ) (σ : Gal(AlgebraicClosure K/K)) :
    absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
        ((Units.map τ.toMonoidHom a : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
        (absoluteGaloisConjugate τ σ) =
      absoluteKummerContinuousNthRootsCharacterEquiv K n hmu
        (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) σ

theorem

exists_moved_absoluteKummerCharacter_of_finite_primePowerRoots

L107 ↗

ClassFieldTower.Martinet.Shafarevich.exists_moved_absoluteKummerCharacter_of_finite_primePowerRoots

Documentation

An eigenunit with primitive prime-order multiplier yields a continuous character moved by conjugation when the prime-power roots form a finite set fixed by the base automorphism. The detecting exponent and character are constructed from the last available root level.

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 exists_moved_absoluteKummerCharacter_of_finite_primePowerRoots
    {p : ℕ} (hp : p.Prime)
    (hfinite : Set.Finite {ξ : K | ∃ m : ℕ, ξ ^ (p ^ m) = 1})
    (ζ : Kˣ) (hζ : IsPrimitiveRoot ζ p)
    (τ : K ≃+* K)
    (hτ : ∀ ξ : K, (∃ m : ℕ, ξ ^ (p ^ m) = 1) → τ ξ = ξ)
    (α : Kˣ) (hα : Units.map τ.toMonoidHom α = ζ * α) :
    ∃ s : ℕ, 1 ≤ s ∧ (primitiveRoots (p ^ s) K).Nonempty ∧
      (∀ m : ℕ, (primitiveRoots (p ^ m) K).Nonempty → m ≤ s) ∧
      ∃ χ : Field.absoluteGaloisGroup K →ₜ*
          DiscreteNthRootsSubgroup (AlgebraicClosure K) (p ^ s),
        ∃ σ : Gal(AlgebraicClosure K/K),
          χ (absoluteGaloisConjugate τ σ) ≠ χ σ

Module documentation

Naturality of absolute Kummer characters

Declarations

absoluteKummerContinuousNthRootsCharacterEquiv_naturality

absoluteKummerContinuousNthRootsCharacterEquiv_naturality_of_fixes_roots

exists_moved_absoluteKummerCharacter_of_finite_primePowerRoots