Nyll.EtaleFundamentalGroups.Kummer.PureRadical.HeightOneRootsOfUnity

Module documentation

Roots of unity at a prime boundary parameter

This is the height-one input consumed by the one-divisor Abhyankar argument. Localizing a Noetherian domain at the principal prime generated by t produces a DVR whose uniformizer is the image of t. Characteristic zero on the boundary residue field makes the pure-radical degree a unit in that DVR, so the DVR roots-of-unity descent theorem applies.

theorem

rootOfUnity_mem_fractionBase_of_primeParameter_pureRadical

L33 ↗

EtaleFundamentalGroups.Kummer.rootOfUnity_mem_fractionBase_of_primeParameter_pureRadical

Documentation

Every root of unity of the radical degree in a pure prime-parameter extension already belongs to the base fraction field.

The DVR, its uniformizer, and unitness of the degree are all produced inside the proof. No regularity, Henselianity, or roots-of-unity hypothesis is assumed.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u v w

Lean source · statement

theorem rootOfUnity_mem_fractionBase_of_primeParameter_pureRadical
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L]
    {t : A} (ht : Prime t)
    (hCharZero : CharZero (A ⧸ Ideal.span {t}))
    (alpha : L)
    (halphaPow : alpha ^ Module.finrank K L =
      algebraMap K L (algebraMap A K t))
    (hgen : IntermediateField.adjoin K {alpha} = ⊤)
    (zeta : L) (hzetaPow : zeta ^ Module.finrank K L = 1) :
    zeta ∈ Set.range (algebraMap K L)

Module documentation

Roots of unity at a prime boundary parameter

Declarations

rootOfUnity_mem_fractionBase_of_primeParameter_pureRadical