Module

ActualFiniteTameNormalizationMap.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameNormalizationMap

2 declarations indexed from sourceView source ↗

Module documentation

Power normalization of finite tame values

Defines the ambient residue power map with exponent given by the ramification index divided by the tame order, and factors the canonical coordinate through it.

Imports7

Imported by4

def

actualFiniteTameNormalizationMap

L39 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameNormalizationMap

Documentation

The actual e/n normalization is the standard power endomorphism of the ambient residue monoid. It is constructed from the original index/order and is independent of any inertia element or character value.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]

Lean source · statement

def actualFiniteTameNormalizationMap (E : FiniteGaloisIntermediateField K L) :
    Q.ResidueField →* Q.ResidueField

theorem

actualFiniteTameCoordinate_eq_normalizationMap

L47 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate_eq_normalizationMap