English
The composition of the isomorphism pullbackSpecIso with the first inclusion map gives the first projection on Spec level.
Русский
Сочетание изоморфизма pullbackSpecIso с первой инклюзией даёт первую проекцию на уровне Spec.
LaTeX
$$$$ \mathrm{pullbackSpecIso}^{-1} \circ \mathrm{fst} = \mathrm{Spec.map}(\mathrm{ofHom}(\mathrm{algebraMap} \; R \; S)) $$$$
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 S` obtained by applying `Spec.map` to the ring morphism `s ↦ s ⊗ₜ[R] 1`
is the first projection.
-/
@[reassoc (attr := simp)]
theorem pullbackSpecIso_hom_fst :
(pullbackSpecIso R S T).hom ≫ Spec.map (ofHom includeLeftRingHom) = pullback.fst _ _ := by
rw [← pullbackSpecIso_inv_fst, Iso.hom_inv_id_assoc]
