English
Let f: A → B and g: A → C be morphisms of affine schemes. Then the square formed by Spec(pushout.inl f g), Spec(pushout.inr f g), Spec.map f, and Spec.map g is a pullback square.
Русский
Пусть f: A → B и g: A → C — морфизмы аффайн-схем. Тогда квадрат, образованный квадратом из Spec(pushout.inl f g), Spec(pushout.inr f g), Spec.map f и Spec.map g, является квадратом-подстановкой (pullback).
LaTeX
$$$$\\mathrm{IsPullback}\\Big(\\mathrm{Spec.map}(\\mathrm{pushout.inl}(f,g)),\\ \\mathrm{Spec.map}(\\mathrm{pushout.inr}(f,g)),\\ \\mathrm{Spec.map}~f,\\ \\mathrm{Spec.map}~g\\Big)$$$$
Lean4
theorem isPullback_Spec_map_pushout {A B C : CommRingCat} (f : A ⟶ B) (g : A ⟶ C) :
IsPullback (Spec.map (pushout.inl f g)) (Spec.map (pushout.inr f g)) (Spec.map f) (Spec.map g) :=
by
apply isPullback_Spec_map_isPushout
exact IsPushout.of_hasPushout f g
