Module

ResidueRoots.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.ResidueRoots

11 declarations indexed from sourceView source ↗

Module documentation

Residue roots of unity

Hensel lifting identifies the finite residue-field unit group with the lifted roots of unity in the valuation ring.

Imports5

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.Filtration
Nyll.ValuedFieldTheory.Valuation.HenselLemma
Mathlib.SetTheory.Cardinal.Finite
Mathlib.FieldTheory.Finite.Basic
Mathlib.RingTheory.RootsOfUnity.Basic

Imported by4

abbrev

residueRootsOfUnityGroup

L44 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup

Documentation

The (q - 1)-st roots of unity in the valuation ring, where q = #κ.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

abbrev residueRootsOfUnityGroup [Finite F.residueField] :
    Subgroup F.valuationSubringˣ

theorem

residueRootPolynomial_derivative_eval_ne_zero

L50 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootPolynomial_derivative_eval_ne_zero

Documentation

Every nonzero residue class is a simple root of X^(#κ - 1) - 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem residueRootPolynomial_derivative_eval_ne_zero
    [Finite F.residueField] (y : F.residueFieldˣ) :
    (((Polynomial.X ^ (Nat.card F.residueField - 1) - 1 :
        Polynomial F.residueField).derivative).eval
          (y : F.residueField)) ≠ 0

theorem

exists_residueRootsOfUnity_lift

L82 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_residueRootsOfUnity_lift

Documentation

Hensel lift of finite-residue-field roots of unity: every residue-field unit has a valuation-ring unit representative satisfying u^(q - 1) = 1.

This is the substantive splitting input for the multiplicative unit decomposition: it upgrades the quotient isomorphism O^*/U^1 ≃ κ^* from an abstract first-isomorphism statement to a root-of-unity representative in O^*.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem exists_residueRootsOfUnity_lift
    [Finite F.residueField] (y : F.residueFieldˣ) :
    ∃ u : F.valuationSubringˣ,
      u ∈ higherPrincipalUnitGroup.residueRootsOfUnityGroup F ∧
        higherPrincipalUnitGroup.residueUnitHom F u = y

def

residueRootsOfUnityResidueHom

L143 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityResidueHom

Documentation

The residue map restricted to the Hensel-lifted (q - 1)-roots of unity.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def residueRootsOfUnityResidueHom [Finite F.residueField] :
    higherPrincipalUnitGroup.residueRootsOfUnityGroup F →* F.residueFieldˣ

theorem

residueRootsOfUnityResidueHom_surjective

L152 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityResidueHom_surjective

Documentation

The specified map is surjective: Function.Surjective (higherPrincipalUnitGroup.residueRootsOfUnityResidueHom F).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem residueRootsOfUnityResidueHom_surjective
    [Finite F.residueField] :
    Function.Surjective
      (higherPrincipalUnitGroup.residueRootsOfUnityResidueHom F)

theorem

residueRootPolynomial_isRoot_of_mem

L164 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootPolynomial_isRoot_of_mem

Documentation

A unit satisfying the Teichmuller equation is a root of X^(q - 1) - 1 over the valuation ring.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem residueRootPolynomial_isRoot_of_mem
    [Finite F.residueField] {u : F.valuationSubringˣ}
    (hu : u ∈ higherPrincipalUnitGroup.residueRootsOfUnityGroup F) :
    (Polynomial.X ^ (Nat.card F.residueField - 1) - 1 :
        Polynomial F.valuationSubring).IsRoot
      (u : F.valuationSubring)

theorem

residueRootPolynomial_derivative_eval_isUnit

L181 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootPolynomial_derivative_eval_isUnit

Documentation

The derivative of X^(q - 1) - 1 at a valuation-ring unit is a unit. This is the simple-root input for uniqueness of Teichmuller representatives.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem residueRootPolynomial_derivative_eval_isUnit
    [Finite F.residueField] (u : F.valuationSubringˣ) :
    IsUnit
      (((Polynomial.X ^ (Nat.card F.residueField - 1) - 1 :
          Polynomial F.valuationSubring).derivative).eval
        (u : F.valuationSubring))

theorem

residueRootsOfUnityResidueHom_injective

L219 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityResidueHom_injective

Documentation

The specified map is injective: Function.Injective (higherPrincipalUnitGroup.residueRootsOfUnityResidueHom F).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem residueRootsOfUnityResidueHom_injective
    [Finite F.residueField] :
    Function.Injective
      (higherPrincipalUnitGroup.residueRootsOfUnityResidueHom F)

theorem

residueRootsOfUnityResidueHom_bijective

L266 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityResidueHom_bijective

Documentation

The specified map is bijective: Function.Bijective (higherPrincipalUnitGroup.residueRootsOfUnityResidueHom F).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem residueRootsOfUnityResidueHom_bijective
    [Finite F.residueField] :
    Function.Bijective
      (higherPrincipalUnitGroup.residueRootsOfUnityResidueHom F)

def

residueRootsOfUnityEquivResidueFieldUnits

L275 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityEquivResidueFieldUnits

Documentation

Hensel's splitting of the residue-unit map on the (q - 1)-roots of unity: the Teichmuller representatives in O^* are exactly κ^*.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def residueRootsOfUnityEquivResidueFieldUnits
    [Finite F.residueField] :
    higherPrincipalUnitGroup.residueRootsOfUnityGroup F ≃*
      F.residueFieldˣ

theorem

residueRootsOfUnityEquivResidueFieldUnits_apply

L288 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityEquivResidueFieldUnits_apply

Documentation

The defining evaluation formula for residueRootsOfUnityEquivResidueFieldUnits is higherPrincipalUnitGroup.residueRootsOfUnityEquivResidueFieldUnits F u = higherPrincipalUnitGroup.residueUnitHom F u.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem residueRootsOfUnityEquivResidueFieldUnits_apply
    [Finite F.residueField]
    (u : higherPrincipalUnitGroup.residueRootsOfUnityGroup F) :
    higherPrincipalUnitGroup.residueRootsOfUnityEquivResidueFieldUnits F u =
      higherPrincipalUnitGroup.residueUnitHom F u

Module documentation

Residue roots of unity

Declarations