English
The composition of the inverse of the pullback iso with the first projection equals the canonical map to the tensor product from rings.
Русский
Состав обратного изоморфизма пулбэка с первой проекцией равен каноническому отображению в тензорном произведении колец.
LaTeX
$$$$ (pullbackSpecIso R S T)^{-1} \circ \mathrm{fst} = \mathrm{Spec.map}(\text{ofHom}(\mathrm{includeLeft})) $$$$
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 first projection is
the morphism `Spec (S ⊗[R] T) ⟶ Spec S` obtained by applying `Spec.map` to the ring morphism
`s ↦ s ⊗ₜ[R] 1`.
-/
@[reassoc (attr := simp)]
theorem pullbackSpecIso_inv_fst :
(pullbackSpecIso R S T).inv ≫ pullback.fst _ _ = Spec.map (ofHom includeLeftRingHom) :=
limit.isoLimitCone_inv_π _ _
