English
A membership relation between opens translates into a preimage inclusion criterion for resLE via theopens mapping and the inclusion maps.
Русский
Членство между открытыми множествами переводится в критерий включения через прообраз для resLE с помощью отображений открытий.
LaTeX
$$$W \le (f.resLE\, U\, V\, e)^{-1}\!O \iff V.ι''W \le f^{-1}\!U.ι''O$$$
Lean4
/-- `f.resLE U V` induces `f.appLE U V` on global sections. -/
noncomputable def arrowResLEAppIso (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U) :
Arrow.mk ((f.resLE U V e).appTop) ≅ Arrow.mk (f.appLE U V e) :=
Arrow.isoMk U.topIso V.topIso <|
by
simp only [Arrow.mk_left, Arrow.mk_right, Functor.id_obj, Scheme.Opens.topIso_hom, eqToHom_op, Arrow.mk_hom,
Scheme.Hom.map_appLE]
rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]