Module

RamificationIndexComparison.lean

Nyll.ValuedFieldTheory.Ramification.RamificationIndexComparison

3 declarations indexed from sourceView source ↗

Module documentation

Comparing exponential and canonical ramification indices

This module compares the exponential-valuation presentation of ramification with the canonical complete-DVF presentation. The comparison is independent of any cyclotomic or Kronecker--Weber hypotheses.

Imports2

Imported by3

theorem

map_maximalIdeal_ringEquiv

L27 ↗

RamificationTheory.map_maximalIdeal_ringEquiv

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory
open ValuationTheory.DiscreteValuationField
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem map_maximalIdeal_ringEquiv
    {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) :
    Ideal.map e (IsLocalRing.maximalIdeal R) =
      IsLocalRing.maximalIdeal S

theorem

ramificationIdx_eq_of_map_eq

L49 ↗

RamificationTheory.ramificationIdx_eq_of_map_eq

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory
open ValuationTheory.DiscreteValuationField
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem ramificationIdx_eq_of_map_eq
    {R R' S : Type*} [CommRing R] [CommRing R'] [CommRing S]
    [Algebra R S] [Algebra R' S]
    (p : Ideal R) (q : Ideal R') (P : Ideal S)
    (h : Ideal.map (algebraMap R S) p =
      Ideal.map (algebraMap R' S) q) :
    Ideal.ramificationIdx' p P = Ideal.ramificationIdx' q P

theorem

exponentialRamificationIndex_eq_ramificationIndex_of_valuationSubrings_eq

L68 ↗

RamificationTheory.exponentialRamificationIndex_eq_ramificationIndex_of_valuationSubrings_eq

Documentation

The ramification index computed from exponential value groups agrees with the canonical ramification index of a finite complete-DVF extension when the two presentations use the same valuation subrings.

This comparison only needs the valued-extension data and the equality of the underlying valuation rings; it is independent of tameness, Henselianity, and residue-field separability.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory
open ValuationTheory.DiscreteValuationField
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem exponentialRamificationIndex_eq_ramificationIndex_of_valuationSubrings_eq
    {K : Type u} {L : Type w} [Field K] [Field L]
    [Algebra K L] [FiniteDimensional K L]
    {base : CompleteDVF.{u, v} K} {target : CompleteDVF.{w, x} L}
    [base.valuation.HasExtension target.valuation]
    (vK : LubinTate.Valuations.ExponentialValuation K)
    (vL : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, vL (algebraMap K L a) = vK a)
    (hV : LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vK =
      base.valuation.valuationSubring)
    (hW : LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vL =
      target.valuation.valuationSubring) :
    exponentialRamificationIndex vK vL =
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
        base.toDVF target.toDVF

Module documentation

Comparing exponential and canonical ramification indices

Declarations

map_maximalIdeal_ringEquiv

ramificationIdx_eq_of_map_eq

exponentialRamificationIndex_eq_ramificationIndex_of_valuationSubrings_eq