Theorems · Theorem · algebraic geometry

AlgebraicGeometry.pullbackSpecIso_inv_snd

∀ (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.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)

The composition of the inverse of the isomorphism pullbackSpecIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the second projection is the morphism Spec (S ⊗[R] T) ⟶ Spec T obtained by applying Spec.map to the ring morphism t ↦ 1 ⊗ₜ[R] t.

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebra