Module

RamificationAddVal.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.RamificationAddVal

3 declarations indexed from sourceView source ↗

Module documentation

Additive valuations in finite complete-DVF extensions

The normalized additive valuation on the target valuation ring restricts to the ramification index times the normalized additive valuation on the base valuation ring. The proof is characteristic-independent and follows from the ideal identity m_K · O_L = m_L ^ e.

Imports2

Imported by6

theorem

addVal_integerMap_eq_ramificationIndex_nsmul

L39 ↗

LocalFieldTheory.DiscreteValuationField.ValuedExtension.addVal_integerMap_eq_ramificationIndex_nsmul

Documentation

The target normalized additive valuation of an element from the base valuation ring is its base additive valuation multiplied by the ramification index. This includes the zero element, whose additive valuation is ⊤.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem addVal_integerMap_eq_ramificationIndex_nsmul
    (a : base.valuationSubring) :
    IsDiscreteValuationRing.addVal target.valuationSubring
        (integerMap base.toDVF target.toDVF a) =
      ramificationIndex base.toDVF target.toDVF •
        IsDiscreteValuationRing.addVal base.valuationSubring a

theorem

addVal_integerMap_eq_ramificationIndex_of_irreducible

L132 ↗

LocalFieldTheory.DiscreteValuationField.ValuedExtension.addVal_integerMap_eq_ramificationIndex_of_irreducible

Documentation

The target additive valuation of the image of a base uniformizer is the ramification index.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem addVal_integerMap_eq_ramificationIndex_of_irreducible
    {a : base.valuationSubring} (ha : Irreducible a) :
    IsDiscreteValuationRing.addVal target.valuationSubring
        (integerMap base.toDVF target.toDVF a) =
      (ramificationIndex base.toDVF target.toDVF : ℕ∞)

theorem

ramificationIndex_eq_one_of_integerMap_uniformizer

L142 ↗

LocalFieldTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_eq_one_of_integerMap_uniformizer

Documentation

If a base uniformizer remains a uniformizer after applying the valuation-ring map, then the relative ramification index is one.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem ramificationIndex_eq_one_of_integerMap_uniformizer
    (a : base.valuationSubring)
    (ha : base.valuation.IsUniformizer (a : K))
    (hmap :
      target.valuation.IsUniformizer
        ((integerMap base.toDVF target.toDVF a :
          target.valuationSubring) : L)) :
    ramificationIndex base.toDVF target.toDVF = 1

Module documentation

Additive valuations in finite complete-DVF extensions

Declarations

addVal_integerMap_eq_ramificationIndex_nsmul

addVal_integerMap_eq_ramificationIndex_of_irreducible

ramificationIndex_eq_one_of_integerMap_uniformizer