NYLL
Module

UniqueExtensionIntegralClosure.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.UniqueExtensionIntegralClosure
8 declarations indexed from sourceView source ↗

Module documentation

Integral closure for a unique discrete valuation extension

This file supplies the noncomplete integral-closure input used in ramification-number theory. For a finite Galois extension with a uniquely chosen extension of the base discrete valuation, the Galois orbit polynomial of an integer has coefficients in the base valuation ring. Consequently the target valuation ring is integral, hence finite, over the base valuation ring.

No completeness or Henselian hypothesis is used.

Imports3
Imported by3

Declarations

def

integralOrbitPolynomial

L44 ↗
RamificationTheory.HilbertRamification.Higher.integralOrbitPolynomial
Documentation

The full Galois-orbit polynomial of an element of the target valuation ring. Uniqueness of the valuation extension makes every factor integral.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open ValuationTheory.DiscreteValuationField.Valuation
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
def integralOrbitPolynomial
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (a : target.valuationSubring) : Polynomial target.valuationSubring
theorem

integralOrbitPolynomial_monic

L56 ↗
RamificationTheory.HilbertRamification.Higher.integralOrbitPolynomial_monic
Documentation

States the theorem integralOrbitPolynomial_monic.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open ValuationTheory.DiscreteValuationField.Valuation
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem integralOrbitPolynomial_monic
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (a : target.valuationSubring) :
    (integralOrbitPolynomial
      (base := base) (target := target) huniq a).Monic
theorem

integralOrbitPolynomial_map_valuationSubringAut

L69 ↗
RamificationTheory.HilbertRamification.Higher.integralOrbitPolynomial_map_valuationSubringAut
Documentation

The orbit polynomial is invariant under every Galois automorphism.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open ValuationTheory.DiscreteValuationField.Valuation
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem integralOrbitPolynomial_map_valuationSubringAut
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (a : target.valuationSubring) (ρ : Gal(L/K)) :
    (integralOrbitPolynomial
        (base := base) (target := target) huniq a).map
      (valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq ρ).toRingHom =
      integralOrbitPolynomial
        (base := base) (target := target) huniq a
theorem

integralOrbitPolynomial_coeff_mem_range

L117 ↗
RamificationTheory.HilbertRamification.Higher.integralOrbitPolynomial_coeff_mem_range
Documentation

Every coefficient of the integral orbit polynomial descends to the base valuation ring.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open ValuationTheory.DiscreteValuationField.Valuation
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem integralOrbitPolynomial_coeff_mem_range
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (a : target.valuationSubring) (n : ℕ) :
    (integralOrbitPolynomial
        (base := base) (target := target) huniq a).coeff n ∈
      Set.range (algebraMap base.valuationSubring target.valuationSubring)
theorem

target_valuationSubring_element_isIntegral_of_uniqueExtension

L149 ↗
RamificationTheory.HilbertRamification.Higher.target_valuationSubring_element_isIntegral_of_uniqueExtension
Documentation

Every target integer is integral over the base valuation ring. The proof uses its monic Galois-orbit polynomial and coefficient descent.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open ValuationTheory.DiscreteValuationField.Valuation
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem target_valuationSubring_element_isIntegral_of_uniqueExtension
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (a : target.valuationSubring) :
    IsIntegral base.valuationSubring a
theorem

target_valuationSubring_isIntegral_of_uniqueExtension

L184 ↗
RamificationTheory.HilbertRamification.Higher.target_valuationSubring_isIntegral_of_uniqueExtension
Documentation

The target valuation ring is integral over the base valuation ring under the standing unique-extension hypotheses of ramification-number theory.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open ValuationTheory.DiscreteValuationField.Valuation
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem target_valuationSubring_isIntegral_of_uniqueExtension
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target) :
    Algebra.IsIntegral base.valuationSubring target.valuationSubring
theorem

target_valuationSubring_isIntegralClosure_of_uniqueExtension

L194 ↗
RamificationTheory.HilbertRamification.Higher.target_valuationSubring_isIntegralClosure_of_uniqueExtension
Documentation

Under the standing hypotheses, the target valuation ring is the actual integral closure of the base valuation ring in L.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open ValuationTheory.DiscreteValuationField.Valuation
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem target_valuationSubring_isIntegralClosure_of_uniqueExtension
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target) :
    IsIntegralClosure target.valuationSubring base.valuationSubring L
theorem

target_valuationSubring_moduleFinite_of_uniqueExtension

L207 ↗
RamificationTheory.HilbertRamification.Higher.target_valuationSubring_moduleFinite_of_uniqueExtension
Documentation

The target valuation ring is finite over the base valuation ring. This is the noncomplete replacement for the completeness-based finite-module input formerly used by the ramification-number theory monogeneity proof.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open ValuationTheory.DiscreteValuationField.Valuation
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem target_valuationSubring_moduleFinite_of_uniqueExtension
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target) :
    Module.Finite base.valuationSubring target.valuationSubring

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