Theorems · Definition · algebraic geometry

PrimeSpectrum.primesOverOrderIsoFiber

(R : Type u_3) →
  (S : Type u_4) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (p : Ideal R) → [inst_3 : p.IsPrime] → ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S)

The OrderIso between the set of primes lying over a prime ideal p : Ideal R, and the prime spectrum of κ(p) ⊗[R] S.

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIdeal.IsPrime