Module

AbsoluteUniformizerRadical.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteUniformizerRadical

2 declarations indexed from sourceView source ↗

Module documentation

Finite Galois radicals inside the prescribed separable closure

The finite field is the normal closure of the field generated by an actual root. A separate integral-closure owner constructs the integral radical from its equation, without mixing the ambient separable closure or prime localization into that construction.

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

Imports3

Mathlib.FieldTheory.Galois.GaloisClosure
Mathlib.FieldTheory.IsSepClosed
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Imported by2

theorem

exists_finiteGalois_radical

L31 ↗

EtaleFundamentalGroups.Inertia.exists_finiteGalois_radical

Documentation

An actual prime-to-characteristic radical lies in a concrete finite Galois subextension of the prescribed separable closure.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem exists_finiteGalois_radical
    (K : Type u) (Ω : Type v) [Field K] [Field Ω]
    [Algebra K Ω] [IsSepClosure K Ω]
    (n : ℕ) (hn : (n : K) ≠ 0) (a : K) :
    ∃ (E : FiniteGaloisIntermediateField K Ω) (β : E),
      β ^ n = algebraMap K E a

theorem

exists_integralClosure_radical_of_pow_eq

L54 ↗

EtaleFundamentalGroups.Inertia.exists_integralClosure_radical_of_pow_eq