NYLL
Module

FiniteGaloisLevel.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteGaloisLevel
16 declarations indexed from sourceView source ↗

Module documentation

Chosen integral-closure ramification filtrations at finite Galois levels

For a complete discretely valued field K and a finite Galois intermediate field E of an algebraic closure, an existence theorem for the integral closure of the valuation ring of K supplies complete-DVF structures on E. This file makes one noncomputable choice of such data. Completeness then gives uniqueness of the extended valuation, so real lower groups and Herbrand upper groups can be formed without asking a caller to provide a filtration. Choice independence is proved in the companion module.

Imports3
Imported by3

Declarations

theorem

chosenIntegralClosureData_exists

L37 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureData_exists
Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · full declaration
theorem chosenIntegralClosureData_exists
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K)) :
    ∃ target : CompleteDVF.{u, 0} E,
      ∃ hExt : base.valuation.HasExtension target.valuation,
        letI : base.valuation.HasExtension target.valuation := hExt
        IsIntegralClosure target.valuationSubring
          base.valuationSubring E ∧
          degree base.toDVF target.toDVF =
            ramificationIndex base.toDVF target.toDVF *
              residueDegree base.toDVF target.toDVF :=
  exists_integralClosure_standard_fundamental_identity
    (K := K) (L := E) base
def

chosenIntegralClosureTarget

L53 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureTarget
Documentation

A complete-DVF structure on a finite Galois level, chosen from the integral-closure existence theorem.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
def chosenIntegralClosureTarget
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K)) :
    CompleteDVF.{u, 0} E
theorem

chosenIntegralClosureTargetHasExtension

L61 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureTargetHasExtension
Documentation

The valuation on chosenIntegralClosureTarget extends the valuation on the base complete DVF.

Source context 7 commands

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

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

instChosenIntegralClosureTargetHasExtension

L68 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.instChosenIntegralClosureTargetHasExtension
Documentation

Provides the instance instChosenIntegralClosureTargetHasExtension.

Source context 7 commands

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

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

chosenIntegralClosureTarget_isIntegralClosure

L76 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureTarget_isIntegralClosure
Documentation

The valuation ring of the chosen finite-level target is the integral closure of the base valuation ring.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenIntegralClosureTarget_isIntegralClosure
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K)) :
    IsIntegralClosure (chosenIntegralClosureTarget base E).valuationSubring
      base.valuationSubring E
theorem

chosenIntegralClosureTarget_isDefectless

L86 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureTarget_isDefectless
Documentation

The chosen target satisfies the fundamental equality; no auxiliary extension marker is selected.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenIntegralClosureTarget_isDefectless
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K)) :
    IsDefectless base.toDVF (chosenIntegralClosureTarget base E).toDVF
theorem

chosenIntegralClosureTarget_hasUniqueValuationExtension

L95 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureTarget_hasUniqueValuationExtension
Documentation

Uniqueness of the extended valuation at a finite Galois level, in the complete-DVF formulation.

Source context 7 commands

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

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

chosenIntegralClosureTarget_hasUniqueDVFValuationExtension

L105 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenIntegralClosureTarget_hasUniqueDVFValuationExtension
Documentation

Uniqueness after forgetting completeness, in the precise universe needed by the real lower ramification groups.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenIntegralClosureTarget_hasUniqueDVFValuationExtension
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K)) :
    RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, u, 0, y}
      base.toDVF (chosenIntegralClosureTarget base E).toDVF
def

chosenLowerRamificationFiltration

L114 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenLowerRamificationFiltration
Documentation

The finite-level lower ramification filtration attached to the chosen integral-closure valuation.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
def chosenLowerRamificationFiltration
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K)) :
    RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
      Gal(E / K)
def

chosenUpperRamificationFiltration

L125 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenUpperRamificationFiltration
Documentation

The finite-level real upper ramification filtration attached to the chosen integral-closure valuation.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
def chosenUpperRamificationFiltration
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K)) :
    ℝ → Subgroup Gal(E / K)
abbrev

chosenUpperRamificationGroup

L134 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenUpperRamificationGroup
Documentation

The chosen upper ramification group at a real index.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
abbrev chosenUpperRamificationGroup
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (t : ℝ) : Subgroup Gal(E / K)
theorem

chosenUpperRamificationFiltration_apply

L142 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenUpperRamificationFiltration_apply
Documentation

States the theorem chosenUpperRamificationFiltration_apply.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenUpperRamificationFiltration_apply
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (t : ℝ) :
    chosenUpperRamificationFiltration base E t =
      Higher.upperRamificationGroupOfUniqueExtension
        (base := base.toDVF) (target := (chosenIntegralClosureTarget base E).toDVF)
        (chosenIntegralClosureTarget_hasUniqueDVFValuationExtension base E) t
theorem

chosenLowerRamificationGroup_normal

L153 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenLowerRamificationGroup_normal
Documentation

States the theorem chosenLowerRamificationGroup_normal.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenLowerRamificationGroup_normal
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (n : ℕ) :
    ((chosenLowerRamificationFiltration base E).lower n).Normal
theorem

chosenLowerRamificationGroup_isClosed

L161 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenLowerRamificationGroup_isClosed
Documentation

Every chosen finite-level integral lower ramification group is closed.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenLowerRamificationGroup_isClosed
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (n : ℕ) :
    IsClosed
      ((chosenLowerRamificationFiltration base E).lower n : Set Gal(E / K))
theorem

chosenUpperRamificationGroup_normal

L170 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenUpperRamificationGroup_normal
Documentation

States the theorem chosenUpperRamificationGroup_normal.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenUpperRamificationGroup_normal
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (t : ℝ) :
    (chosenUpperRamificationGroup base E t).Normal
theorem

chosenUpperRamificationGroup_isClosed

L183 ↗
RamificationTheory.HilbertRamification.FiniteGaloisLevel.chosenUpperRamificationGroup_isClosed
Documentation

Every chosen finite-level upper ramification group is closed.

Source context 7 commands

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

noncomputable section
universe u v y
namespace RamificationTheory.HilbertRamification.FiniteGaloisLevel
open ValuationTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenUpperRamificationGroup_isClosed
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (t : ℝ) :
    IsClosed (chosenUpperRamificationGroup base E t : Set Gal(E / K))

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