Module

IntermediateField.lean

Nyll.EtaleFundamentalGroups.Kummer.PureRadical.IntermediateField

2 declarations indexed from sourceView source ↗

Module documentation

Intermediate fields of a pure radical extension

Let L = K(α) be finite, put e = [L : K], and suppose that α ^ e belongs to K. If every e-th root of unity in L already belongs to K, then every intermediate field F is generated by α ^ [L : F]. In particular, its exponent divides e.

The proof uses the relative norm from L to F. The quotient N_{L/F}(α) / α ^ [L : F] is an e-th root of unity, so the root-of-unity hypothesis puts it in the base field and shows that α ^ [L : F] belongs to F. The reverse inclusion follows from a minimal-polynomial degree comparison.

This is the field-theoretic core of Stacks Project, Lemma 15.115.4 (tag 0EXP), used in the DVR pure-radical classification of tag 09EV.

Imports2

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.RingTheory.Norm.Basic

Imported by2

theorem

intermediateField_eq_adjoin_pow_finrank_of_pureRadical

L40 ↗

EtaleFundamentalGroups.Kummer.intermediateField_eq_adjoin_pow_finrank_of_pureRadical

Documentation

An intermediate field of a pure radical extension is generated by the power whose exponent is its relative degree.

This is the abstract field-theoretic core of Stacks tag 0EXP.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v

Lean source · statement

theorem intermediateField_eq_adjoin_pow_finrank_of_pureRadical
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (α : L) (hα : α ≠ 0)
    (hpow : α ^ Module.finrank K L ∈ Set.range (algebraMap K L))
    (hgen : IntermediateField.adjoin K {α} = ⊤)
    (hroots : ∀ ζ : L, ζ ^ Module.finrank K L = 1 →
      ζ ∈ Set.range (algebraMap K L))
    (F : IntermediateField K L) :
    F = IntermediateField.adjoin K {α ^ Module.finrank F L}

theorem

exists_intermediateField_eq_adjoin_pow_of_pureRadical

L136 ↗

EtaleFundamentalGroups.Kummer.exists_intermediateField_eq_adjoin_pow_of_pureRadical