English
The image of a basic open under the inclusion corresponds to the corresponding basic open on X.
Русский
Образ базового открытого множества под включением соответствует базовому открытому множеству на X.
LaTeX
$$$ U.\\iota \\; ''ᵁ\\; U.toScheme.basicOpen r = X.basicOpen r $$$
Lean4
theorem map_basicOpen (r : Γ(U, ⊤)) :
U.ι ''ᵁ U.toScheme.basicOpen r = X.basicOpen (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top.symm).op r) :=
by
refine (Scheme.image_basicOpen (X.ofRestrict U.isOpenEmbedding) r).trans ?_
rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.isOpenEmbedding_obj_top).op]
rw [← CommRingCat.comp_apply, ← CategoryTheory.Functor.map_comp, ← op_comp, eqToHom_trans, eqToHom_refl, op_id,
CategoryTheory.Functor.map_id]
congr
exact PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ _ _
