English
With the same gluing datum, the prime variant expresses the same relation as above but with a slightly rearranged expression of the transition and structure maps, showing compatibility of the preimage-image correspondence under the gluing data.
Русский
С тем же набором данных склейки формула с апострофом демонстрирует ту же связь между прообразом и образом, но с иной записью переходных и структурных отображений; это подтверждает совместимость сопоставления прообраза и образа в рамках данных склейки.
LaTeX
$$$\\mathsf{ι}_j^{-1}(\\mathsf{ι}_i''U) = (t_{i j} \\gg f)''((f)^{-1}U)$.$$
Lean4
theorem preimage_image_eq_image' (i j : D.J) (U : Set (𝖣.U i)) :
𝖣.ι j ⁻¹' (𝖣.ι i '' U) = (D.t i j ≫ D.f _ _) '' (D.f _ _ ⁻¹' U) :=
by
convert D.preimage_image_eq_image i j U using 1
rw [coe_comp, coe_comp, Set.image_comp]
congr! 1
rw [← Set.eq_preimage_iff_image_eq, Set.preimage_preimage]
· change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _
rw [𝖣.t_inv_assoc]
rw [← isIso_iff_bijective]
apply (forget TopCat).map_isIso
