Theorems · Definition · algebraic geometry

AlgebraicGeometry.pullbackSpecIso

(R S T : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      [inst_2 : CommRing T] →
        [inst_3 : Algebra R S] →
          [inst_4 : Algebra R T] →
            CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
                (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))) ≅
              AlgebraicGeometry.Spec (CommRingCat.of (TensorProduct R S T))

The isomorphism between the fibred product of two schemes Spec S and Spec T over a scheme Spec R and the Spec of the tensor product S ⊗[R] T.

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

26 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebra