NYLL
Module

HerbrandFunction.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.HerbrandFunction
14 declarations indexed from sourceView source ↗

Module documentation

Herbrand functions for a general discretely valued field

This file attaches the group-theoretic Herbrand functions directly to the real lower ramification groups of RealLowerGroups. The only valued-field input is the stated unique-extension hypothesis that the chosen valuation on the top field is the unique extension of the base valuation. In particular, none of the definitions or elementary inverse-function facts below assumes that either field is complete.

Imports2
Imported by6

Declarations

def

lowerRamificationFiltrationOfUniqueExtension

L40 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationFiltrationOfUniqueExtension
Documentation

The integral levels of the real lower-ramification groups, packaged as a AntitoneNormalSubgroupFiltration. This is the general-DVF replacement for the complete-only toLowerRamificationFiltration.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
Lean source · full declaration
def lowerRamificationFiltrationOfUniqueExtension
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) :
    RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration Gal(L/K) where
  lower n := lowerRamificationGroup
    (base := base) (target := target) huniq (n : ℝ)
  lower_normal n := lowerRamificationGroup_normal
    (base := base) (target := target) huniq (n : ℝ)
  antitone := by
    intro m n hmn
    apply lowerRamificationGroup_antitone
      (base := base) (target := target) huniq
    exact_mod_cast hmn
theorem

lowerRamificationFiltrationOfUniqueExtension_lower

L55 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationFiltrationOfUniqueExtension_lower
Documentation

States the theorem lowerRamificationFiltrationOfUniqueExtension_lower.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem lowerRamificationFiltrationOfUniqueExtension_lower
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (n : ℕ) :
    (lowerRamificationFiltrationOfUniqueExtension
      (base := base) (target := target) huniq).lower n =
      lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ)
instance

generalDVFGalFintype

L67 ↗
RamificationTheory.HilbertRamification.Higher.generalDVFGalFintype
Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
instance generalDVFGalFintype : Fintype Gal(L/K)
def

herbrandFunctionOfUniqueExtension

L73 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunctionOfUniqueExtension
Documentation

The Herbrand-function sum formula, defined under the stated unique-extension and separable-residue assumptions: the Herbrand function attached to the actual lower groups.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
def herbrandFunctionOfUniqueExtension
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) (s : ℝ) : ℝ
def

inverseHerbrandFunctionOfUniqueExtension

L81 ↗
RamificationTheory.HilbertRamification.Higher.inverseHerbrandFunctionOfUniqueExtension
Documentation

The inverse Herbrand function in the general-DVF setting.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
def inverseHerbrandFunctionOfUniqueExtension
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) (t : ℝ) : ℝ
theorem

herbrandFunctionOfUniqueExtension_apply

L90 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunctionOfUniqueExtension_apply
Documentation

States the theorem herbrandFunctionOfUniqueExtension_apply.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
omit [FiniteDimensional K L] in
Lean source · statement
theorem herbrandFunctionOfUniqueExtension_apply
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) (s : ℝ) :
    herbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq s =
      RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction
        (lowerRamificationFiltrationOfUniqueExtension
          (base := base) (target := target) huniq) s
theorem

inverseHerbrandFunctionOfUniqueExtension_apply

L102 ↗
RamificationTheory.HilbertRamification.Higher.inverseHerbrandFunctionOfUniqueExtension_apply
Documentation

States the theorem inverseHerbrandFunctionOfUniqueExtension_apply.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
omit [FiniteDimensional K L] in
Lean source · statement
theorem inverseHerbrandFunctionOfUniqueExtension_apply
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) (t : ℝ) :
    inverseHerbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq t =
      DiscreteValuationField.AntitoneNormalSubgroupFiltration.inverseHerbrandFunction
        (lowerRamificationFiltrationOfUniqueExtension
          (base := base) (target := target) huniq) t
theorem

herbrandFunctionOfUniqueExtension_psi

L113 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunctionOfUniqueExtension_psi
Documentation

States the theorem herbrandFunctionOfUniqueExtension_psi.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
theorem herbrandFunctionOfUniqueExtension_psi
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) (t : ℝ) :
    herbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq
        (inverseHerbrandFunctionOfUniqueExtension
          (base := base) (target := target) huniq t) = t
theorem

inverseHerbrandFunctionOfUniqueExtension_eta

L125 ↗
RamificationTheory.HilbertRamification.Higher.inverseHerbrandFunctionOfUniqueExtension_eta
Documentation

States the theorem inverseHerbrandFunctionOfUniqueExtension_eta.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
theorem inverseHerbrandFunctionOfUniqueExtension_eta
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) (s : ℝ) :
    inverseHerbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq
        (herbrandFunctionOfUniqueExtension
          (base := base) (target := target) huniq s) = s
theorem

herbrandFunctionOfUniqueExtension_strictMono

L137 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunctionOfUniqueExtension_strictMono
Documentation

States the theorem herbrandFunctionOfUniqueExtension_strictMono.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
theorem herbrandFunctionOfUniqueExtension_strictMono
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) :
    StrictMono (herbrandFunctionOfUniqueExtension
      (base := base) (target := target) huniq)
theorem

inverseHerbrandFunctionOfUniqueExtension_strictMono

L147 ↗
RamificationTheory.HilbertRamification.Higher.inverseHerbrandFunctionOfUniqueExtension_strictMono
Documentation

States the theorem inverseHerbrandFunctionOfUniqueExtension_strictMono.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
theorem inverseHerbrandFunctionOfUniqueExtension_strictMono
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) :
    StrictMono (inverseHerbrandFunctionOfUniqueExtension
      (base := base) (target := target) huniq)
def

upperRamificationGroupOfUniqueExtension

L158 ↗
RamificationTheory.HilbertRamification.Higher.upperRamificationGroupOfUniqueExtension
Documentation

The upper ramification group defined through the inverse Herbrand function under the noncomplete standing assumptions: G^t = G_{psi(t)}.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
def upperRamificationGroupOfUniqueExtension
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) (t : ℝ) : Subgroup Gal(L/K)
theorem

upperRamificationGroupOfUniqueExtension_herbrandFunction

L167 ↗
RamificationTheory.HilbertRamification.Higher.upperRamificationGroupOfUniqueExtension_herbrandFunction
Documentation

States the theorem upperRamificationGroupOfUniqueExtension_herbrandFunction.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
theorem upperRamificationGroupOfUniqueExtension_herbrandFunction
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) (s : ℝ) :
    upperRamificationGroupOfUniqueExtension
        (base := base) (target := target) huniq
        (herbrandFunctionOfUniqueExtension
          (base := base) (target := target) huniq s) =
      lowerRamificationGroup
        (base := base) (target := target) huniq s
theorem

inverseHerbrandFunctionOfUniqueExtension_ge_neg_one_iff

L184 ↗
RamificationTheory.HilbertRamification.Higher.inverseHerbrandFunctionOfUniqueExtension_ge_neg_one_iff
Documentation

States the theorem inverseHerbrandFunctionOfUniqueExtension_ge_neg_one_iff.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
namespace Higher
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
noncomputable local instance generalDVFGalFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
  (inverseHerbrandFunction_mem_Ici_neg_one_iff) in
Lean source · statement
theorem inverseHerbrandFunctionOfUniqueExtension_ge_neg_one_iff
    (huniq : DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
      base target) {t : ℝ} :
    -1 ≤ inverseHerbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq t ↔ -1 ≤ t

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