English
For an open immersion f: X → Y and any open U in X with a section r ∈ Γ(X, U), the image of the basic open X.basicOpen r under f is the basic open Y.basicOpen of the transported element.
Русский
Для открытого вложения f: X → Y и любой открытой U ⊆ X с секцией r, образ D_X(r) в Y равен D_Y((f.appIso U)^{-1} r).
LaTeX
$$$f''^\\!\\!\\!∘ X.basicOpen(r) = Y.basicOpen((f.appIso\,U)^{-1}(r)).$$$
Lean4
theorem image_basicOpen {U : X.Opens} (r : Γ(X, U)) : f ''ᵁ X.basicOpen r = Y.basicOpen ((f.appIso U).inv r) :=
by
have e := Scheme.preimage_basicOpen f ((f.appIso U).inv r)
rw [Scheme.Hom.appIso_inv_app_apply, Scheme.basicOpen_res, inf_eq_right.mpr _] at e
· rw [← e, f.image_preimage_eq_opensRange_inter, inf_eq_right]
refine Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _)
· exact (X.basicOpen_le r).trans (f.preimage_image_eq _).ge
