Module

RegularLocalQuotientLift.lean

Nyll.SchemeTheory.RingTheory.RegularLocalQuotientLift

2 declarations indexed from sourceView source ↗

Module documentation

Lifting regularity through a nonzerodivisor quotient

If a Noetherian local ring modulo a nonzerodivisor is regular, then the original ring is regular. A minimal generating set of the quotient maximal ideal lifts, together with the nonzerodivisor, to a generating set of the original maximal ideal. The dimension formula gives the required bound.

This proves the one-element assertion of Stacks Project, Lemma 10.106.7 (tag 00NU), used for a regular Cartier divisor in Lemma 58.31.3 (0EYE).

Imports5

Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.Algebra.Module.SpanRank
Mathlib.RingTheory.Ideal.Quotient.Operations

Imported by3

theorem

maximalIdeal_spanFinrank_le_quotient_add_one

L33 ↗

SchemeTheory.maximalIdeal_spanFinrank_le_quotient_add_one

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace SchemeTheory
universe u

Lean source · statement

theorem maximalIdeal_spanFinrank_le_quotient_add_one
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (x : R) [IsLocalRing (R ⧸ Ideal.span {x})] :
    (maximalIdeal R).spanFinrank ≤
      (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1

theorem

isRegularLocalRing_of_quotient_span_singleton

L87 ↗

SchemeTheory.isRegularLocalRing_of_quotient_span_singleton

Documentation

A Noetherian local ring is regular if its quotient by a nonzerodivisor in the maximal ideal is regular.