English
Assume P is a morphism property stable under base change and preserved under pushouts as in IsJointlySurjectivePreserving. For X, Y, S schemes with a pullback of f: X → S and g: Y → S, and given x ∈ X and y ∈ Y with f.base x = g.base y, there exists a ∈ pullback f g such that (pullback.snd f g).base a = y.
Русский
Пусть P — свойство морфизмов, устойчивое к базовому базированию и сохраняющееся под объединениями, как в IsJointlySurjectivePreserving. Пусть существуют схемы X, Y, S с f: X → S, g: Y → S, т. е. имеется pullback, и выбраны x ∈ X, y ∈ Y такие, что f.base x = g.base y. Тогда существует a ∈ pullback f g, удовлетворяющее (pullback.snd f g).base a = y.
LaTeX
$$$\\exists a : \\uparrow(\\text{pullback } f g), (pullback.snd f g).base\\ a = y$$$
Lean4
theorem exists_preimage_snd_triplet_of_prop [IsJointlySurjectivePreserving P] {X Y S : Scheme.{u}} {f : X ⟶ S}
{g : Y ⟶ S} [HasPullback f g] (hf : P f) (x : X) (y : Y) (h : f.base x = g.base y) :
∃ a : ↑(pullback f g), (pullback.snd f g).base a = y :=
by
let iso := pullbackSymmetry f g
haveI : HasPullback g f := hasPullback_symmetry f g
obtain ⟨a, ha⟩ := exists_preimage_fst_triplet_of_prop hf y x h.symm
use (pullbackSymmetry f g).inv.base a
rwa [← Scheme.comp_base_apply, pullbackSymmetry_inv_comp_snd]
