NYLL
Module

NormFormulaExtension.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaExtension
5 declarations indexed from sourceView source ↗

Module documentation

algebraic extension and integral closure

This file packages the explicit algebraic-extension statement. A valuation is represented by its valuation subring, so uniqueness is literal equality of valuation subrings (equivalently, equivalence of valuations).

Imports2
Imported by11

Declarations

theorem

henselianValuation_iff_henselFactorization

L25 ↗
AlgebraicNumberTheory.Valuations.henselianValuation_iff_henselFactorization
Documentation

the primitive factorization definition for the valuation subring attached to a nonarchimedean absolute value, reduced to the exact factorization property used below.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
Lean source · statement
theorem henselianValuation_iff_henselFactorization
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) :
    ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
        (absoluteValueValuationSubring
          v hnonarch).valuation ↔
      ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
        (absoluteValueValuationSubring v hnonarch)
theorem

normFormula_algebraic_extension

L43 ↗
AlgebraicNumberTheory.Valuations.normFormula_algebraic_extension
Documentation

the finite norm-formula theorem: a Henselian nonarchimedean valuation has exactly one extension to every algebraic extension, and the valuation ring of that extension is the actual integral closure of the base valuation ring.

The extension is expressed by its valuation subring. The first conjunct says that its canonical valuation extends the base valuation; the second is the integral-closure identification.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
Lean source · full declaration
theorem normFormula_algebraic_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (absoluteValueValuationSubring
        v hnonarch).valuation) :
    let V := absoluteValueValuationSubring v hnonarch
    ∃! W : ValuationSubring L,
      V.valuation.HasExtension W.valuation ∧
        W.toSubring = (integralClosure V L).toSubring := by
  let V := absoluteValueValuationSubring v hnonarch
  have hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty V :=
    (henselianValuation_iff_henselFactorization v hnonarch).1 hhens
  have hvalV :
      ∀ z : L,
        z ∈ (integralClosure V L).toSubring ∨
          z⁻¹ ∈ (integralClosure V L).toSubring :=
    normFormula_algebraic_integralClosure_mem_or_inv_of_henselFactorization
      v hnonarch hv
  have hval :
      ∀ z : L,
        z ∈ (integralClosure V.valuation.valuationSubring L).toSubring ∨
          z⁻¹ ∈
            (integralClosure V.valuation.valuationSubring L).toSubring := by
    rw [ValuationSubring.valuationSubring_valuation]
    exact hvalV
  let B : ValuationSubring L :=
    ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
      (L := L) V.valuation hval
  have hBext : V.valuation.HasExtension B.valuation :=
    open ValuationTheory.DiscreteValuationField.Valuation in
      integralClosureValuationSubringOfMemOrInv_hasExtension
        (L := L) V.valuation hval
  have hBclosure : B.toSubring = (integralClosure V L).toSubring := by
    change
      (integralClosure V.valuation.valuationSubring L).toSubring =
        (integralClosure V L).toSubring
    rw [ValuationSubring.valuationSubring_valuation]
  refine ⟨B, ⟨hBext, hBclosure⟩, ?_⟩
  intro W hW
  let : V.valuation.HasExtension W.valuation := hW.1
  simpa only [ValuationSubring.valuationSubring_valuation] using
    open DiscreteValuationField.Valuation in
      normFormula_extension_valuationSubring_eq_integralClosure_of_mem_or_inv
        (K := K) (L := L) V hval W.valuation
theorem

absoluteValueValuation_hasExtension_of_extends

L92 ↗
AlgebraicNumberTheory.Valuations.absoluteValueValuation_hasExtension_of_extends
Documentation

Exact extension of nonarchimedean absolute values supplies extension of the canonical valuations of their closed unit balls.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
Lean source · full declaration
theorem absoluteValueValuation_hasExtension_of_extends
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ)
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w)
    (hext : ∀ a : K, w (algebraMap K L a) = v a) :
    let V := absoluteValueValuationSubring v hv
    let W := absoluteValueValuationSubring w hw
    V.valuation.HasExtension W.valuation := by
  let V := absoluteValueValuationSubring v hv
  let W := absoluteValueValuationSubring w hw
  apply _root_.Valuation.HasExtension.ofComapInteger
  rw [ValuationSubring.integer_valuation, ValuationSubring.integer_valuation]
  have hcomap :=
    comap_absoluteValueUnitBallSubring_eq_of_extends
      v w hv hw hext
  ext x
  change algebraMap K L x ∈ absoluteValueUnitBallSubring w hw ↔
    x ∈ absoluteValueUnitBallSubring v hv
  constructor
  · intro hx
    have hx' : x ∈ Subring.comap (algebraMap K L)
        (absoluteValueUnitBallSubring w hw) := hx
    rw [hcomap] at hx'
    exact hx'
  · intro hx
    have hx' : x ∈ Subring.comap (algebraMap K L)
        (absoluteValueUnitBallSubring w hw) := by
      rw [hcomap]
      exact hx
    exact hx'
theorem

normFormula_finite_normFormulaAbsoluteValue_eq_of_valuationSubring_eq_of_henselFactorization

