structure AlgebraicHartogs.HeightOnePrime (A : Type u_1) [CommRing A] : Type u_1

A height-one prime ideal in a commutative ring, bundled with the proofs that it is prime and has height exactly one.

• asIdeal : Ideal A
• isPrime : self.asIdeal.IsPrime
• height_eq : self.asIdeal.height = 1

theorem AlgebraicHartogs.HeightOnePrime.ne_bot {A : Type u_1} [CommRing A] [IsDomain A] (p : HeightOnePrime A) : p.asIdeal ≠ ⊥

A height-one prime is non-zero (the zero ideal has height 0 in a domain).

theorem AlgebraicHartogs.exists_height_one_prime_containing {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] (a : A) (ha_ne : a ≠ 0) (ha_nu : ¬IsUnit a) : ∃ (p : HeightOnePrime A), a ∈ p.asIdeal

Krull's Hauptidealsatz: any nonzero non-unit element of a Noetherian domain is contained in some height-one prime ideal.

theorem AlgebraicHartogs.mem_of_mem_all_prime_localizations {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (x : K) (hx : ∀ (v : PrimeSpectrum A), x ∈ Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) : x ∈ Set.range ⇑(algebraMap A K)

An element of the fraction field K lying in every prime localization of A comes from A itself; this is the algebraic Hartogs principle over all primes.

theorem AlgebraicHartogs.height_eq_one_of_prime_ne_bot {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (p : Ideal A) [hp : p.IsPrime] (hne : p ≠ ⊥) : p.height = 1

In a Dedekind domain, every nonzero prime ideal has height exactly one.

theorem AlgebraicHartogs.algebraicHartogs_dedekind {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (x : K) (hx : ∀ (v : IsDedekindDomain.HeightOneSpectrum A), x ∈ Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) : x ∈ Set.range ⇑(algebraMap A K)

Algebraic Hartogs theorem for Dedekind domains: a fraction-field element regular at every height-one prime is globally regular.

def AlgebraicHartogs.equivHeightOneSpectrumPrime {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] : IsDedekindDomain.HeightOneSpectrum A ≃ HeightOnePrime A

Equivalence between Mathlib's HeightOneSpectrum and our HeightOnePrime structure for a Dedekind domain.