English
The fst projection of the symmetric carrier equivalence recovers the x component of the triplet, and the snd projection recovers the y component, establishing a compatibility with the pullback.
Русский
Проекции fst и snd носителя через симметрическую эквивалентность возвращают соответствующие компоненты x и y тройки, демонстрируя совместимость с pullback.
LaTeX
$$$\text{carrierEquiv}.symm \langle T, p \rangle \mapsto (\text{fst base} = x, \text{snd base} = y)$$$
Lean4
/-- If `f : X ⟶ S` and `g : Y ⟶ S` are morphisms of schemes and `x : X` and `y : Y` are points such
that `f x = g y`, then there exists `z : X ×[S] Y` lying above `x` and `y`.
In other words, the map from the underlying topological space of `X ×[S] Y` to the fiber product
of the underlying topological spaces of `X` and `Y` over `S` is surjective.
-/
theorem exists_preimage_pullback (x : X) (y : Y) (h : f.base x = g.base y) :
∃ z : ↑(pullback f g), (pullback.fst f g).base z = x ∧ (pullback.snd f g).base z = y :=
(Pullback.Triplet.mk' x y h).exists_preimage
