Module

ActualFiniteCanonicalTameMorphism.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteCanonicalTameMorphism

1 declaration indexed from sourceView source ↗

Module documentation

Canonical tame morphisms at finite stages

Constructs the canonical tame morphism from finite normalization inertia to its residue-root group using the original DVR, Galois extension, and chosen prime.

Imports7

Imported by6

def

actualFiniteCanonicalTameMorphism

L32 ↗

EtaleFundamentalGroups.Inertia.actualFiniteCanonicalTameMorphism

Documentation

The actual canonical finite character constructed solely from the original DVR, Galois extension, chosen normalization prime, and finite Galois level.

Source context 4 commands

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

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

Lean source · statement

def actualFiniteCanonicalTameMorphism
    (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) :
    actualFiniteStageInertiaGroup A K L Q E ⟶ actualFiniteStageTameRootsGroup A K L Q E

Module documentation

Canonical tame morphisms at finite stages

Declarations

actualFiniteCanonicalTameMorphism