Module

Field.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.Field

2 declarations indexed from sourceView source ↗

Module documentation

Cyclic tame inertia for exponential valuations

This file is the field-valued entry point for the DVR cyclicity theorem. A discrete production ExponentialValuation supplies a discrete valuation ring, so cyclicity follows directly from the valuation-subring theorem in CyclicInertia.Ideal.

Imports2

Imported by1

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.All

theorem

discreteExponentialValuation_inertiaGroup_isCyclic_of_card_coprime_ringExpChar

L30 ↗

TameAbhyankar.SGA1.discreteExponentialValuation_inertiaGroup_isCyclic_of_card_coprime_ringExpChar

Documentation

The inertia group attached to a discrete exponential valuation is cyclic when its order is prime to the exponential residue characteristic.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem discreteExponentialValuation_inertiaGroup_isCyclic_of_card_coprime_ringExpChar
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hw : LubinTate.Valuations.DiscreteExponentialValuation w)
    [Finite (inertiaGroup K
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring w))]
    (hcop : Nat.Coprime
      (Nat.card (inertiaGroup K
        (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring w)))
      (ringExpChar (IsLocalRing.ResidueField
        (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring w)))) :
    IsCyclic (inertiaGroup K
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring w))

theorem

discreteExponentialValuation_maximalIdealInertia_isCyclic_of_card_coprime_ringExpChar

L55 ↗

TameAbhyankar.SGA1.discreteExponentialValuation_maximalIdealInertia_isCyclic_of_card_coprime_ringExpChar