English
Let f: X -> Z and g: Y -> Z be maps. There is a canonical isomorphism between the pullback of f and g and the subspace of X × Y consisting of pairs (x,y) with f(x) = g(y). Under this isomorphism, the inverse composed with the first projection is exactly the standard projection to the X-factor; equivalently, the first projection on X in the pullback equals the composition inv followed by fst.
Русский
Пусть объекты X, Y, Z и отображения f: X → Z, g: Y → Z. Существует каноническое изоморфное отображение между пределом типа pullback(f,g) и подпространством X × Y состоящим из пар (x,y) с f(x) = g(y). Под этим изоморфизмом обратное отображение, далее первая проекция, совпадает с обычной проекцией на X; то есть pullbackFst = inv ≫ fst.
LaTeX
$$$ (pullbackIsoProdSubtype f g)^{-1} \circ pullback.fst\, f\, g = pullbackFst\, f\, g $$$
Lean4
@[reassoc (attr := simp)]
theorem pullbackIsoProdSubtype_inv_fst (f : X ⟶ Z) (g : Y ⟶ Z) :
(pullbackIsoProdSubtype f g).inv ≫ pullback.fst _ _ = pullbackFst f g := by
simp [pullbackCone, pullbackIsoProdSubtype]
