English
Let X, Y, Z be schemes with an open cover 𝒰 of X, a morphism f: X → Z and a morphism g: Y → Z. For all indices i, j in the covering, a certain canonical map from the iterated pullback to X ×_Z Y satisfies a natural compatibility: the second projection of the pullback after the lift equals the second projection composed with the first projection.
Русский
Пусть X, Y, Z — схемы, 𝒰 — открытое покрытие X, f: X → Z, g: Y → Z. Для всех индексов i, j из покрытия существует каноническое отображение из повторного волокна в X ×_Z Y, и проекции удовлетворяют естественной совместимости: вторая проекция после подъёма равна второй проекции, предварительно композиции с первой.
LaTeX
$$$$ p_2 \circ \varphi_{i,j} = p_2 \circ p_1' $$$$
Lean4
@[simp, reassoc]
theorem pullbackFstιToV_snd (i j : 𝒰.I₀) :
pullbackFstιToV 𝒰 f g i j ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.snd _ _ := by simp [pullbackFstιToV, p1]
