English
The image of the map from the pullback to the product via fst and snd equals the set of pairs (x,y) with f(x) = g(y).
Русский
Образ отображения предела в произведение по fst и snd совпадает с парами (x,y), удовлетворяющими f(x) = g(y).
LaTeX
$$$ \operatorname{range}\big( \mathrm{prod.lift}( \mathrm{pullback.fst} f g, \mathrm{pullback.snd} f g ) \big) = \{ x \in X \times Y \mid (\mathrm{prod.fst} \circ f)(x) = (\mathrm{prod.snd} \circ g)(x) \} $$$
Lean4
theorem range_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :
Set.range (prod.lift (pullback.fst f g) (pullback.snd f g)) =
{x | (Limits.prod.fst ≫ f) x = (Limits.prod.snd ≫ g) x} :=
by
ext x
constructor
· rintro ⟨y, rfl⟩
simp only [← ConcreteCategory.comp_apply, Set.mem_setOf_eq]
simp [pullback.condition]
· rintro (h : f (_, _).1 = g (_, _).2)
use (pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩
apply Concrete.limit_ext
rintro ⟨⟨⟩⟩ <;> rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π] <;>
-- This used to be `simp` before https://github.com/leanprover/lean4/pull/2644
cat_disch
