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