Module

UniqueExtensionPrimitive.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.UniqueExtensionPrimitive

5 declarations indexed from sourceView source ↗

Module documentation

primitive irreducible reductions

This file supplies the last Galois/Newton-polygon input in the converse of the unique-extension criterion. Uniqueness of the extension valuation ring makes it invariant under the finite Galois group of a splitting field. Consequently conjugate roots have the same value. Vieta's formulas then show that a primitive irreducible polynomial has either full-degree reduction or constant reduction; in the full-degree case the monic normalization has no coprime nonconstant residual factorization.

Imports3

Nyll.ValuedFieldTheory.Valuation.Henselian.UniqueExtensionReduction
Nyll.ValuedFieldTheory.Valuation.Henselian.MonicFactorization
Mathlib.GroupTheory.OrderOfElement

Imported by11

theorem

valuation_algEquiv_eq_of_unique_extension_of_finiteDimensional

L37 ↗

AlgebraicNumberTheory.Valuations.valuation_algEquiv_eq_of_unique_extension_of_finiteDimensional

Documentation

A finite-order ground-field automorphism stabilizing a valuation subring preserves its canonical valuation exactly. Stabilization first preserves the order relation on values. A strict change would iterate around the finite orbit of the automorphism and give a strict cycle.

Source context 6 commands

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

noncomputable section
open Polynomial
namespace AlgebraicNumberTheory
namespace Valuations
open ValuationTheory.Valuations
universe u

Lean source · statement

theorem valuation_algEquiv_eq_of_unique_extension_of_finiteDimensional
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (σ : L ≃ₐ[K] L) (x : L) :
    W.valuation (σ x) = W.valuation x

theorem

valuation_eq_on_roots_of_irreducible_of_unique_extension

L119 ↗

AlgebraicNumberTheory.Valuations.valuation_eq_on_roots_of_irreducible_of_unique_extension

Documentation

Roots of one irreducible ground-field polynomial have the same canonical value in a finite normal splitting field with a unique extension valuation ring.

Source context 6 commands

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

noncomputable section
open Polynomial
namespace AlgebraicNumberTheory
namespace Valuations
open ValuationTheory.Valuations
universe u

Lean source · statement

theorem valuation_eq_on_roots_of_irreducible_of_unique_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Normal K L] [FiniteDimensional K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (p : Polynomial K) (hirr : Irreducible p)
    {a b : L}
    (ha : a ∈ (p.map (algebraMap K L)).roots)
    (hb : b ∈ (p.map (algebraMap K L)).roots) :
    W.valuation a = W.valuation b

theorem

valuation_coeff_prod_X_sub_C_lt_coeff_zero_of_one_lt

L152 ↗

AlgebraicNumberTheory.Valuations.valuation_coeff_prod_X_sub_C_lt_coeff_zero_of_one_lt

Documentation

If all roots of a split monic product have value strictly larger than one, every positive-degree coefficient has value strictly smaller than the constant coefficient.

Source context 6 commands

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

noncomputable section
open Polynomial
namespace AlgebraicNumberTheory
namespace Valuations
open ValuationTheory.Valuations
universe u

Lean source · full declaration

theorem valuation_coeff_prod_X_sub_C_lt_coeff_zero_of_one_lt
    {L Γ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation L Γ) (s : Multiset L)
    (hs : ∀ α ∈ s, 1 < w α) (j : ℕ) (hj : 0 < j) :
    w (((s.map (fun α => Polynomial.X - Polynomial.C α)).prod).coeff j) <
      w (((s.map (fun α => Polynomial.X - Polynomial.C α)).prod).coeff 0) :=
  DiscreteValuationField.valuation_coeff_prod_X_sub_C_lt_coeff_zero_of_one_lt
    w s hs j hj

theorem

primitive_irreducible_reduction_natDegree_zero_of_leadingCoeff_nonunit

L165 ↗

AlgebraicNumberTheory.Valuations.primitive_irreducible_reduction_natDegree_zero_of_leadingCoeff_nonunit

Documentation

In the nonmonic branch of Artin's argument, uniqueness on the splitting field forces every root to have value greater than one. Vieta's formula then puts every positive-degree coefficient in the maximal ideal, so the reduction is constant.

Source context 6 commands

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

noncomputable section
open Polynomial
namespace AlgebraicNumberTheory
namespace Valuations
open ValuationTheory.Valuations
universe u

Lean source · statement

theorem primitive_irreducible_reduction_natDegree_zero_of_leadingCoeff_nonunit
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (Q : Polynomial V) (hQprim : Q.IsPrimitive)
    (hQirr : Irreducible (Q.map V.subtype))
    [IsSplittingField K L (Q.map V.subtype)]
    (hlead : ¬ IsUnit Q.leadingCoeff) :
    (Q.map (IsLocalRing.residue V)).natDegree = 0

theorem

primitiveIrreducibleReductionProperty_of_unique_algebraic_extensions

L309 ↗

AlgebraicNumberTheory.Valuations.primitiveIrreducibleReductionProperty_of_unique_algebraic_extensions

Documentation

The primitive-irreducible reduction property in the last paragraph of the proof of the unique-extension criterion, obtained directly from unique extension valuation rings on algebraic fields.

Source context 6 commands

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

noncomputable section
open Polynomial
namespace AlgebraicNumberTheory
namespace Valuations
open ValuationTheory.Valuations
universe u

Lean source · statement

theorem primitiveIrreducibleReductionProperty_of_unique_algebraic_extensions
    {K : Type u} [Field K] (V : ValuationSubring K)
    (hunique : ∀ (E : Type u) [Field E] [Algebra K E]
      [Algebra.IsAlgebraic K E],
        ∃! W : ValuationSubring E,
          V.valuation.HasExtension W.valuation) :
    DiscreteValuationField.PrimitiveIrreducibleReductionProperty V

Module documentation

primitive irreducible reductions

Declarations

valuation_algEquiv_eq_of_unique_extension_of_finiteDimensional

valuation_eq_on_roots_of_irreducible_of_unique_extension

valuation_coeff_prod_X_sub_C_lt_coeff_zero_of_one_lt

primitive_irreducible_reduction_natDegree_zero_of_leadingCoeff_nonunit

primitiveIrreducibleReductionProperty_of_unique_algebraic_extensions