Module

FormallyEtale.lean

Nyll.EtaleFundamentalGroups.Kummer.AdjoinRoot.FormallyEtale

2 declarations indexed from sourceView source ↗

Module documentation

Formal etaleness of an explicit adjoined root

A monic equation whose derivative is a unit at its adjoined root is formally etale. Choosing the derivative itself as the denominator in a standard etale presentation makes the Bezout condition tautological; localization at that denominator then disappears because it is already a unit.

Imports2

Mathlib.RingTheory.Etale.StandardEtale
Nyll.EtaleFundamentalGroups.Kummer.Radicals.Explicit

Imported by9

theorem

formallyEtale_adjoinRoot_of_monic_of_isUnit_aeval_derivative

L31 ↗

EtaleFundamentalGroups.Kummer.formallyEtale_adjoinRoot_of_monic_of_isUnit_aeval_derivative

Documentation

If a monic polynomial has unit derivative at its adjoined root, then its adjoined-root algebra is formally etale.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem formallyEtale_adjoinRoot_of_monic_of_isUnit_aeval_derivative
    {A : Type u} [CommRing A] {f : A[X]} (hf : f.Monic)
    (hDerivative : IsUnit (aeval (AdjoinRoot.root f) f.derivative)) :
    Algebra.FormallyEtale A (AdjoinRoot f)

theorem

formallyEtale_adjoinRoot_X_pow_sub_C

L61 ↗

EtaleFundamentalGroups.Kummer.formallyEtale_adjoinRoot_X_pow_sub_C