Theorems · Definition · commutative algebra

IsDedekindDomain.HeightOneSpectrum.equivPrimesOver

{A : Type u_4} →
  [inst : CommRing A] →
    {p : Ideal A} →
      [hpm : p.IsMaximal] →
        (B : Type u_5) →
          [inst_1 : CommRing B] →
            [IsDedekindDomain B] →
              [inst_3 : Algebra A B] →
                [IsDomain A] →
                  [Module.IsTorsionFree A B] →
                    p ≠ 0 → { v // v.asIdeal ∣ Ideal.map (algebraMap A B) p } ≃ ↑(p.primesOver B)

The bijection between the elements of the height one prime spectrum of B that divide the lift of the maximal ideal p in B and the primes over p in B.

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

3 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIdeal.IsMaximalCommRingIsDedekindDomainAlgebraIsDomainModule.IsTorsionFree