Conormal injectivity for a regular local quotient

Proved

RegularLocalConormal.inf_maximalIdeal_sq_eq_mul

by tomasz · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

commutative-algebraphilippon-multiplicityproof-frontierregular-local-rings

Let $(R,\mathfrak m)$ be a commutative regular local ring and let $I\subseteq R$ be an ideal such that $R/I$ is also a regular local ring. Then

I\cap\mathfrak m^2=\mathfrak m I.

Equivalently, the natural map $I/\mathfrak m I\longrightarrow\mathfrak m/\mathfrak m^2$ is injective. Thus a relation in $I$ whose first-order class vanishes already belongs to $\mathfrak m I$ .

This is the conormal injectivity consequence of the theorem that the kernel of a regular quotient of a regular local ring is generated by part of a minimal system of generators of the maximal ideal. It has no polynomial, geometric, characteristic, or residue-field restriction. The case $I=0$ is included.

Formalization Note. The complete Lean proof uses Nakayama to compare the minimal numbers of generators under a surjection whose kernel lies in the maximal-ideal square. A dimension drop in a domain makes such a kernel zero when both rings are regular. Induction then passes through quotients by parameters and lifts the conormal equality back. The actual proofs of regular-local domainhood and parameter-quotient regularity are included in the submission. There are no Open theorem dependencies, and the original formal statement is unchanged.

Preamble

import Mathlib
set_option autoImplicit false

Formal statement

namespace RegularLocalConormal

theorem inf_maximalIdeal_sq_eq_mul
    (R : Type*) [CommRing R] [IsRegularLocalRing R]
    (I : Ideal R) [IsRegularLocalRing (R ⧸ I)] :
    I ⊓ (IsLocalRing.maximalIdeal R) ^ 2 = IsLocalRing.maximalIdeal R * I := by sorry

end RegularLocalConormal

Source

Stacks Project, Lemma 10.106.4 (Tag 00NR), https://stacks.math.columbia.edu/tag/00NR : for a regular local ring with regular quotient, the kernel is generated by a subset of a minimal system of generators of the maximal ideal. The conormal-injectivity consequence is explicitly used in the proof of Lemma 10.135.6 (Tag 00SE), https://stacks.math.columbia.edu/tag/00SE , in the paragraph containing J/mJ -> I/mI -> m/m^2, where the composition is declared injective by Lemma 10.106.4 and its proof. The present ideal equality is exactly that injectivity assertion for the kernel J, renamed I. No hypotheses about a third quotient or complete intersections are imported from Lemma 10.135.6.

View graph