NYLL
Module

LocalPrimeCoheightOne.lean

Nyll.EtaleFundamentalGroups.Purity.LocalPrimeCoheightOne
1 declaration indexed from sourceView source ↗

Module documentation

A one-dimensional prime quotient over a nonmaximal radical

A proper ideal with nonmaximal radical lies in a nonmaximal prime. The spectrum of a Noetherian local ring has finite dimension, so a prime of coheight one lies above that prime. The quotient-spectrum order isomorphism identifies its coheight with the dimension of its quotient.

Imports5
Imported by1

Declarations

theorem

exists_prime_over_lt_maximalIdeal_with_quotient_dim_one

L32 ↗
EtaleFundamentalGroups.Purity.exists_prime_over_lt_maximalIdeal_with_quotient_dim_one
Documentation

A proper ideal whose radical is not maximal is contained in a nonmaximal prime with one-dimensional quotient.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem exists_prime_over_lt_maximalIdeal_with_quotient_dim_one
    (I : Ideal R) (hI : I ≠ ⊤) (hradical : I.radical ≠ maximalIdeal R) :
    ∃ P : Ideal R, I ≤ P ∧ P.IsPrime ∧ P < maximalIdeal R ∧
      ringKrullDim (R ⧸ P) = (1 : WithBot ℕ∞)

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