Theorems · Definition · algebraic geometry

AlgebraicGeometry.Spec.fiberToSpecResidueFieldIso

(R S : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      [inst_2 : Algebra R S] →
        (p : PrimeSpectrum R) →
          CategoryTheory.Arrow.mk
              (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
                (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) p) ≅
            CategoryTheory.Arrow.mk
              (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))

The morphism from the fiber of Spec S ⟶ Spec R at some prime p to Spec κ(p) is isomorphic to the map induced by κ(p) ⟶ κ(p) ⊗[R] S.

Defined in

Mathlib.AlgebraicGeometry.Fiber

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra