Module

HenselianPrimePowerRoots.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianPrimePowerRoots

3 declarations indexed from sourceView source ↗

Module documentation

Lifting and finiteness of primary roots

Hensel lifting supplies primitive roots, while injectivity of torsion reduction transfers finiteness of each primary component in residue characteristic zero.

Imports2

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianTorsionRoots
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by2

theorem

primitiveRoots_prime_nonempty_of_residue

L25 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.primitiveRoots_prime_nonempty_of_residue

Documentation

A primitive root of prime order in the residue field lifts to the field.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
universe u v
variable {K : Type u} [Field K] (F : HenselianDVF.{u, v} K)

Lean source · statement

theorem primitiveRoots_prime_nonempty_of_residue
    [CharZero F.residueField] {p : ℕ} (hp : p.Prime)
    (hres : (primitiveRoots p F.residueField).Nonempty) :
    (primitiveRoots p K).Nonempty

theorem

finite_primaryComponent_of_finite_residuePrimaryComponent

L53 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.finite_primaryComponent_of_finite_residuePrimaryComponent

Documentation

In residue characteristic zero, finiteness of the residual primary roots implies finiteness of the primary roots in the Henselian field.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
universe u v
variable {K : Type u} [Field K] (F : HenselianDVF.{u, v} K)

Lean source · statement

theorem finite_primaryComponent_of_finite_residuePrimaryComponent
    [CharZero F.residueField] {p : ℕ} (hp : p.Prime)
    [Finite (CommGroup.primaryComponent F.residueFieldˣ p)] :
    Finite (CommGroup.primaryComponent Kˣ p)

theorem

finite_primePowerRoots_of_finite_residuePrimaryComponent

L82 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.finite_primePowerRoots_of_finite_residuePrimaryComponent

Documentation

The corresponding set of field roots is finite.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
universe u v
variable {K : Type u} [Field K] (F : HenselianDVF.{u, v} K)

Lean source · statement

theorem finite_primePowerRoots_of_finite_residuePrimaryComponent
    [CharZero F.residueField] {p : ℕ} (hp : p.Prime)
    [Finite (CommGroup.primaryComponent F.residueFieldˣ p)] :
    Set.Finite {z : K | ∃ n : ℕ, z ^ (p ^ n) = 1}

Module documentation

Lifting and finiteness of primary roots

Declarations

primitiveRoots_prime_nonempty_of_residue

finite_primaryComponent_of_finite_residuePrimaryComponent

finite_primePowerRoots_of_finite_residuePrimaryComponent