Module

PrimeContainingAtHeightOne.lean

Nyll.SchemeTheory.RingTheory.PrimeContainingAtHeightOne

4 declarations indexed from sourceView source ↗

Module documentation

Height-one primes containing an element of a local ring

This file proves the local-ring prime-existence statement of Stacks Project Tag 0BJG. A prime chain selects a positive-dimensional component of a hypersurface, and localization decreases the positive height.

Imports4

Nyll.SchemeTheory.RingTheory.PuncturedHypersurfacePrime
Mathlib.RingTheory.Ideal.Height
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.Tactic.Push

Imported by3

theorem

two_le_quotient_dimension_of_prime_chain

L28 ↗

SchemeTheory.two_le_quotient_dimension_of_prime_chain

Documentation

A strict prime chain below the maximal ideal gives quotient dimension at least two. The primes need not be minimal, and Noetherianity is unnecessary.

Source context 3 commands

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

open IsLocalRing
namespace SchemeTheory
universe u

Lean source · statement

theorem two_le_quotient_dimension_of_prime_chain
    {R : Type u} [CommRing R] [IsLocalRing R]
    (P Q : Ideal R) [P.IsPrime] [Q.IsPrime]
    (hPQ : P < Q) (hQm : Q < maximalIdeal R) :
    (2 : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ P)

theorem

exists_positive_height_prime_below_maximal

L67 ↗

SchemeTheory.exists_positive_height_prime_below_maximal

Source context 3 commands

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

open IsLocalRing
namespace SchemeTheory
universe u

Lean source · statement

theorem exists_positive_height_prime_below_maximal
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdim : (2 : WithBot ℕ∞) ≤ ringKrullDim R)
    (f : R) (hf : f ∈ maximalIdeal R) :
    ∃ Q : Ideal R, Q.IsPrime ∧ f ∈ Q ∧
      (1 : ℕ∞) ≤ Q.height ∧ Q < maximalIdeal R

theorem

exists_height_one_prime_containing

L114 ↗

SchemeTheory.exists_height_one_prime_containing

Documentation

Every element of the maximal ideal of a positive-dimensional Noetherian local ring lies in a height-one prime.

Source context 3 commands

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

open IsLocalRing
namespace SchemeTheory
universe u

Lean source · statement

theorem exists_height_one_prime_containing
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdim : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (f : R) (hf : f ∈ maximalIdeal R) :
    ∃ P : Ideal R, P.IsPrime ∧ f ∈ P ∧ P.height = 1

theorem

exists_prime_containing_ringKrullDim_localization_eq_one

L170 ↗

SchemeTheory.exists_prime_containing_ringKrullDim_localization_eq_one

Documentation

In a positive-dimensional Noetherian local ring, every element of the maximal ideal lies in a prime whose localization has dimension one (Stacks Project Tag 0BJG).

Source context 3 commands

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

open IsLocalRing
namespace SchemeTheory
universe u

Lean source · statement

theorem exists_prime_containing_ringKrullDim_localization_eq_one
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdim : (1 : WithBot ℕ∞) ≤ ringKrullDim R)
    (f : R) (hf : f ∈ maximalIdeal R) :
    ∃ (P : Ideal R) (_ : P.IsPrime), f ∈ P ∧
      ringKrullDim (Localization.AtPrime P) = 1

Module documentation

Height-one primes containing an element of a local ring

Declarations

two_le_quotient_dimension_of_prime_chain

exists_positive_height_prime_below_maximal

exists_height_one_prime_containing

exists_prime_containing_ringKrullDim_localization_eq_one