NYLL
Module

FiniteGaloisLevelIndependence.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteGaloisLevelIndependence
15 declarations indexed from sourceView source ↗

Module documentation

Choice independence at finite Galois levels

The ramification filtration of a finite extension depends only on its valuation ring. For a finite Galois level over a complete discretely valued field, uniqueness of the extended valuation therefore identifies the filtration formed from the chosen integral-closure target with the filtration formed from any other complete-DVF target extending the base valuation.

Imports1
Imported by2

Declarations

theorem

lowerRamificationFiltration_ext

L37 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationFiltration_ext
Source context 10 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.Higher
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : DVF.{u, v} K}
variable {target : DVF.{w, x} L} {target' : DVF.{w, y} L}
variable [base.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target'.valuation]
Lean source · statement
theorem lowerRamificationFiltration_ext
    {G : Type z} [Group G]
    {F F' :
      RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration G}
    (h : F.lower = F'.lower) :
    F = F'
theorem

lowerRamificationGroup_eq_of_valuationSubring_eq

L50 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroup_eq_of_valuationSubring_eq
Documentation

Real lower ramification groups are unchanged when the two target valuations have the same valuation ring.

Source context 10 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.Higher
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : DVF.{u, v} K}
variable {target : DVF.{w, x} L} {target' : DVF.{w, y} L}
variable [base.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target'.valuation]
Lean source · statement
theorem lowerRamificationGroup_eq_of_valuationSubring_eq
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x} base target)
    (huniq' : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, y, y} base target')
    (hvaluationSubring :
      target.valuation.valuationSubring = target'.valuation.valuationSubring)
    (s : ℝ) :
    lowerRamificationGroup
        (base := base) (target := target) huniq s =
      lowerRamificationGroup
        (base := base) (target := target') huniq' s
theorem

lowerRamificationFiltration_eq_of_valuationSubring_eq

L151 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationFiltration_eq_of_valuationSubring_eq
Documentation

Integral lower ramification filtrations are unchanged when the two target valuations have the same valuation ring.

Source context 10 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.Higher
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : DVF.{u, v} K}
variable {target : DVF.{w, x} L} {target' : DVF.{w, y} L}
variable [base.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target'.valuation]
Lean source · statement
theorem lowerRamificationFiltration_eq_of_valuationSubring_eq
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x} base target)
    (huniq' : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, y, y} base target')
    (hvaluationSubring :
      target.valuation.valuationSubring = target'.valuation.valuationSubring) :
    lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target) huniq =
      lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target') huniq'
theorem

herbrandFunction_eq_of_valuationSubring_eq

L168 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunction_eq_of_valuationSubring_eq
Documentation

Herbrand functions are unchanged when the two target valuations have the same valuation ring.

Source context 10 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.Higher
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : DVF.{u, v} K}
variable {target : DVF.{w, x} L} {target' : DVF.{w, y} L}
variable [base.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target'.valuation]
Lean source · statement
theorem herbrandFunction_eq_of_valuationSubring_eq
    [FiniteDimensional K L]
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x} base target)
    (huniq' : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, y, y} base target')
    (hvaluationSubring :
      target.valuation.valuationSubring = target'.valuation.valuationSubring) :
    herbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq =
      herbrandFunctionOfUniqueExtension
        (base := base) (target := target') huniq'
theorem

inverseHerbrandFunction_eq_of_valuationSubring_eq

L188 ↗
RamificationTheory.HilbertRamification.Higher.inverseHerbrandFunction_eq_of_valuationSubring_eq
Documentation

Inverse Herbrand functions are unchanged when the two target valuations have the same valuation ring.

Source context 10 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.Higher
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : DVF.{u, v} K}
variable {target : DVF.{w, x} L} {target' : DVF.{w, y} L}
variable [base.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target'.valuation]
Lean source · statement
theorem inverseHerbrandFunction_eq_of_valuationSubring_eq
    [FiniteDimensional K L]
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x} base target)
    (huniq' : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, y, y} base target')
    (hvaluationSubring :
      target.valuation.valuationSubring = target'.valuation.valuationSubring) :
    inverseHerbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq =
      inverseHerbrandFunctionOfUniqueExtension
        (base := base) (target := target') huniq'
theorem

upperRamificationGroup_eq_of_valuationSubring_eq

L208 ↗
RamificationTheory.HilbertRamification.Higher.upperRamificationGroup_eq_of_valuationSubring_eq
Documentation

Upper ramification groups are unchanged when the two target valuations have the same valuation ring.

Source context 10 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.Higher
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : DVF.{u, v} K}
variable {target : DVF.{w, x} L} {target' : DVF.{w, y} L}
variable [base.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target'.valuation]
Lean source · statement
theorem upperRamificationGroup_eq_of_valuationSubring_eq
    [FiniteDimensional K L]
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x} base target)
    (huniq' : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, y, y} base target')
    (hvaluationSubring :
      target.valuation.valuationSubring = target'.valuation.valuationSubring)
    (t : ℝ) :
    upperRamificationGroupOfUniqueExtension
        (base := base) (target := target) huniq t =
      upperRamificationGroupOfUniqueExtension
        (base := base) (target := target') huniq' t
theorem

chosenIntegralClosureTarget_valuation_isEquiv

L241 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureTarget_valuation_isEquiv
Documentation

The valuation on the chosen integral-closure target is equivalent to the valuation on every other complete-DVF target extending the base valuation.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenIntegralClosureTarget_valuation_isEquiv
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation] :
    (chosenIntegralClosureTarget base E).valuation.IsEquiv target.valuation
theorem

chosenIntegralClosureTarget_valuationSubring_eq

L251 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureTarget_valuationSubring_eq
Documentation

The chosen integral-closure valuation ring equals the valuation ring of every other complete-DVF target extending the base valuation.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenIntegralClosureTarget_valuationSubring_eq
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation] :
    (chosenIntegralClosureTarget base E).valuation.valuationSubring =
      target.valuation.valuationSubring
theorem

hasUniqueValuationExtension_of_finiteGaloisLevel

L264 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.hasUniqueValuationExtension_of_finiteGaloisLevel
Documentation

Every complete-DVF target at the same finite Galois level inherits unique valuation extension from the chosen target.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem hasUniqueValuationExtension_of_finiteGaloisLevel
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation] :
    ValuedExtension.HasUniqueValuationExtension.{u, v, u, x, y}
      (base := base) (target := target)
theorem

hasUniqueDVFValuationExtension_of_finiteGaloisLevel

L277 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.hasUniqueDVFValuationExtension_of_finiteGaloisLevel
Documentation

The preceding uniqueness statement after forgetting completeness.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem hasUniqueDVFValuationExtension_of_finiteGaloisLevel
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation] :
    RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, u, x, y}
      base.toDVF target.toDVF
theorem

chosenLowerRamificationGroup_eq

L288 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenLowerRamificationGroup_eq
Documentation

The chosen real lower ramification groups agree with those formed from any other complete-DVF target at the same finite Galois level.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenLowerRamificationGroup_eq
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation]
    (s : ℝ) :
    Higher.lowerRamificationGroup
        (base := base.toDVF)
        (target := (chosenIntegralClosureTarget base E).toDVF)
        (chosenIntegralClosureTarget_hasUniqueDVFValuationExtension base E) s =
      Higher.lowerRamificationGroup
        (base := base.toDVF) (target := target.toDVF)
        (hasUniqueDVFValuationExtension_of_finiteGaloisLevel base E target) s
theorem

chosenLowerRamificationFiltration_eq

L308 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenLowerRamificationFiltration_eq
Documentation

The chosen integral lower filtration agrees with that formed from any other complete-DVF target at the same finite Galois level.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenLowerRamificationFiltration_eq
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation] :
    chosenLowerRamificationFiltration base E =
      Higher.lowerRamificationFiltrationOfUniqueExtension
        (base := base.toDVF) (target := target.toDVF)
        (hasUniqueDVFValuationExtension_of_finiteGaloisLevel base E target)
theorem

chosenHerbrandFunction_eq

L324 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenHerbrandFunction_eq
Documentation

The chosen Herbrand function agrees with that formed from any other complete-DVF target at the same finite Galois level.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenHerbrandFunction_eq
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation] :
    Higher.herbrandFunctionOfUniqueExtension
        (base := base.toDVF)
        (target := (chosenIntegralClosureTarget base E).toDVF)
        (chosenIntegralClosureTarget_hasUniqueDVFValuationExtension base E) =
      Higher.herbrandFunctionOfUniqueExtension
        (base := base.toDVF) (target := target.toDVF)
        (hasUniqueDVFValuationExtension_of_finiteGaloisLevel base E target)
theorem

chosenInverseHerbrandFunction_eq

L343 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenInverseHerbrandFunction_eq
Documentation

The chosen inverse Herbrand function agrees with that formed from any other complete-DVF target at the same finite Galois level.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenInverseHerbrandFunction_eq
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation] :
    Higher.inverseHerbrandFunctionOfUniqueExtension
        (base := base.toDVF)
        (target := (chosenIntegralClosureTarget base E).toDVF)
        (chosenIntegralClosureTarget_hasUniqueDVFValuationExtension base E) =
      Higher.inverseHerbrandFunctionOfUniqueExtension
        (base := base.toDVF) (target := target.toDVF)
        (hasUniqueDVFValuationExtension_of_finiteGaloisLevel base E target)
theorem

chosenUpperRamificationGroup_eq

L362 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenUpperRamificationGroup_eq
Documentation

The chosen upper ramification groups agree with those formed from any other complete-DVF target at the same finite Galois level.

Source context 6 commands

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

noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenUpperRamificationGroup_eq
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (target : CompleteDVF.{u, x} E)
    [base.valuation.HasExtension target.valuation]
    (t : ℝ) :
    chosenUpperRamificationGroup base E t =
      Higher.upperRamificationGroupOfUniqueExtension
        (base := base.toDVF) (target := target.toDVF)
        (hasUniqueDVFValuationExtension_of_finiteGaloisLevel base E target) t

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