NYLL
Module

RamificationDepth.lean

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

Module documentation

General-DVF ramification numbers as a nonarchimedean depth

Imports4
Imported by5

Declarations

theorem

addVal_valuationSubringAutOfUniqueExtension

L33 ↗
RamificationTheory.HilbertRamification.Higher.addVal_valuationSubringAutOfUniqueExtension
Documentation

The additive valuation of the target DVR is invariant under the valuation-ring action supplied by unique extension.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 addVal_valuationSubringAutOfUniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (sigma : Gal(L/K)) (a : target.valuationSubring) :
    IsDiscreteValuationRing.addVal target.valuationSubring
        (valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a) =
      IsDiscreteValuationRing.addVal target.valuationSubring a
theorem

valuationSubringAutOfUniqueExtension_mul_sub_eq

L47 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_mul_sub_eq
Documentation

Product displacement identity for the unique-extension action.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 valuationSubringAutOfUniqueExtension_mul_sub_eq
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (a : target.valuationSubring) (sigma tau : Gal(L/K)) :
    valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq (sigma * tau) a - a =
      valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma
          (valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq tau a - a) +
        (valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a - a)
theorem

ramificationNumberOfUniqueExtension_mul_ge_min

L64 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberOfUniqueExtension_mul_ge_min
Documentation

States the theorem ramificationNumberOfUniqueExtension_mul_ge_min.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 ramificationNumberOfUniqueExtension_mul_ge_min
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (a : target.valuationSubring) (sigma tau : Gal(L/K)) :
    min
        (ramificationNumberOfUniqueExtension
          (base := base) (target := target) huniq a sigma)
        (ramificationNumberOfUniqueExtension
          (base := base) (target := target) huniq a tau) ≤
      ramificationNumberOfUniqueExtension
        (base := base) (target := target) huniq a (sigma * tau)
theorem

ramificationNumberOfUniqueExtension_mul_eq_min_of_ne

L94 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberOfUniqueExtension_mul_eq_min_of_ne
Documentation

States the theorem ramificationNumberOfUniqueExtension_mul_eq_min_of_ne.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 ramificationNumberOfUniqueExtension_mul_eq_min_of_ne
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (a : target.valuationSubring) {sigma tau : Gal(L/K)}
    (hne : ramificationNumberOfUniqueExtension
          (base := base) (target := target) huniq a sigma ≠
        ramificationNumberOfUniqueExtension
          (base := base) (target := target) huniq a tau) :
    ramificationNumberOfUniqueExtension
        (base := base) (target := target) huniq a (sigma * tau) =
      min
        (ramificationNumberOfUniqueExtension
          (base := base) (target := target) huniq a sigma)
        (ramificationNumberOfUniqueExtension
          (base := base) (target := target) huniq a tau)
theorem

ramificationNumberOfUniqueExtension_eq_top_iff

L134 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberOfUniqueExtension_eq_top_iff
Documentation

States the theorem ramificationNumberOfUniqueExtension_eq_top_iff.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 ramificationNumberOfUniqueExtension_eq_top_iff
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {a : target.valuationSubring}
    (ha : Algebra.adjoin base.valuationSubring
      ({a} : Set target.valuationSubring) = ⊤)
    (sigma : Gal(L/K)) :
    ramificationNumberOfUniqueExtension
        (base := base) (target := target) huniq a sigma = ⊤ ↔ sigma = 1
theorem

ramificationNumberOfUniqueExtension_conj

L182 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberOfUniqueExtension_conj
Documentation

States the theorem ramificationNumberOfUniqueExtension_conj.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 ramificationNumberOfUniqueExtension_conj
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {a : target.valuationSubring}
    (ha : Algebra.adjoin base.valuationSubring
      ({a} : Set target.valuationSubring) = ⊤)
    (sigma tau : Gal(L/K)) :
    ramificationNumberOfUniqueExtension
        (base := base) (target := target) huniq a (tau * sigma * tau⁻¹) =
      ramificationNumberOfUniqueExtension
        (base := base) (target := target) huniq a sigma
def

ramificationNumberDepthOfUniqueExtension

L235 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberDepthOfUniqueExtension
Documentation

The canonical ramification number is a nonarchimedean depth under the general DVF standing hypotheses.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · full declaration
def ramificationNumberDepthOfUniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target) :
    RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth Gal(L/K) where
  depth := intrinsicRamificationNumberOfUniqueExtension
    (base := base) (target := target) huniq
  depth_eq_top_iff := by
    intro sigma
    exact ramificationNumberOfUniqueExtension_eq_top_iff
      (base := base) (target := target) huniq
      (chosenRamificationGeneratorOfUniqueExtension_adjoin_eq_top
        (base := base) (target := target) huniq) sigma
  depth_mul_ge_min := ramificationNumberOfUniqueExtension_mul_ge_min
    (base := base) (target := target) huniq
      (chosenRamificationGeneratorOfUniqueExtension
        (base := base) (target := target) huniq)
  depth_mul_eq_min_of_ne := ramificationNumberOfUniqueExtension_mul_eq_min_of_ne
    (base := base) (target := target) huniq
      (chosenRamificationGeneratorOfUniqueExtension
        (base := base) (target := target) huniq)
  depth_conj := fun gamma sigma => ramificationNumberOfUniqueExtension_conj
    (base := base) (target := target) huniq
      (chosenRamificationGeneratorOfUniqueExtension_adjoin_eq_top
        (base := base) (target := target) huniq) sigma gamma
theorem

ramificationNumberDepthOfUniqueExtension_depth

L262 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberDepthOfUniqueExtension_depth
Documentation

States the theorem ramificationNumberDepthOfUniqueExtension_depth.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
theorem ramificationNumberDepthOfUniqueExtension_depth
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (sigma : Gal(L/K)) :
    (ramificationNumberDepthOfUniqueExtension
      (base := base) (target := target) huniq).depth sigma =
      intrinsicRamificationNumberOfUniqueExtension
        (base := base) (target := target) huniq sigma

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