Nyll.ValuedFieldTheory.Valuation.Henselian.FiniteResidueRootLifting

Module documentation

Lifting residue roots of unity in one finite field extension

Over a Henselian valued field of residue characteristic zero, a fixed finite residue extension determines one finite intermediate field in which its primitive roots of unity lift for every positive order. The field is constructed from the residue Galois stabilizer.

theorem

exists_finiteIntermediateField_lifting_residue_roots

L34 ↗

ValuationTheory.Henselian.exists_finiteIntermediateField_lifting_residue_roots

Documentation

Every root of unity in a fixed finite residue extension lifts into one finite field extension. The field is the fixed field of the inverse image of its residue Galois stabilizer; it works simultaneously for all positive orders.

Source context 4 commands

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

namespace ValuationTheory.Henselian
open IsLocalRing
open RamificationTheory.HilbertRamification.ValuationSubring
universe u v t w x

Lean source · statement

theorem exists_finiteIntermediateField_lifting_residue_roots
    {K : Type u} {Ω : Type v} [Field K] [Field Ω]
    [Algebra K Ω] [IsAlgClosure K Ω]
    {Γ : Type w} {Δ : Type x}
    [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
    (v : Valuation K Γ) (w : Valuation Ω Δ) [v.HasExtension w]
    [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
    [CharZero (ResidueField v.valuationSubring)]
    (E : Type t) [Field E] [Algebra (ResidueField v.valuationSubring) E]
    [FiniteDimensional (ResidueField v.valuationSubring) E] :
    ∃ F : IntermediateField K Ω, FiniteDimensional K F ∧
      ∀ (n : ℕ), 0 < n → (∃ ζ : E, IsPrimitiveRoot ζ n) →
        ∃ ζ : F, IsPrimitiveRoot ζ n

Module documentation

Lifting residue roots of unity in one finite field extension

Declarations

exists_finiteIntermediateField_lifting_residue_roots