English
For maps f: W → Y and g: X → Z, the range of the product map prod.map f g equals the intersection of preimages of the ranges of f and g under the respective projections.
Русский
Для отображений f: W → Y и g: X → Z множество образа произведения prod.map f g совпадает с пересечением предобразных изображений f и g через соответствующие проекции.
LaTeX
$$$\\operatorname{range}(\\mathrm{Limits.prod.map} f g) = (\\mathrm{Limits.prod.fst})^{-1}(\\operatorname{range} f) \\cap (\\mathrm{Limits.prod.snd})^{-1}(\\operatorname{range} g)$$$
Lean4
theorem range_prod_map {W X Y Z : TopCat.{u}} (f : W ⟶ Y) (g : X ⟶ Z) :
Set.range (Limits.prod.map f g) =
(Limits.prod.fst : Y ⨯ Z ⟶ _) ⁻¹' Set.range f ∩ (Limits.prod.snd : Y ⨯ Z ⟶ _) ⁻¹' Set.range g :=
by
ext x
constructor
· rintro ⟨y, rfl⟩
simp_rw [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range, ← ConcreteCategory.comp_apply, Limits.prod.map_fst,
Limits.prod.map_snd, ConcreteCategory.comp_apply, exists_apply_eq_apply, and_self_iff]
· rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
use (prodIsoProd W X).inv (x₁, x₂)
apply Concrete.limit_ext
rintro ⟨⟨⟩⟩
· rw [← ConcreteCategory.comp_apply]
erw [Limits.prod.map_fst]
rw [ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_fst_apply]
exact hx₁
· rw [← ConcreteCategory.comp_apply]
erw [Limits.prod.map_snd]
rw [ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_snd_apply]
exact hx₂
