Module

HenselianNilIdeal.lean

Nyll.SchemeTheory.RingTheory.HenselianNilIdeal

2 declarations indexed from sourceView source ↗

Module documentation

Henselian pairs defined by nil ideals

For a polynomial with an approximate simple root modulo a nil ideal, its initial error generates a nilpotent principal ideal. The adic filtration for this smaller ideal terminates, so completeness supplies a root whose correction lies in the original ideal. The original nil ideal need not be nilpotent.

Imports7

Mathlib.LinearAlgebra.SModEq.Basic
Mathlib.RingTheory.AdicCompletion.Basic
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.Jacobson.Ideal
Mathlib.RingTheory.Nilpotent.Lemmas

Imported by2

theorem

isAdicComplete_of_pow_eq_bot

L32 ↗

HenselianRing.isAdicComplete_of_pow_eq_bot

Source context 3 commands

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

@[expose] public section
universe u
namespace HenselianRing

Lean source · full declaration

theorem isAdicComplete_of_pow_eq_bot
    {R : Type u} [CommRing R] (J : Ideal R) (n : ℕ) (hn : J ^ n = ⊥) :
    IsAdicComplete J R where
  haus' x hx := by
    simpa only [Ideal.smul_eq_mul, Ideal.mul_top, hn, SModEq.bot] using hx n
  prec' f hf := by
    refine ⟨f n, fun m ↦ ?_⟩
    obtain hmn | hnm := le_total m n
    · exact hf hmn
    · have h : f n = f m := by
        simpa only [Ideal.smul_eq_mul, Ideal.mul_top, hn, SModEq.bot] using hf hnm
      rw [h]

theorem

of_le_nilradical

L47 ↗

HenselianRing.of_le_nilradical

Documentation

Every nil ideal defines a Henselian pair. No uniform nilpotence exponent for the ideal is required.