NYLL
Module

HenselianIntegral.lean

Nyll.SchemeTheory.RingTheory.HenselianIntegral
1 declaration indexed from sourceView source ↗

Module documentation

Henselian pairs under integral extension

For a monic polynomial with an approximate simple root, the standard étale algebra obtained by inverting its derivative has a section over the quotient. The integral-base section theorem lifts that section and hence the root. This proves Henselian ascent without a finiteness or locality hypothesis.

Imports4
Imported by1

Declarations

theorem

of_isIntegral

L33 ↗
HenselianRing.of_isIntegral
Documentation

Integral extension preserves Henselian pairs. The integral algebra need not be finite as a module, local, or complete.

Source context 4 commands

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

@[expose] public section
open Polynomial
universe u
namespace HenselianRing
Lean source · statement
theorem of_isIntegral
    {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
    [Algebra.IsIntegral R B] (I : Ideal R) [HenselianRing R I] :
    HenselianRing B (I.map (algebraMap R B))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.