Module

ActualFiniteNormalizationRestriction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationRestriction

2 declarations indexed from sourceView source ↗

Module documentation

Galois restriction on finite normalizations

Constructs the finite Galois action on its normalization and the homomorphism restricting ambient Galois automorphisms to those coefficient automorphisms.

Imports6

Imported by8

def

finiteNormalizationGaloisGroupMap

L35 ↗

EtaleFundamentalGroups.Inertia.finiteNormalizationGaloisGroupMap

Documentation

The actual finite Galois action on its literal native normalization.

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] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]

Lean source · full declaration

def finiteNormalizationGaloisGroupMap (E : FiniteGaloisIntermediateField K L) :
    GrpCat.Hom (finiteGaloisGroupObject K L E)
      (commAlgAutomorphismGroup A (finiteAbsoluteNormalizationAlgebra A K L E)) where
  hom' := (normalizationAutomorphismGroupMap A (finiteLevelFieldAlgebra A K L E)).hom'.comp
    (scalarRestrictionGroupMap A K (finiteLevelFieldAlgebra A K L E)).hom'

def