Module

RootsDownstairsAction.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.RootsDownstairsAction

3 declarations indexed from sourceView source ↗

Module documentation

Roots downstairs and the canonical actions

The moved classes constructed from eigenunits detect the genuine relative Galois action on H¹ and the canonical action on topological abelianization.

Imports4

Imported by2

theorem

rootsDownstairs_h1_action_ne_one

L29 ↗

ClassFieldTower.Martinet.Shafarevich.rootsDownstairs_h1_action_ne_one

Documentation

Every nonidentity relative automorphism acts nontrivially on continuous H¹ at the last prime-power root level.

Source context 4 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
attribute [local instance] discreteZModTopology discreteZMod

Lean source · statement

theorem rootsDownstairs_h1_action_ne_one
    [CharZero K] [FiniteDimensional K L] [IsGalois K L]
    {p : ℕ} (hp : p.Prime) (hdeg : Module.finrank K L = p)
    (hμ : (primitiveRoots p K).Nonempty)
    (hfinite : Set.Finite {ξ : L | ∃ m : ℕ, ξ ^ (p ^ m) = 1})
    (hdown : ∀ ξ : L, (∃ m : ℕ, ξ ^ (p ^ m) = 1) →
      ξ ∈ Set.range (algebraMap K L))
    (τ : Gal(L/K)) (hτ : τ ≠ 1) :
    ∃ s : ℕ, 1 ≤ s ∧ (primitiveRoots (p ^ s) L).Nonempty ∧
      (∀ m : ℕ, (primitiveRoots (p ^ m) L).Nonempty → m ≤ s) ∧
      relativeGaloisH1Action (n := p ^ s) K L τ ≠ 1

theorem

rootsDownstairs_faithful_h1_action

L53 ↗

ClassFieldTower.Martinet.Shafarevich.rootsDownstairs_faithful_h1_action

Documentation

The last prime-power root level gives a faithful relative Galois action on continuous degree-one classes. Maximality makes this level uniform in τ.

Source context 4 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
attribute [local instance] discreteZModTopology discreteZMod

Lean source · statement

theorem rootsDownstairs_faithful_h1_action
    [CharZero K] [FiniteDimensional K L] [IsGalois K L]
    {p : ℕ} (hp : p.Prime) (hdeg : Module.finrank K L = p)
    (hμ : (primitiveRoots p K).Nonempty)
    (hfinite : Set.Finite {ξ : L | ∃ m : ℕ, ξ ^ (p ^ m) = 1})
    (hdown : ∀ ξ : L, (∃ m : ℕ, ξ ^ (p ^ m) = 1) →
      ξ ∈ Set.range (algebraMap K L)) :
    ∃ s : ℕ, 1 ≤ s ∧ (primitiveRoots (p ^ s) L).Nonempty ∧
      (∀ m : ℕ, (primitiveRoots (p ^ m) L).Nonempty → m ≤ s) ∧
      Function.Injective (relativeGaloisH1Action (n := p ^ s) K L)

theorem

rootsDownstairs_abelianization_action_ne_one

L77 ↗

ClassFieldTower.Martinet.Shafarevich.rootsDownstairs_abelianization_action_ne_one

Documentation

Roots downstairs detect the canonical automorphism of the abelianized absolute Galois group, with no chosen-lift assumption.

Source context 4 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
attribute [local instance] discreteZModTopology discreteZMod

Lean source · statement

theorem rootsDownstairs_abelianization_action_ne_one
    [CharZero K] [FiniteDimensional K L] [IsGalois K L]
    {p : ℕ} (hp : p.Prime) (hdeg : Module.finrank K L = p)
    (hμ : (primitiveRoots p K).Nonempty)
    (hfinite : Set.Finite {ξ : L | ∃ m : ℕ, ξ ^ (p ^ m) = 1})
    (hdown : ∀ ξ : L, (∃ m : ℕ, ξ ^ (p ^ m) = 1) →
      ξ ∈ Set.range (algebraMap K L))
    (τ : Gal(L/K)) (hτ : τ ≠ 1) :
    absoluteGaloisAbelianizationAction τ.toRingEquiv ≠ 1

Module documentation

Roots downstairs and the canonical actions

Declarations

rootsDownstairs_h1_action_ne_one

rootsDownstairs_faithful_h1_action

rootsDownstairs_abelianization_action_ne_one