English
Let D be a gluing datum and i, j two indices with U a subset of the i-th open set. Then the preimage, in the j-component, of the image of U under the i-th inclusion coincides with the image, under the transition map, of the preimage of U along the j-to-i transition.
Русский
Пусть D будет данными склейки, и пусть i, j — индексы; для множества U ⊆ 𝖣.U i справедливо, что прообраз изображения U под вхождение ι_i по отношению к j-координате равен образу прообраза U под переходному отображению между i и j.
LaTeX
$$$\\iota_j^{-1}(\\iota_i''U) = (t_{j i} \\;\\gg\\; f)''((f)^{-1}(U))$$$
Lean4
theorem preimage_image_eq_image (i j : D.J) (U : Set (𝖣.U i)) :
𝖣.ι j ⁻¹' (𝖣.ι i '' U) = D.f _ _ '' ((D.t j i ≫ D.f _ _) ⁻¹' U) :=
by
have : D.f _ _ ⁻¹' (𝖣.ι j ⁻¹' (𝖣.ι i '' U)) = (D.t j i ≫ D.f _ _) ⁻¹' U :=
by
ext x
conv_rhs => rw [← Set.preimage_image_eq U (D.ι_injective _)]
simp
rw [← this, Set.image_preimage_eq_inter_range]
symm
apply Set.inter_eq_self_of_subset_left
rw [← D.preimage_range i j]
exact Set.preimage_mono (Set.image_subset_range _ _)
