English
If pushouts are taken in rings, their opposite consistency yields a pullback in schemes; i.e., Spec maps commute with pullbacks.
Русский
Если в кольцах взять относительные схождения (pushout), получаем пулбэк в схемах; то есть отображения Spec совместимы с пулбэками.
LaTeX
$$$$ \text{isPullback of Spec maps via pushout} $$$$
Lean4
/-- The composition 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 morphism
`Spec (S ⊗[R] T) ⟶ Spec T` obtained by applying `Spec.map` to the ring morphism `t ↦ 1 ⊗ₜ[R] t`
is the second projection.
-/
@[reassoc (attr := simp)]
theorem pullbackSpecIso_hom_snd :
(pullbackSpecIso R S T).hom ≫ Spec.map (ofHom (toRingHom includeRight)) = pullback.snd _ _ := by
rw [← pullbackSpecIso_inv_snd, Iso.hom_inv_id_assoc]
