English
The composition of the inverse pullback isomorphism with the second projection yields the canonical map corresponding to the right tensor factor.
Русский
Сочетание обратного изоморфизма пулбэка с второй проекцией даёт каноническое отображение, соответствующее правому тензорному фактору.
LaTeX
$$$$ (pullbackSpecIso R S T)^{-1} \circ \mathrm{snd} = \mathrm{Spec.map}(\text{ofHom}(\text{includeRight})) $$$$
Lean4
/-- 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`.
-/
@[reassoc (attr := simp)]
theorem pullbackSpecIso_inv_snd :
(pullbackSpecIso R S T).inv ≫ pullback.snd _ _ =
Spec.map (ofHom (R := T) (S := S ⊗[R] T) (toRingHom includeRight)) :=
limit.isoLimitCone_inv_π _ _
