NYLL
Module

DiscreteAbsoluteCenter.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DiscreteAbsoluteCenter
1 declaration indexed from sourceView source ↗

Module documentation

Absolute Galois centers over Henselian discrete valuations

For a Henselian discrete valuation field of residue characteristic zero containing all p-power roots, a Kummer extension supplies nontrivial inertia and hence a nonidentity element of the absolute Galois center.

Imports4
Imported by2

Declarations

theorem

exists_ne_one_mem_absoluteGalois_center_of_all_primePowerRoots

L30 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_ne_one_mem_absoluteGalois_center_of_all_primePowerRoots
Documentation

Over a residue-zero Henselian DVF containing all p-power roots, a cyclic Kummer extension supplies finite nontrivial inertia; compactness then gives a nonidentity element of the actual absolute Galois center.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.ValuationSubring
universe u v
Lean source · statement
theorem HenselianDVF.exists_ne_one_mem_absoluteGalois_center_of_all_primePowerRoots
    {K : Type u} [Field K] (D : HenselianDVF.{u, v} K)
    [CharZero D.residueField]
    (p : ℕ) [Fact p.Prime]
    (hroots : ∀ n : ℕ, ∃ ζ : K, IsPrimitiveRoot ζ (p ^ n)) :
    ∃ σ : Gal(AlgebraicClosure K/K),
      σ ∈ Subgroup.center Gal(AlgebraicClosure K/K) ∧ σ ≠ 1

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