English
In a pullback square with open immersions iU: U → X and iV: V → Y, for any open W ⊆ V one has iU^{-1}(f'^{-1}(W)) = f^{-1}(iV^{-1}(W)).
Русский
В квадрате тяготения с открытыми вложениями iU: U → X и iV: V → Y, для любого открытого W ⊆ V выполняется iU^{-1}(f'^{-1}(W)) = f^{-1}(iV^{-1}(W)).
LaTeX
$$$ i_U^{-1}(f'^{-1}(W)) = f^{-1}(i_V^{-1}(W)) $$$
Lean4
theorem image_preimage_eq_preimage_image_of_isPullback {X Y U V : Scheme.{u}} {f : X ⟶ Y} {f' : U ⟶ V} {iU : U ⟶ X}
{iV : V ⟶ Y} [IsOpenImmersion iV] [IsOpenImmersion iU] (H : IsPullback f' iU iV f) (W : V.Opens) :
iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W := by
ext x
by_cases hx : x ∈ Set.range iU.base
· obtain ⟨x, rfl⟩ := hx
simp only [IsOpenMap.coe_functor_obj, TopologicalSpace.Opens.map_coe, iU.isOpenEmbedding.injective.mem_set_image,
Set.mem_preimage, SetLike.mem_coe, ← Scheme.comp_base_apply, ← H.w]
simp only [Scheme.comp_coeBase, TopCat.comp_app, iV.isOpenEmbedding.injective.mem_set_image, SetLike.mem_coe]
· constructor
· rintro ⟨x, hx, rfl⟩; cases hx ⟨x, rfl⟩
· rintro ⟨y, hy, e : iV.base y = f.base x⟩
obtain ⟨x, rfl⟩ := (IsOpenImmersion.range_pullback_snd_of_left iV f).ge ⟨y, e⟩
rw [← H.isoPullback_inv_snd] at hx
cases hx ⟨_, rfl⟩
