Module

Relative.lean

Nyll.EtaleFundamentalGroups.Kummer.Radicals.Relative

1 declaration indexed from sourceView source ↗

Module documentation

A Kummer radical relative to a faithfully flat prefix

This file treats the final stage of an iterated radical construction. If T is faithfully flat over A, formal unramifiedness of the radical over A restricts to formal unramifiedness over T. The explicit derivative calculation then makes the exponent a unit in T, and faithful flatness reflects that unit back to A.

AdjoinRoot already supplies the direct A-algebra structure and the scalar tower through T, so no competing local algebra instances are installed.

Imports2

Imported by3

theorem

isUnit_natCast_of_formallyUnramified_relativeRadical

L38 ↗

EtaleFundamentalGroups.Kummer.isUnit_natCast_of_formallyUnramified_relativeRadical

Documentation

For a Kummer radical over a faithfully flat A-algebra T, formal unramifiedness over A forces its positive exponent to be a unit in A. The radicand may be any element of T; no unit or descent hypothesis on it is needed for this direction.

Taking T to be the algebra obtained from all preceding radicals gives the last-exponent step for an iterated Kummer construction.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v

Lean source · statement

theorem isUnit_natCast_of_formallyUnramified_relativeRadical
    {A : Type u} {T : Type v}
    [CommRing A] [CommRing T] [Algebra A T]
    [Nontrivial T] [Module.FaithfullyFlat A T]
    {a : T} {n : ℕ} (hn : 0 < n)
    [Algebra.FormallyUnramified A
      (AdjoinRoot (X ^ n - C a))] :
    IsUnit (n : A)

Module documentation

A Kummer radical relative to a faithfully flat prefix

Declarations

isUnit_natCast_of_formallyUnramified_relativeRadical