English
The preimage of an open under resLE is the pullback of the corresponding inclusions; explicitly, the preimage of O under resLE equals V.ι^{-1} of f^{-1}ᵁ U.ι''O.
Русский
Обратный образ открытого пространства под resLE равен вытяжке соответствующих включений; явное равенство: предобраз O через resLE равен V.ι^{-1} (f^{-1}ᵁ U.ι '' O).
LaTeX
$$$f.resLE U V e^{-1}\!\_\! O = V.ι^{-1}\!\_\! (f^{-1}\!\_\! U.ι ''\! O)$$$
Lean4
theorem resLE_appLE {U : Y.Opens} {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U) (O : U.toScheme.Opens) (W : V.toScheme.Opens)
(e' : W ≤ resLE f U V e ⁻¹ᵁ O) :
(f.resLE U V e).appLE O W e' = f.appLE (U.ι ''ᵁ O) (V.ι ''ᵁ W) ((le_preimage_resLE_iff f e O W).mp e') :=
by
simp only [appLE, resLE, comp_coeBase, Opens.map_comp_obj, comp_app, morphismRestrict_app', homOfLE_leOfHom,
homOfLE_app, Category.assoc, Opens.toScheme_presheaf_map, Quiver.Hom.unop_op, opensFunctor_map_homOfLE]
rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
rfl
