Nonzero prime ideals lying over a prime #

For an injective algebra map of commutative rings R → B, the nonzero prime ideals of B lying over a nonzero prime v of R correspond to Ideal.primesOver v.asIdeal B. The correspondence is IsDedekindDomain.HeightOneSpectrum.liesOverEquivPrimesOver. It uses Mathlib's type of nonzero prime ideals, IsDedekindDomain.HeightOneSpectrum, without requiring either ring to be Dedekind or the extension to be integral. For an integral extension of domains, TauCeti.sigmaPrimesOverEquivPrimesAbove assembles these fibres into the canonical carrier of primes above a set; its forward map keeps the top prime, and its inverse indexes that prime by its contraction.

source

instance IsDedekindDomain.HeightOneSpectrum.liesOver_val {R : Type u_1} {B : Type u_2} [CommRing R] [CommRing B] [Algebra R B] {v : HeightOneSpectrum R} (w : { w : HeightOneSpectrum B // w.asIdeal.LiesOver v.asIdeal }) :

(↑w).asIdeal.LiesOver v.asIdeal

A height one prime of B taken from the subtype of those lying over v lies over v.

source

def IsDedekindDomain.HeightOneSpectrum.liesOverEquivPrimesOver {R : Type u_1} (B : Type u_2) [CommRing R] [CommRing B] [Algebra R B] [FaithfulSMul R B] (v : HeightOneSpectrum R) :

{ w : HeightOneSpectrum B // w.asIdeal.LiesOver v.asIdeal } ≃ ↑(v.asIdeal.primesOver B)

The nonzero prime ideals of B lying over a nonzero prime v of R are precisely Ideal.primesOver v.asIdeal B. Injectivity of the algebra map ensures that an ideal lying above v is nonzero; neither ring needs to be a Dedekind domain.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.liesOverEquivPrimesOver_apply {R : Type u_1} (B : Type u_2) [CommRing R] [CommRing B] [Algebra R B] [FaithfulSMul R B] (v : HeightOneSpectrum R) (w : { w : HeightOneSpectrum B // w.asIdeal.LiesOver v.asIdeal }) :

↑((liesOverEquivPrimesOver B v) w) = (↑w).asIdeal

source

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.liesOverEquivPrimesOver_symm_apply {R : Type u_1} (B : Type u_2) [CommRing R] [CommRing B] [Algebra R B] [FaithfulSMul R B] (v : HeightOneSpectrum R) (Q : ↑(v.asIdeal.primesOver B)) :

(↑((liesOverEquivPrimesOver B v).symm Q)).asIdeal = ↑Q

source

def TauCeti.sigmaPrimesOverEquivPrimesAbove (R : Type u_1) (B : Type u_2) [CommRing R] [IsDomain R] [CommRing B] [IsDomain B] [Algebra R B] [Algebra.IsIntegral R B] [FaithfulSMul R B] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) :

(v : ↑S) × ↑((↑v).asIdeal.primesOver B) ≃ ↑(IsDedekindDomain.HeightOneSpectrum.primesAbove R B S)

Primes above a set correspond to the sigma family of primes over each member of that set. The forward map keeps the top prime; the inverse indexes it by its contraction.

Equations