English
For a pullback square of f i j and f i k, the image of the pulled-back set under π2 equals the inverse image of the image under f i j along f i k; i.e., the pullback base compatibility holds for the underlying presheaf.
Русский
Для квадрата вытаскивания касательно f i j и f i k верна совместимость образа вытянутого множества по проекции с обратным образом образа через f i j вдоль f i k.
LaTeX
$$$(\\pi_2 i,j,k)''((\\pi_1 i,j,k)^{-1}' S) = D.f_{i k}^{-1}(D.f_{i j}''S)$$$
Lean4
theorem pullback_base (i j k : D.J) (S : Set (D.V (i, j)).carrier) :
(π₂ i, j, k) '' ((π₁ i, j, k) ⁻¹' S) = D.f i k ⁻¹' (D.f i j '' S) :=
by
have eq₁ : _ = (π₁ i, j, k).base := PreservesPullback.iso_hom_fst (forget C) _ _
have eq₂ : _ = (π₂ i, j, k).base := PreservesPullback.iso_hom_snd (forget C) _ _
rw [← eq₁, ← eq₂, TopCat.coe_comp, Set.image_comp, TopCat.coe_comp, Set.preimage_comp, Set.image_preimage_eq]
· simp only [forget_obj, forget_map, TopCat.pullback_snd_image_fst_preimage]
rw [← TopCat.epi_iff_surjective]
infer_instance
