Module

HenselianRootsOfUnity.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianRootsOfUnity

12 declarations indexed from sourceView source ↗

Module documentation

Reduction of roots of unity over a Henselian DVF

If the root order is nonzero in the residue field, Hensel lifting and uniqueness make reduction bijective on roots of unity. No completeness or finiteness assumption on the residue field is needed.

Imports3

Nyll.ValuedFieldTheory.Valuation.HenselLemma
Mathlib.RingTheory.RootsOfUnity.Basic
Mathlib.Algebra.Order.GroupWithZero.Basic

Imported by3

def

rootsOfUnityReduction

L26 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnityReduction

Documentation

Reduction on the actual group of roots of unity in the valuation ring.

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

def rootsOfUnityReduction (n : ℕ) :
    rootsOfUnity n F.valuationSubring →* rootsOfUnity n F.residueField

theorem

rootsOfUnityReduction_apply

L30 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnityReduction_apply

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 rootsOfUnityReduction_apply (n : ℕ)
    (ζ : rootsOfUnity n F.valuationSubring) :
    ((rootsOfUnityReduction F n ζ : F.residueFieldˣ) : F.residueField) =
      F.residueMap ((ζ : F.valuationSubringˣ) : F.valuationSubring)

theorem

rootPolynomial_derivative_isUnit

L35 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootPolynomial_derivative_isUnit

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 rootPolynomial_derivative_isUnit
    (n : ℕ) [NeZero (n : F.residueField)] (a : F.valuationSubringˣ) :
    IsUnit (((Polynomial.X ^ n - 1 : Polynomial F.valuationSubring).derivative).eval
      (a : F.valuationSubring))

theorem

rootsOfUnityReduction_injective

L47 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnityReduction_injective

Documentation

Reduction is injective when the root order is nonzero in the residue 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 rootsOfUnityReduction_injective (n : ℕ) [NeZero (n : F.residueField)] :
    Function.Injective (rootsOfUnityReduction F n)

theorem

rootsOfUnityReduction_surjective

L61 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnityReduction_surjective

Documentation

Each residual root of unity lifts to an actual root in the valuation ring.

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 rootsOfUnityReduction_surjective (n : ℕ) [NeZero (n : F.residueField)] :
    Function.Surjective (rootsOfUnityReduction F n)

theorem

rootsOfUnityReduction_bijective

L91 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnityReduction_bijective

Documentation

Reduction is a bijection on roots whose order is invertible in the residue 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 rootsOfUnityReduction_bijective (n : ℕ) [NeZero (n : F.residueField)] :
    Function.Bijective (rootsOfUnityReduction F n)

def

rootsOfUnityReductionEquiv

L96 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnityReductionEquiv

Documentation

The multiplicative equivalence obtained from actual root reduction.

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

def rootsOfUnityReductionEquiv (n : ℕ) [NeZero (n : F.residueField)] :
    rootsOfUnity n F.valuationSubring ≃* rootsOfUnity n F.residueField

theorem

rootsOfUnityReductionEquiv_apply

L100 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnityReductionEquiv_apply

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 rootsOfUnityReductionEquiv_apply (n : ℕ) [NeZero (n : F.residueField)]
    (ζ : rootsOfUnity n F.valuationSubring) :
    rootsOfUnityReductionEquiv F n ζ = rootsOfUnityReduction F n ζ

theorem

rootsOfUnity_toField_bijective

L104 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnity_toField_bijective

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 rootsOfUnity_toField_bijective (D : DVF.{u, v} K)
    (n : ℕ) [NeZero n] :
    Function.Bijective (restrictRootsOfUnity (algebraMap D.valuationSubring K) n)

def

rootsOfUnityFieldEquiv

L127 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.rootsOfUnityFieldEquiv

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

def rootsOfUnityFieldEquiv (D : DVF.{u, v} K)
    (n : ℕ) [NeZero n] : rootsOfUnity n D.valuationSubring ≃* rootsOfUnity n K

def

fieldRootsOfUnityReductionEquiv

L134 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.fieldRootsOfUnityReductionEquiv

Documentation

Reduction identifies the actual field roots with the residue-field roots. Every field root is first regarded as a valuation-ring unit.

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

def fieldRootsOfUnityReductionEquiv
    (n : ℕ) [NeZero (n : F.residueField)] :
    rootsOfUnity n K ≃* rootsOfUnity n F.residueField

theorem

fieldRootsOfUnityReductionEquiv_toField

L141 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.fieldRootsOfUnityReductionEquiv_toField

Documentation

The field-root equivalence is the actual residue map on integral roots.

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 fieldRootsOfUnityReductionEquiv_toField
    (n : ℕ) [NeZero (n : F.residueField)] (ζ : rootsOfUnity n F.valuationSubring) :
    fieldRootsOfUnityReductionEquiv F n
        (restrictRootsOfUnity (algebraMap F.valuationSubring K) n ζ) =
      rootsOfUnityReduction F n ζ

Module documentation

Reduction of roots of unity over a Henselian DVF

Declarations