Theorems · Theorem · algebraic geometry

AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc

∀ (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] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of S) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
        h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) h

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 first projection is the morphism Spec (S ⊗[R] T) ⟶ Spec S obtained by applying Spec.map to the ring morphism s ↦ s ⊗ₜ[R] 1.

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebra