Module

FiniteIdealTameCharacter.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealTameCharacter

3 declarations indexed from sourceView source ↗

Module documentation

Tame characters on original ideal inertia

Constructs the original ideal-inertia group object, its localization comparison, and the finite tame character on that original group.

Imports5

Imported by7

def

idealInertiaGroupObject

L31 ↗

EtaleFundamentalGroups.Inertia.idealInertiaGroupObject

Documentation

The native group of original ideal inertia.

Source context 5 commands

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

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

Lean source · statement

def idealInertiaGroupObject (B : Type u) [CommRing B]
    (G : Type u) [Group G] [MulSemiringAction G B] (Q : Ideal B) : GrpCat.{u}

def

idealLocalizationInertiaGroupMap

L36 ↗

EtaleFundamentalGroups.Inertia.idealLocalizationInertiaGroupMap

Documentation

The actual original-to-local inertia comparison as a native group map.

Source context 5 commands

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

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

Lean source · statement

def idealLocalizationInertiaGroupMap
    (B : Type u) [CommRing B] (G : Type u) [Group G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] :
    Q.inertia G →*
      (IsLocalRing.maximalIdeal (Localization.AtPrime Q)).inertia (MulAction.stabilizer G Q)

def

finiteIdealTameCharacterGroupMap

L45 ↗

EtaleFundamentalGroups.Inertia.finiteIdealTameCharacterGroupMap

Documentation

The actual finite tame character on original ideal inertia. Its uniformizer and root group are constructed in the literal localization.

Source context 5 commands

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

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

Lean source · full declaration

def finiteIdealTameCharacterGroupMap
    (B : Type u) [CommRing B] [IsDedekindDomain B]
    (G : Type u) [Group G] [Finite G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) :
    letI : IsDiscreteValuationRing (Localization.AtPrime Q) :=
      SchemeTheory.localizationAtPrime_isDiscreteValuationRing B Q hQ
    idealInertiaGroupObject B G Q →*
      localTameRootsGroupObject (Localization.AtPrime Q) (MulAction.stabilizer G Q) := by
  letI : IsDiscreteValuationRing (Localization.AtPrime Q) :=
    SchemeTheory.localizationAtPrime_isDiscreteValuationRing B Q hQ
  exact (localTameCharacterGroupMap (Localization.AtPrime Q) (MulAction.stabilizer G Q)).comp
    (idealLocalizationInertiaGroupMap B G Q)

Module documentation

Tame characters on original ideal inertia

Declarations

idealInertiaGroupObject

idealLocalizationInertiaGroupMap

finiteIdealTameCharacterGroupMap