Module

DVRRamificationOrder.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DVRRamificationOrder

2 declarations indexed from sourceView source ↗

Module documentation

Ramification indices as uniformizer orders

Identifies both ideal ramification-index conventions with the additive valuation of a mapped base uniformizer for an injective map of discrete valuation rings.

Imports4

Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.RamificationInertia.Ramification
Mathlib.NumberTheory.RamificationInertia.Ramification
Mathlib.RingTheory.Ideal.Span

Imported by3

theorem

ramificationIdx'_eq_addVal_uniformizer

L31 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.ramificationIdx'_eq_addVal_uniformizer

Documentation

The literal maximal-ideal ramification index is the additive order of the actual mapped base uniformizer. The comparison uses no group or residue field.

Source context 6 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (A : Type u) (B : Type v)
variable [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
variable [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B]

Lean source · statement

theorem ramificationIdx'_eq_addVal_uniformizer
    (hinj : Function.Injective (algebraMap A B)) (π : A) (hπ : Irreducible π) :
    Ideal.ramificationIdx' (maximalIdeal A) (maximalIdeal B) =
      (IsDiscreteValuationRing.addVal B (algebraMap A B π)).toNat

theorem

ramificationIdx_eq_addVal_uniformizer

L54 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.ramificationIdx_eq_addVal_uniformizer