Module

PuncturedHypersurfacePrime.lean

Nyll.SchemeTheory.RingTheory.PuncturedHypersurfacePrime

2 declarations indexed from sourceView source ↗

Module documentation

Nonclosed points of local hypersurfaces

A principal hypersurface in a Noetherian local ring of dimension at least two contains a prime different from the maximal ideal. The same construction on a prime quotient produces a point on a specified irreducible component.

Imports3

Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.LocalRing.Quotient
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by3

theorem

exists_prime_containing_ne_maximal_of_two_le_ringKrullDim

L26 ↗

SchemeTheory.exists_prime_containing_ne_maximal_of_two_le_ringKrullDim

Documentation

A hypersurface in local dimension at least two contains a nonclosed point.

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_ne_maximal_of_two_le_ringKrullDim
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdim : (2 : WithBot ℕ∞) ≤ ringKrullDim R)
    (f : R) (hf : f ∈ maximalIdeal R) :
    ∃ P : Ideal R, P.IsPrime ∧ f ∈ P ∧ P ≠ maximalIdeal R

theorem

exists_prime_over_containing_ne_maximal_of_two_le_quotient_ringKrullDim

L45 ↗

SchemeTheory.exists_prime_over_containing_ne_maximal_of_two_le_quotient_ringKrullDim