NYLL
Module

FiniteIdealCanonicalTameCharacter.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealCanonicalTameCharacter
2 declarations indexed from sourceView source ↗

Module documentation

Normalized tame characters at finite ideals

Defines the ramification-index-to-tame-order normalization exponent and the resulting canonical character on finite ideal inertia.

Imports4
Imported by8

Declarations

def

finiteIdealNormalizationExponent

L30 ↗
EtaleFundamentalGroups.Inertia.finiteIdealNormalizationExponent
Documentation

The actual original-prime e/n normalization exponent.

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 v
Lean source · statement
def finiteIdealNormalizationExponent
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [IsDedekindDomain B]
    [Algebra A B] (G : Type v) [Group G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) : ℕ
def

finiteIdealCanonicalTameCharacterGroupMap

L38 ↗
EtaleFundamentalGroups.Inertia.finiteIdealCanonicalTameCharacterGroupMap
Documentation

The canonical e/n-normalized character of the actual original finite ideal inertia, taking values in its full actual root group.

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 v
Lean source · full declaration
def finiteIdealCanonicalTameCharacterGroupMap
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [IsDedekindDomain B]
    [Algebra A B] (G : Type v) [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 (localTameRootsPowerGroupMap (Localization.AtPrime Q) (MulAction.stabilizer G Q)
    (finiteIdealNormalizationExponent A B G Q hQ)).comp
      (finiteIdealTameCharacterGroupMap B G Q hQ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.