Module

StandardEtaleLifting.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.StandardEtaleLifting

2 declarations indexed from sourceView source ↗

Module documentation

Lifting points of standard étale algebras

The simple-root condition for a Henselian pair lifts a residue point of a standard étale algebra to the base ring. The defining monic polynomial and its derivative condition supply the Hensel input, and the Jacobson condition makes the localization denominator invertible at the lifted root.

Imports2

Mathlib.RingTheory.Henselian
Mathlib.RingTheory.Etale.StandardEtale

Imported by2

theorem

exists_standardEtale_lift

L25 ↗

ValuationTheory.Henselian.exists_standardEtale_lift

Documentation

A point of a standard étale algebra modulo a Henselian ideal lifts to a point over the original ring.

Source context 2 commands

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

namespace ValuationTheory.Henselian
variable {R : Type*} [CommRing R] {I : Ideal R} [HenselianRing R I]

Lean source · statement

theorem exists_standardEtale_lift
    (P : StandardEtalePair R) (σ : P.Ring →ₐ[R] R ⧸ I) :
    ∃ τ : P.Ring →ₐ[R] R, (Ideal.Quotient.mkₐ R I).comp τ = σ

theorem

exists_isStandardEtale_lift

L59 ↗

ValuationTheory.Henselian.exists_isStandardEtale_lift