English
Restricting a morphism twice onto a basic open is isomorphic to restricting once to that basic open.
Русский
Ограничение морфизма дважды на базовое открытое множество изоморфно одному ограничению на это базовое открытое множество.
LaTeX
$$def morphismRestrictRestrictBasicOpen {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (r : Γ(Y, U)) : Arrow.mk (f|_U|_ U.basicOpen (Y.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op r)) ≅ Arrow.mk (f|_ Y.basicOpen r)$$
Lean4
/-- Restricting a morphism twice onto a basic open set is isomorphic to one restriction. -/
def morphismRestrictRestrictBasicOpen {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (r : Γ(Y, U)) :
Arrow.mk (f ∣_ U ∣_ U.toScheme.basicOpen (Y.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op r)) ≅
Arrow.mk (f ∣_ Y.basicOpen r) :=
by
refine morphismRestrictRestrict _ _ _ ≪≫ morphismRestrictEq _ ?_
have e := Scheme.preimage_basicOpen U.ι r
rw [Scheme.Opens.ι_app] at e
rw [← U.toScheme.basicOpen_res_eq _ (eqToHom U.inclusion'_map_eq_top).op]
erw [← elementwise_of% Y.presheaf.map_comp]
rw [eqToHom_op, eqToHom_op, eqToHom_map, eqToHom_trans]
erw [← e]
ext1
dsimp [Opens.map_coe]
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left, Scheme.Opens.range_ι]
exact Y.basicOpen_le r
