Module

EtaleDerivative.lean

Nyll.EtaleFundamentalGroups.Kummer.Obstructions.EtaleDerivative

1 declaration indexed from sourceView source ↗

Module documentation

The derivative criterion for a monogenic etale algebra

For an adjoined-root algebra, formal unramifiedness forces the derivative of the defining polynomial at the distinguished root to be a unit. The proof descends the usual polynomial derivative to the quotient by the derivative value. This descended derivation sends the distinguished root to one, while formal unramifiedness says that every such derivation is zero.

Imports2

Mathlib.RingTheory.Unramified.Basic
Mathlib.Algebra.Polynomial.Derivation

Imported by4

theorem

isUnit_aeval_derivative_of_formallyUnramified

L32 ↗

EtaleFundamentalGroups.Kummer.isUnit_aeval_derivative_of_formallyUnramified

Documentation

If AdjoinRoot f is formally unramified over its coefficient ring, then the derivative of f at the distinguished root is a unit.

No monicity hypothesis is needed for this direction.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem isUnit_aeval_derivative_of_formallyUnramified
    {R : Type u} [CommRing R] (f : R[X])
    [Algebra.FormallyUnramified R (AdjoinRoot f)] :
    IsUnit (aeval (AdjoinRoot.root f) f.derivative)

Module documentation

The derivative criterion for a monogenic etale algebra

Declarations

isUnit_aeval_derivative_of_formallyUnramified