L128 ↗
AlgebraicNumberTheory.Valuations.normFormula_finite_normFormulaAbsoluteValue_eq_of_valuationSubring_eq_of_henselFactorization
Documentation

Equality of the closed unit balls of an extension absolute value and the finite norm-formula absolute value forces pointwise equality. The normalization is recovered by taking the field norm, so equivalence of valuations is upgraded to equality of the chosen absolute values.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
Lean source · statement
theorem normFormula_finite_normFormulaAbsoluteValue_eq_of_valuationSubring_eq_of_henselFactorization
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (absoluteValueValuationSubring v hnonarch))
    (w : AbsoluteValue L ℝ) (hwnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue w)
    (hw_ext : ∀ a : K, w (algebraMap K L a) = v a)
    (hsub :
      absoluteValueValuationSubring w hwnonarch =
        absoluteValueValuationSubring
          (normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
            (K := K) (L := L) v hnonarch hv)
          (normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_nonarchimedean
            (K := K) (L := L) v hnonarch hv)) :
    w =
      normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
        (K := K) (L := L) v hnonarch hv
theorem

normFormula_finite_extension_norm_formula

L233 ↗
AlgebraicNumberTheory.Valuations.normFormula_finite_extension_norm_formula
Documentation

The finite-degree part of the finite norm-formula theorem: the unique extended absolute value is the norm formula |N(x)|^(1/[L:K]).

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
Lean source · full declaration
theorem normFormula_finite_extension_norm_formula
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (absoluteValueValuationSubring
        v hnonarch).valuation) :
    let hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
        (absoluteValueValuationSubring v hnonarch) :=
      (henselianValuation_iff_henselFactorization v hnonarch).1 hhens
    let extended :=
      normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
        (K := K) (L := L) v hnonarch hv
    LubinTate.Valuations.NonarchimedeanAbsoluteValue extended ∧
      (∀ a : K, extended (algebraMap K L a) = v a) ∧
        (∀ x : L, extended x =
          v (Algebra.norm K x) ^ (1 / (Module.finrank K L : ℝ))) ∧
          ∀ w : AbsoluteValue L ℝ,
            LubinTate.Valuations.NonarchimedeanAbsoluteValue w →
              (∀ a : K, w (algebraMap K L a) = v a) →
                w = extended := by
  let V := absoluteValueValuationSubring v hnonarch
  let hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty V :=
    (henselianValuation_iff_henselFactorization v hnonarch).1 hhens
  let extended :=
    normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
      (K := K) (L := L) v hnonarch hv
  let hextendedNonarch :=
    normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_nonarchimedean
      (K := K) (L := L) v hnonarch hv
  refine ⟨hextendedNonarch, ?_, ?_, ?_⟩
  · exact
      normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_extends_base
        (K := K) (L := L) v hnonarch hv
  · intro x
    exact
      normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_apply
        (K := K) (L := L) v hnonarch hv x
  · intro w hwnonarch hw_ext
    let W := absoluteValueValuationSubring w hwnonarch
    let R := absoluteValueValuationSubring
      extended hextendedNonarch
    let : Algebra.IsAlgebraic K L := Algebra.IsAlgebraic.of_finite K L
    have hvalV :
        ∀ z : L,
          z ∈ (integralClosure V L).toSubring ∨
            z⁻¹ ∈ (integralClosure V L).toSubring :=
      normFormula_algebraic_integralClosure_mem_or_inv_of_henselFactorization
        v hnonarch hv
    have hval :
        ∀ z : L,
          z ∈ (integralClosure V.valuation.valuationSubring L).toSubring ∨
            z⁻¹ ∈
              (integralClosure V.valuation.valuationSubring L).toSubring := by
      rw [ValuationSubring.valuationSubring_valuation]
      exact hvalV
    let : V.valuation.HasExtension W.valuation :=
      absoluteValueValuation_hasExtension_of_extends
        v w hnonarch hwnonarch hw_ext
    have hW :=
      open DiscreteValuationField.Valuation in
        normFormula_extension_valuationSubring_eq_integralClosure_of_mem_or_inv
          (K := K) (L := L) V hval W.valuation
    have hextendedBase : ∀ a : K, extended (algebraMap K L a) = v a :=
      normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_extends_base
        (K := K) (L := L) v hnonarch hv
    let : V.valuation.HasExtension R.valuation :=
      absoluteValueValuation_hasExtension_of_extends
        v extended hnonarch hextendedNonarch hextendedBase
    have hR :=
      open DiscreteValuationField.Valuation in
        normFormula_extension_valuationSubring_eq_integralClosure_of_mem_or_inv
          (K := K) (L := L) V hval R.valuation
    have hsub : W = R := by
      simpa only [ValuationSubring.valuationSubring_valuation] using
        hW.trans hR.symm
    exact
      normFormula_finite_normFormulaAbsoluteValue_eq_of_valuationSubring_eq_of_henselFactorization
        (K := K) (L := L) v hnonarch hv w hwnonarch hw_ext
        (by simpa [W, R, extended, hextendedNonarch] using hsub)

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