Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteDecompositionTowerCoefficient

Module documentation

Literal coefficients of finite decomposition restriction

The constructed finite decomposition restriction is the literal restriction of coefficient automorphisms along the actual finite normalization inclusion. Its square follows from an actual original decomposition lift and the existing normalization action square.

theorem

actualFiniteDecompositionTowerRestriction_coefficient

L34 ↗

EtaleFundamentalGroups.Inertia.actualFiniteDecompositionTowerRestriction_coefficient

Documentation

The canonical finite decomposition map restricts actual coefficient automorphisms along the literal finite normalization inclusion.

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 actualFiniteDecompositionTowerRestriction_coefficient
    (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) [hQ : Q.IsPrime]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F)
    (τ : (commAlgIdealDecompositionGroup A (finiteAbsoluteNormalizationAlgebra A K L F)
      (finiteAbsoluteNormalizationPrime A K L Q F)).carrier) :
    (actualFiniteNormalizationTowerRingMap A K L E F h).comp
        (commAlgAutomorphismRingHom A (finiteAbsoluteNormalizationAlgebra A K L E)
          ((actualFiniteDecompositionTowerRestriction A K L Q E F h).hom'.toFun τ).val) =
      (commAlgAutomorphismRingHom A (finiteAbsoluteNormalizationAlgebra A K L F) τ.val).comp
        (actualFiniteNormalizationTowerRingMap A K L E F h)

Module documentation

Literal coefficients of finite decomposition restriction

Declarations

actualFiniteDecompositionTowerRestriction_coefficient