English
Let f: X → Y be a morphism in a category with pullbacks. Consider the diagonal morphism diagonal f and the canonical map map that transfers pullback objects along i₁ and i₂. Then composing the appropriate pullback projection snd with fst and the map data yields the standard projection fst on the pullback, i.e. the composite equals pullback.fst.
Русский
Пусть f: X → Y — морфизм в категории, в которой существуют волокоподобные (pullback). Рассматривая диагональ f и каноническое отображение map, получаемое переносом пределов вдоль i₁ и i₂, композиция соответствующих проекций snd и fst с картой даёт обычную проекцию fst на предельном объекте; равенство: равенство композиций равно pullback.fst.
LaTeX
$$$$\text{pullback.snd}(\text{diagonal}(f),\ \text{map}(i_1\,\!\gg\!\snd(f,i))\ (i_2\,\!\gg\!\snd(f,i))\ f\ f\ (i_1\gg\!\fst(f,i))\ (i_2\gg\!\fst(f,i))\ i\ (\text{condition})\ (\text{condition})) \\gg\ fst\ _\ _ \\ =\ pullback.fst\ _\ _ $$$$
Lean4
@[reassoc (attr := simp)]
theorem pullback_diagonal_map_snd_fst_fst :
(pullback.snd (diagonal f)
(map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i (by simp [condition])
(by simp [condition]))) ≫
fst _ _ ≫ i₁ ≫ fst _ _ =
pullback.fst _ _ :=
by
conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]
rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]
