Module

PrincipalUnitRoots.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.PrincipalUnitRoots

3 declarations indexed from sourceView source ↗

Module documentation

Roots of principal units sufficiently close to one

In a Henselian valued field, every element closer to one than the square of the value of a nonzero integer n is an nth power. Rescaling the binomial polynomial gives a simple residual root, even when n is not a residue unit.

Imports8

Nyll.ValuedFieldTheory.Valuation.Henselian.NonmonicSimpleRoot
Mathlib.Algebra.Polynomial.Div
Mathlib.Algebra.Polynomial.Coeff
Mathlib.Topology.Algebra.Valued.ValuationTopology
Mathlib.Topology.Algebra.Group.Units
Mathlib.Topology.Algebra.OpenSubgroup
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.FieldSimp

Imported by2

theorem

exists_binomial_quadratic_remainder

L28 ↗

ValuationTheory.exists_binomial_quadratic_remainder

Source context 2 commands

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

namespace ValuationTheory
open Polynomial

Lean source · statement

theorem exists_binomial_quadratic_remainder
    {R : Type*} [CommRing R] (n : ℕ) :
    ∃ Q : R[X], ∀ t : R, (1 + t) ^ n = 1 + (n : R) * t + t ^ 2 * Q.eval t

theorem

exists_pow_eq_of_valuation_sub_one_lt_natCast_sq

L49 ↗

ValuationTheory.exists_pow_eq_of_valuation_sub_one_lt_natCast_sq

Documentation

The Hensel bound for nth roots near one, including the case when the integer n is divisible by the residue characteristic.

Source context 2 commands

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

namespace ValuationTheory
open Polynomial

Lean source · statement

theorem exists_pow_eq_of_valuation_sub_one_lt_natCast_sq
    {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ)
    [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
    (n : ℕ) (hn : (n : K) ≠ 0) (a : K)
    (ha : v (a - 1) < v (n : K) ^ 2) :
    ∃ b : K, b ^ n = a

theorem

isOpen_unit_pow_range

L97 ↗

ValuationTheory.isOpen_unit_pow_range

Documentation

In a Henselian valued field, the nth-power subgroup of the multiplicative group is open whenever n is nonzero in the field.

Source context 2 commands

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

namespace ValuationTheory
open Polynomial

Lean source · statement

theorem isOpen_unit_pow_range
    {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ] [Valued K Γ]
    [HenselianRing (Valued.v : Valuation K Γ).valuationSubring
      (IsLocalRing.maximalIdeal (Valued.v : Valuation K Γ).valuationSubring)]
    (n : ℕ) (hn : (n : K) ≠ 0) :
    IsOpen ((powMonoidHom n : Kˣ →* Kˣ).range : Set Kˣ)

Module documentation

Roots of principal units sufficiently close to one

Declarations

exists_binomial_quadratic_remainder

exists_pow_eq_of_valuation_sub_one_lt_natCast_sq

isOpen_unit_pow_range