Module

ActualFiniteInertiaRestriction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Restriction to finite normalization inertia

Constructs the inclusion of original inertia into the ambient Galois group and its restriction to the intrinsic inertia group of a finite normalization.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteInertiaRestriction
Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationRestriction
Nyll.EtaleFundamentalGroups.Inertia.CommAlgInertiaRestriction
Mathlib.Algebra.Category.Grp.Basic

Imported by16

def

actualNormalizationInertiaInclusion

L35 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationInertiaInclusion

Documentation

The actual original inertia includes into the original ambient group.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
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 actualNormalizationInertiaInclusion (Q : Ideal (integralClosure A L)) :
    GrpCat.Hom (actualNormalizationInertiaGroup A K L Q) (galoisGroupObject K L) where
  hom' := (Q.inertia Gal(L/K)).subtype

def

actualFiniteInertiaCoefficientMap

L40 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaCoefficientMap

Documentation

The prescribed finite coefficient automorphism map on actual original inertia.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
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 actualFiniteInertiaCoefficientMap (Q : Ideal (integralClosure A L))
    (E : FiniteGaloisIntermediateField K L) :
    GrpCat.Hom (actualNormalizationInertiaGroup A K L Q)
      (commAlgAutomorphismGroup A (finiteAbsoluteNormalizationAlgebra A K L E)) where
  hom' := (actualFiniteNormalizationRestriction A K L E).hom'.comp
    (actualNormalizationInertiaInclusion A K L Q).hom'

def