Module

FiniteIdealCanonicalTameEvaluation.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealCanonicalTameEvaluation

2 declarations indexed from sourceView source ↗

Module documentation

Uniformizer evaluation of finite ideal characters

Evaluates powers of the finite ideal tame character through uniformizer ratios, including the canonical normalized character.

Imports3

Imported by2

theorem

finiteIdealTameCharacterGroupMap_pow_eq_uniformizer

L29 ↗

EtaleFundamentalGroups.Inertia.finiteIdealTameCharacterGroupMap_pow_eq_uniformizer

Documentation

At the original prime, every power of the existing tame character is the residue of the actual ratio at any chosen uniformizer, to that same power.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
open scoped Pointwise
universe u v

Lean source · full declaration

theorem finiteIdealTameCharacterGroupMap_pow_eq_uniformizer
    (B G : Type v) [CommRing B] [IsDedekindDomain B]
    [Group G] [Finite G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) (m : ℕ)
    (π : Localization.AtPrime Q) (hπ : Irreducible π) (σ : Q.inertia G) :
    letI : IsDiscreteValuationRing (Localization.AtPrime Q) :=
      SchemeTheory.localizationAtPrime_isDiscreteValuationRing B Q hQ
    (show rootsOfUnity (finiteIdealTameOrder B G Q hQ) Q.ResidueField from
      ((finiteIdealTameCharacterGroupMap B G Q hQ).toFun σ) ^ m).val.val =
      ((IsLocalRing.residue (Localization.AtPrime Q)).toFun
        (uniformizerRatioUnit (Localization.AtPrime Q) (MulAction.stabilizer G Q) π hπ
          ⟨σ.val, Q.inertia_le_stabilizer σ.property⟩).val) ^ m := by
  let : IsDiscreteValuationRing (Localization.AtPrime Q) :=
    SchemeTheory.localizationAtPrime_isDiscreteValuationRing B Q hQ
  exact tameCharacter_pow_eq_uniformizer (Localization.AtPrime Q)
    (MulAction.stabilizer G Q) m π hπ
    ((idealLocalizationInertiaGroupMap B G Q).toFun σ)

theorem

finiteIdealCanonicalTameCharacterGroupMap_eq_uniformizer

L49 ↗

EtaleFundamentalGroups.Inertia.finiteIdealCanonicalTameCharacterGroupMap_eq_uniformizer