English
Let f: X → Z and g: Y → Z be morphisms in TopCat and U ⊆ X. Then the image of the pullback of f and g under the snd projection equals the preimage under g of the image of U under f:
Русский
Пусть f: X → Z и g: Y → Z — морфизмы в TopCat, и U ⊆ X. Тогда образ притяжения (pullback) под действием snd равен предобразу по g образа U под f:
LaTeX
$$$ (pullback.snd\, f\, g)\\,[(pullback.fst\, f\, g)^{-1}(U)] = g^{-1}(f(U)) $$$
Lean4
theorem pullback_snd_image_fst_preimage (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set X) :
(pullback.snd f g) '' ((pullback.fst f g) ⁻¹' U) = g ⁻¹' (f '' U) :=
by
ext x
constructor
· rintro ⟨y, hy, rfl⟩
exact ⟨(pullback.fst f g) y, hy, CategoryTheory.congr_fun pullback.condition y⟩
· rintro
⟨y, hy, eq⟩
-- next 5 lines were
-- `exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, by simpa, by simp⟩` before https://github.com/leanprover-community/mathlib4/pull/13170
refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, ?_, ?_⟩
· simp only [coe_of, Set.mem_preimage]
convert hy
rw [pullbackIsoProdSubtype_inv_fst_apply]
· rw [pullbackIsoProdSubtype_inv_snd_apply]
