Theorems · Definition · commutative algebra

Ideal.fiberIsoOfBijectiveResidueField

{R : Type u_1} →
  {R' : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing R'] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R R'] →
              [inst_4 : Algebra R S] →
                {p : Ideal R} →
                  {q : Ideal R'} →
                    [inst_5 : p.IsPrime] →
                      [inst_6 : q.IsPrime] →
                        [inst_7 : q.LiesOver p] →
                          Function.Bijective ⇑(Ideal.ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) →
                            ↑(q.primesOver (TensorProduct R R' S)) ≃o ↑(p.primesOver S)

If q is a prime of R' lying over p, a prime of R, such that κ(q) = κ(p), then the fiber of R' → R' ⊗[R] S over q is in bijection with the fiber of R → S over p.

Defined in

Mathlib.RingTheory.Etale.QuasiFinite

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebraIdeal.IsPrimeIdeal.IsPrimeIdeal.LiesOver