instHasPullback — Mathlib

English

Any pair of morphisms between schemes has a pullback object, given by the fiber product scheme.

Русский

Любая пара отображений между схемами имеет пулбэк-объект, заданный через точное волокно.

LaTeX

$$$$ \exists P, p_1: P \to X, p_2: P \to Y, f p_1 = g p_2, \text{ and } P \text{ is a pullback} $$$$

Lean4

instance {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) : HasPullback f g :=
  hasPullback_of_cover (Z.affineCover.pullback₁ f) f g

Похожие утверждения