Module

ActualFiniteTameCoordinate.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameCoordinate

1 declaration indexed from sourceView source ↗

Module documentation

Finite coordinates of the canonical tame character

Constructs the ambient residue-root coordinate on original inertia by composing finite restriction, the canonical tame character, and residue embedding.

Imports8

Imported by13

def

actualFiniteTameCoordinate

L34 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate

Documentation

The actual finite coordinate of the canonical tame character on the original inertia group. Restriction, the canonical e/n character, and the residue embedding are all constructed from the original data.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory SchemeTheory
universe u v w

Lean source · statement

def actualFiniteTameCoordinate
    (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]
    (E : FiniteGaloisIntermediateField K L) :
    actualNormalizationInertiaGroup A K L Q ⟶
      normalizationRootsGroup A L Q (actualFiniteStageTameOrder A K L Q E)

Module documentation

Finite coordinates of the canonical tame character

Declarations

actualFiniteTameCoordinate