Module

ActualFiniteNormalizationTowerAction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationTowerAction

1 declaration indexed from sourceView source ↗

Module documentation

Galois action on finite normalization towers

Proves that the two restricted Galois automorphisms commute with the inclusion between nested finite normalizations.

Imports4

Imported by5

theorem

actualFiniteNormalizationTowerRingMap_action

L32 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationTowerRingMap_action

Documentation

The two actual restricted automorphisms commute with the literal finite normalization tower inclusion. The equation follows from their already proved original ambient inclusion squares.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L]

Lean source · statement

theorem actualFiniteNormalizationTowerRingMap_action
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) (σ : Gal(L/K)) :
    (actualFiniteNormalizationTowerRingMap A K L E F h).comp
        (actualFiniteNormalizationRestrictionRingHom A K L E σ) =
      (actualFiniteNormalizationRestrictionRingHom A K L F σ).comp
        (actualFiniteNormalizationTowerRingMap A K L E F h)

Module documentation

Galois action on finite normalization towers

Declarations

actualFiniteNormalizationTowerRingMap_action