Nyll.EtaleFundamentalGroups.Inertia.AbsoluteNormalizationRadicalStage

Module documentation

The actual finite-normalization radical stage of the absolute DVR argument

The ambient radical producer chooses the finite Galois field and uniformizer. Its literal membership and proved integrality construct the root in the native finite normalization. The original power equation is retained using the stored coefficient map, with no finite-field scalar action opened here.

theorem

exists_finiteAbsoluteNormalization_uniformizer_radical

L30 ↗

EtaleFundamentalGroups.Inertia.exists_finiteAbsoluteNormalization_uniformizer_radical

Documentation

Every invertible exponent occurs as a uniformizer radical in the actual normalization of a finite Galois subextension of the given separable closure.

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 exists_finiteAbsoluteNormalization_uniformizer_radical
    (A : Type u) (K : Type v) (Ω : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
    [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
    (n : ℕ) (hn : IsUnit (n : A)) :
    ∃ (E : FiniteGaloisIntermediateField K Ω) (π : A)
      (γ : finiteAbsoluteNormalizationAlgebra A K Ω E),
      Irreducible π ∧ γ ^ n =
        commAlgCoefficientMap (finiteAbsoluteNormalizationAlgebra A K Ω E) π

Module documentation

The actual finite-normalization radical stage of the absolute DVR argument

Declarations

exists_finiteAbsoluteNormalization_uniformizer_radical