Module

ActualFiniteInertiaRestrictionConjugate.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaRestrictionConjugate

1 declaration indexed from sourceView source ↗

Module documentation

Actual finite restriction preserves original conjugation

Both restrictions project to the same constructed normalization ring map. The group calculation is closed in its sparse full-Galois owner before the four original and finite D/I groups occur together.

Imports6

Imported by2

theorem

actualFiniteInertiaRestriction_conjugate

L28 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaRestriction_conjugate

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · statement

theorem actualFiniteInertiaRestriction_conjugate
    (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]
    (Q : Ideal (normalizationCommAlgCat A L).carrier)
    (E : FiniteGaloisIntermediateField K L)
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    (actualFiniteInertiaRestriction A K L Q E).hom'.toFun
        (originalFiniteNormalizationInertiaConjugate A K L Q d σ) =
      commAlgIdealInertiaConjugate A (finiteAbsoluteNormalizationAlgebra A K L E)
        (finiteAbsoluteNormalizationPrime A K L Q E)
        ((actualFiniteDecompositionRestriction A K L Q E).hom'.toFun d)
        ((actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ)

Module documentation

Actual finite restriction preserves original conjugation

Declarations

actualFiniteInertiaRestriction_conjugate