NYLL
Module

DVRRootsOfUnity.lean

Nyll.EtaleFundamentalGroups.Kummer.PureRadical.DVRRootsOfUnity
2 declarations indexed from sourceView source ↗

Module documentation

Roots of unity in a tame pure-radical DVR extension

This file supplies the non-Henselian roots-of-unity input in the DVR form of Stacks Project, Lemma 15.115.6 (tag 09EV). If a uniformizer acquires an n-th root and n is a unit in the base DVR, then every n-th root of unity in the resulting pure-radical field already belongs to the base fraction field.

The proof uses the canonical power-basis normal form in the root algebra. A nonzero element with zero constant coefficient has uniformizer order not divisible by n. Applying this to the nonconstant part of a root of unity, the linear term of the binomial expansion has the same order, whereas the whole expression comes from the base DVR and hence has order divisible by n, a contradiction.

Imports4
Imported by2

Declarations

theorem

exists_add_pow_sub_pow_eq_linear_add_sq_mul

L37 ↗
EtaleFundamentalGroups.Kummer.exists_add_pow_sub_pow_eq_linear_add_sq_mul
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w
Lean source · statement
theorem exists_add_pow_sub_pow_eq_linear_add_sq_mul
    {R : Type u} [CommRing R] (x y : R) (n : ℕ) (hn : 0 < n) :
    ∃ q : R,
      (x + y) ^ n - x ^ n =
        (n : R) * x ^ (n - 1) * y + y ^ 2 * q
theorem

rootOfUnity_mem_fractionBase_of_dvr_pureRadical

L63 ↗
EtaleFundamentalGroups.Kummer.rootOfUnity_mem_fractionBase_of_dvr_pureRadical
Documentation

In a tame pure-uniformizer extension of DVR fraction fields, every root of unity whose order divides the radical degree descends to the base field.

All hypotheses are source data of the pure-radical presentation. In particular, no Henselian or roots-of-unity descent assumption is used.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w
Lean source · statement
theorem rootOfUnity_mem_fractionBase_of_dvr_pureRadical
    {V : Type u} {K : Type v} {L : Type w}
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Field L]
    [Algebra V K] [IsFractionRing V K]
    [Algebra K L] [Algebra V L] [IsScalarTower V K L]
    [FiniteDimensional K L]
    {n : ℕ} (hn : 0 < n) (hnUnit : IsUnit (n : V))
    (pi : V) (hpi : Prime pi)
    (alpha : L)
    (hdegree : Module.finrank K L = n)
    (halphaPow : alpha ^ n = algebraMap K L (algebraMap V K pi))
    (hgen : IntermediateField.adjoin K {alpha} = ⊤)
    (zeta : L) (hzetaPow : zeta ^ n = 1) :
    zeta ∈ Set.range (algebraMap K L)

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