Module

OriginalFiniteNormalizationInertiaConjugateMap.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteNormalizationInertiaConjugateMap

1 declaration indexed from sourceView source ↗

Module documentation

Conjugation compatibility of normalization restriction

Proves that normalization restriction intertwines original finite-field inertia conjugation with intrinsic normalization inertia conjugation.

Imports10

Imported by2

theorem

originalFiniteNormalizationInertiaConjugate_map

L35 ↗

EtaleFundamentalGroups.Inertia.originalFiniteNormalizationInertiaConjugate_map

Documentation

The actual normalization restriction intertwines the native original and intrinsic inertia conjugates. Both ambient actions remain in their owners.

Source context 4 commands

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

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

Lean source · statement

theorem originalFiniteNormalizationInertiaConjugate_map
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F))
    (d : normalizationDecompositionGroup A K F Q)
    (σ : actualNormalizationInertiaGroup A K F Q) :
    (originalFiniteNormalizationInertiaMorphism A K F Q).hom'.toFun
        (originalFiniteNormalizationInertiaConjugate A K F Q d σ) =
      commAlgIdealInertiaConjugate A (normalizationCommAlgCat A F) Q
        ((originalFiniteNormalizationDecompositionMorphism A K F Q).hom'.toFun d)
        ((originalFiniteNormalizationInertiaMorphism A K F Q).hom'.toFun σ)

Module documentation

Conjugation compatibility of normalization restriction

Declarations

originalFiniteNormalizationInertiaConjugate_map