Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaTowerCoefficient

Module documentation

Literal coefficients of finite inertia restriction

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

theorem

actualFiniteInertiaTowerRestriction_coefficient

L34 ↗

EtaleFundamentalGroups.Inertia.actualFiniteInertiaTowerRestriction_coefficient

Documentation

The canonical finite inertia 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 actualFiniteInertiaTowerRestriction_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)
    (τ : (commAlgIdealInertiaGroup 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)
          ((actualFiniteInertiaTowerRestriction 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 inertia restriction

Declarations

actualFiniteInertiaTowerRestriction_coefficient