Module

RootsDownstairs.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.RootsDownstairs

4 declarations indexed from sourceView source ↗

Module documentation

Roots downstairs detect prime-degree Galois automorphisms

For a prime-degree Galois extension with finite prime-power roots all in the base, each nonidentity automorphism moves a continuous degree-one class. The eigenunit, coefficient exponent, character, and point detecting movement are all constructed.

Imports4

Nyll.GaloisCohomology.Kummer.Concrete.PrimeCyclicEigenunit
Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteKummerNaturality
Nyll.ProCGroups.ProP.ContinuousH1
Mathlib.Algebra.CharP.Algebra

Imported by3

instance

discreteZModTopology

L28 ↗

ClassFieldTower.Martinet.Shafarevich.discreteZModTopology

Source context 4 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

instance discreteZModTopology (n : ℕ) : TopologicalSpace (ZMod n)

instance

discreteZMod

L29 ↗

ClassFieldTower.Martinet.Shafarevich.discreteZMod

Source context 5 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
local instance discreteZModTopology (n : ℕ) : TopologicalSpace (ZMod n) := ⊥

Lean source · statement

instance discreteZMod (n : ℕ) : DiscreteTopology (ZMod n)

theorem

rootsDownstairs_exists_moved_h1

L33 ↗

ClassFieldTower.Martinet.Shafarevich.rootsDownstairs_exists_moved_h1

Documentation

With all prime-power roots downstairs, each nonidentity automorphism of a prime-degree Galois extension moves a continuous ZMod (p^s) degree-one class.

Source context 6 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
local instance discreteZModTopology (n : ℕ) : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod (n : ℕ) : DiscreteTopology (ZMod n) := discreteTopology_bot _

Lean source · statement

theorem rootsDownstairs_exists_moved_h1
    [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) ∧
      ∃ c : ClassFieldTower.ProP.ContinuousH1ZMod
          (p := p ^ s) (G := Field.absoluteGaloisGroup L),
        ∃ σ : Gal(AlgebraicClosure L/L),
          c (Additive.ofMul
              (absoluteGaloisConjugate τ.toRingEquiv σ : Field.absoluteGaloisGroup L)) ≠
            c (Additive.ofMul (σ : Field.absoluteGaloisGroup L))

theorem

rootsDownstairs_nontrivial_h1

L70 ↗

ClassFieldTower.Martinet.Shafarevich.rootsDownstairs_nontrivial_h1

Documentation

The roots-downstairs detection statement for an arbitrary prime-degree Galois extension, with the last coefficient level and a moved degree-one class.

Source context 6 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
local instance discreteZModTopology (n : ℕ) : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod (n : ℕ) : DiscreteTopology (ZMod n) := discreteTopology_bot _

Lean source · statement

theorem rootsDownstairs_nontrivial_h1
    [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) ∧
      ∃ τ : Gal(L/K), τ ≠ 1 ∧
        ∃ c : ClassFieldTower.ProP.ContinuousH1ZMod
            (p := p ^ s) (G := Field.absoluteGaloisGroup L),
          ∃ σ : Gal(AlgebraicClosure L/L),
            c (Additive.ofMul
                (absoluteGaloisConjugate τ.toRingEquiv σ : Field.absoluteGaloisGroup L)) ≠
              c (Additive.ofMul (σ : Field.absoluteGaloisGroup L))

Module documentation

Roots downstairs detect prime-degree Galois automorphisms

Declarations

discreteZModTopology

discreteZMod

rootsDownstairs_exists_moved_h1

rootsDownstairs_nontrivial_h1