NYLL
Module

DyadicNormObstruction.lean

Nyll.ValuedFieldTheory.Valuation.DyadicNormObstruction
7 declarations indexed from sourceView source ↗

Module documentation

Quadratic norm obstruction in dyadic Henselian fields

A nonsquare defines a quadratic norm form whose values do not all lie in the two square classes killed by adjoining its square root. The proof normalizes the valuation, minimizes within a unit square class, and then constructs a norm at the sharp Hensel boundary.

Imports5
Imported by2

Declarations

theorem

valuation_one_add_eq_one_of_one_sub_sq_value

L24 ↗
ValuationTheory.valuation_one_add_eq_one_of_one_sub_sq_value
Source context 1 command

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

namespace ValuationTheory
Lean source · statement
theorem valuation_one_add_eq_one_of_one_sub_sq_value
    {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) (b : K) (hb : v b ≤ 1)
    (hval : v (1 - b ^ 2) = 1) : v (1 + b) = 1
theorem

valuation_sub_one_eq_two_sq_of_minimal_squareClass

L40 ↗
ValuationTheory.valuation_sub_one_eq_two_sq_of_minimal_squareClass
Documentation

Minimality within a nonsquare unit class forces the dyadic Hensel bound to be attained if the norm of 1 + sqrt(a) lies in either allowed square class.

Source context 1 command

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

namespace ValuationTheory
Lean source · statement
theorem valuation_sub_one_eq_two_sq_of_minimal_squareClass
    {K : Type*} [Field K] [CharZero K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
    (h2 : v (2 : K) < 1) (a : K) (ha : v a = 1) (hns : ¬ IsSquare a)
    (hmin : ∀ c : Kˣ, v (c : K) = 1 →
      v (a - 1) ≤ v (a * (c : K) ^ 2 - 1))
    (hnorm : IsSquare (1 - a) ∨ IsSquare ((1 - a) / a)) :
    v (a - 1) = v (2 : K) ^ 2
theorem

exists_quadraticForm_outside_squareClasses_of_boundary

L121 ↗
ValuationTheory.exists_quadraticForm_outside_squareClasses_of_boundary
Documentation

At the dyadic Hensel boundary, a uniformizer supplies a quadratic norm outside both possible square classes.

Source context 1 command

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

namespace ValuationTheory
Lean source · statement
theorem exists_quadraticForm_outside_squareClasses_of_boundary
    {K : Type*} [Field K] [CharZero K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    (h2 : v (2 : K) < 1) (a π : K) (ha : v a = 1)
    (hπ : v π = WithZero.exp (-1 : ℤ))
    (heq : v (a - 1) = v (2 : K) ^ 2) :
    ∃ x y : K, ¬ IsSquare (x ^ 2 - a * y ^ 2) ∧
      ¬ IsSquare ((x ^ 2 - a * y ^ 2) / a)
theorem

exists_quadraticForm_outside_squareClasses_of_unit

L196 ↗
ValuationTheory.exists_quadraticForm_outside_squareClasses_of_unit
Documentation

A nonsquare unit in a Henselian dyadic field has a quadratic norm outside the two square classes that become squares in the quadratic extension.

Source context 1 command

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

namespace ValuationTheory
Lean source · statement
theorem exists_quadraticForm_outside_squareClasses_of_unit
    {K : Type*} [Field K] [CharZero K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
    (h2 : v (2 : K) < 1) (a π : K) (ha : v a = 1)
    (hπ : v π = WithZero.exp (-1 : ℤ)) (hns : ¬ IsSquare a) :
    ∃ x y : K, ¬ IsSquare (x ^ 2 - a * y ^ 2) ∧
      ¬ IsSquare ((x ^ 2 - a * y ^ 2) / a)
theorem

not_isSquare_of_valuation_eq_exp_odd

L256 ↗
ValuationTheory.not_isSquare_of_valuation_eq_exp_odd
Source context 1 command

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

namespace ValuationTheory
Lean source · statement
theorem not_isSquare_of_valuation_eq_exp_odd
    {K : Type*} [Field K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    (a : K) (n : ℤ) (hn : Odd n) (ha : v a = WithZero.exp n) :
    ¬ IsSquare a
theorem

exists_quadraticForm_outside_squareClasses_of_uniformizer_value

L273 ↗
ValuationTheory.exists_quadraticForm_outside_squareClasses_of_uniformizer_value
Documentation

The ramified normalized square class already gives the required norm at (1,1).

Source context 1 command

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

namespace ValuationTheory
Lean source · statement
theorem exists_quadraticForm_outside_squareClasses_of_uniformizer_value
    {K : Type*} [Field K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    (h2 : v (2 : K) < 1) (a : K) (ha : v a = WithZero.exp (-1 : ℤ)) :
    ∃ x y : K, ¬ IsSquare (x ^ 2 - a * y ^ 2) ∧
      ¬ IsSquare ((x ^ 2 - a * y ^ 2) / a)
theorem

exists_quadraticForm_outside_squareClasses

L297 ↗
ValuationTheory.exists_quadraticForm_outside_squareClasses
Documentation

Every nontrivial quadratic square class over a Henselian dyadic discretely valued field has a norm which stays outside the two classes killed in the extension.

Source context 1 command

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

namespace ValuationTheory
Lean source · statement
theorem exists_quadraticForm_outside_squareClasses
    {K : Type*} [Field K] [CharZero K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
    (h2 : v (2 : K) < 1) (a π : K)
    (hπ : v π = WithZero.exp (-1 : ℤ)) (hns : ¬ IsSquare a) :
    ∃ x y : K, ¬ IsSquare (x ^ 2 - a * y ^ 2) ∧
      ¬ IsSquare ((x ^ 2 - a * y ^ 2) / a)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.