NYLL
Module

AbsoluteUniformizerAmbient.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteUniformizerAmbient
2 declarations indexed from sourceView source ↗

Module documentation

An actual finite Galois uniformizer radical in the ambient separable closure

The established finite-field radical construction is exposed through its literal ambient element and finite-level membership. The later native normalization owner can consume this without opening the finite field's scalar actions alongside the original absolute prime.

Reference: Stacks Project, Tag 0BUB. https://stacks.math.columbia.edu/tag/0BUB

Imports2
Imported by2

Declarations

theorem

exists_finiteGalois_ambient_radical

L30 ↗
EtaleFundamentalGroups.Inertia.exists_finiteGalois_ambient_radical
Documentation

Retain the actual finite-field radical as an ambient element together with its literal finite-level membership.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem exists_finiteGalois_ambient_radical
    (K : Type v) (Ω : Type w) [Field K] [Field Ω]
    [Algebra K Ω] [IsSepClosure K Ω]
    (n : ℕ) (hn : (n : K) ≠ 0) (a : K) :
    ∃ (E : FiniteGaloisIntermediateField K Ω) (α : Ω),
      α ∈ E.toIntermediateField ∧ α ^ n = algebraMap K Ω a
theorem

exists_finiteGalois_ambient_uniformizer_radical

L43 ↗
EtaleFundamentalGroups.Inertia.exists_finiteGalois_ambient_uniformizer_radical
Documentation

The original DVR and its actual separable closure produce a nonzero integral uniformizer radical in an actual finite Galois level. Only the ambient scalar actions occur in this endpoint.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem exists_finiteGalois_ambient_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) (α : Ω),
      Irreducible π ∧ α ≠ 0 ∧ α ∈ E.toIntermediateField ∧
        IsIntegral A α ∧ α ^ n = algebraMap A Ω π

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.