EtaleFundamentalGroups.exists_height_one_prime_containing_of_mem_maximalIdeal
Every element of the maximal ideal of a positive-dimensional Noetherian local domain is contained in a height-one prime.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe uLean source · statement
theorem exists_height_one_prime_containing_of_mem_maximalIdeal
{A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
[IsLocalRing A] (hA : 1 ≤ ringKrullDim A)
{f : A} (hf : f ∈ maximalIdeal A) :
∃ p : Ideal A, p.IsPrime ∧ p.height = 1 ∧ f ∈ p