English
A universal formula for appLE of restricted morphisms: the value equals the composition of appLE on U-images, the restriction morphism, and the original appLE, with the appropriate le-maps composed.
Русский
Универсальная формула для appLE ограниченных морфизмов: значение равно композиции appLE по образом U, ограничение и исходный appLE с соответствующим образом круто.
LaTeX
$$$(f|_U).appLE\;V\;W\;e = f.appLE (U.ι''ᵁ V) ((f^{-1}ᵁ U).ι''ᵁ W) ((Set.image_mono e).trans (image_morphismRestrict_preimage f U V).le)$$$
Lean4
@[simp]
theorem morphismRestrict_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V W e) :
(f ∣_ U).appLE V W e =
f.appLE (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ((Set.image_mono e).trans (image_morphismRestrict_preimage f U V).le) :=
by rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map, Scheme.Hom.appLE_map]
