Module

RelativeRadical.lean

Nyll.EtaleFundamentalGroups.Kummer.Descent.RelativeRadical

1 declaration indexed from sourceView source ↗

Module documentation

Descent through a relative Kummer radical

For the final stage of a relative Kummer construction, formal unramifiedness over the prefix makes the derivative a unit. Monicity then makes the final stage formally etale. Its positive-degree monic presentation is faithfully flat, so formal unramifiedness descends to the prefix.

All algebra structures and scalar towers below are the canonical instances provided by AdjoinRoot.

Imports3

Imported by3

theorem

formallyUnramified_prefix_of_formallyUnramified_relativeRadical

L34 ↗

EtaleFundamentalGroups.Kummer.formallyUnramified_prefix_of_formallyUnramified_relativeRadical

Documentation

If the total relative Kummer algebra is formally unramified over the original base, then its prefix is formally unramified too.

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 formallyUnramified_prefix_of_formallyUnramified_relativeRadical
    {A : Type u} {T : Type v}
    [CommRing A] [CommRing T] [Algebra A T]
    [Nontrivial T]
    {a : T} {n : ℕ} (hn : 0 < n)
    [Algebra.FormallyUnramified A
      (AdjoinRoot (X ^ n - C a))] :
    Algebra.FormallyUnramified A T

Module documentation

Descent through a relative Kummer radical

Declarations

formallyUnramified_prefix_of_formallyUnramified_relativeRadical