English
The value of a restricted morphism on an open V equals a composition of the original morphism with a suitable restriction map on the presheaf.
Русский
Значение ограниченного морфизма на открытом V равно композиции исходного морфизма с соответствующей картой ограничения на прешейфе.
LaTeX
$$$(f \lvert_U).app V = f.app (U.ι ''ᵁ V) \;\circ\; X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op$$$
Lean4
theorem morphismRestrict_app {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) :
(f ∣_ U).app V = f.app (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op :=
by
have := Scheme.congr_app (morphismRestrict_ι f U) (U.ι ''ᵁ V)
simp only [Scheme.preimage_comp, Opens.toScheme_presheaf_obj, Hom.app_eq_appLE, comp_appLE, Opens.ι_appLE, eqToHom_op,
Opens.toScheme_presheaf_map, eqToHom_unop] at this
have e : U.ι ⁻¹ᵁ (U.ι ''ᵁ V) = V := Opens.ext (Set.preimage_image_eq _ Subtype.coe_injective)
have e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ U.ι ⁻¹ᵁ U.ι ''ᵁ V := by rw [e]
simp only [Opens.toScheme_presheaf_obj, Hom.app_eq_appLE, eqToHom_op, Hom.appLE_map]
rw [← (f ∣_ U).appLE_map' _ e', ← (f ∣_ U).map_appLE' _ e]
simp only [Opens.toScheme_presheaf_obj, eqToHom_eq_homOfLE, Opens.toScheme_presheaf_map, Quiver.Hom.unop_op,
Hom.opensFunctor_map_homOfLE]
rw [this, Hom.appLE_map, Hom.appLE_map, Hom.appLE_map]
