Module

ActualFiniteRootsGroupMap.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteRootsGroupMap

1 declaration indexed from sourceView source ↗

Module documentation

Finite residue roots in the ambient field

Constructs the homomorphism from finite tame-degree residue roots into roots of the same degree in the original ambient residue field.

Imports6

Imported by6

def

actualFiniteRootsGroupMap

L31 ↗

EtaleFundamentalGroups.Inertia.actualFiniteRootsGroupMap

Documentation

The actual tame-degree root group at a finite prime embeds into the same-degree root group of the original ambient residue field.

Source context 4 commands

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

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

Lean source · statement

def actualFiniteRootsGroupMap
    (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 (SchemeTheory.normalizationCommAlgCat A L)) [Q.IsMaximal]
    (E : FiniteGaloisIntermediateField K L) :
    actualFiniteStageTameRootsGroup A K L Q E ⟶
      normalizationRootsGroup A L Q (actualFiniteStageTameOrder A K L Q E)

Module documentation

Finite residue roots in the ambient field

Declarations

actualFiniteRootsGroupMap