English
The image of a basic open via the restriction equals the basic open of X after transporting along topIso.
Русский
Образ базового открытого через ограничение равен базовому открытому X после переноса по topIso.
LaTeX
$$$ U.ι ''ᵁ (U.toScheme.basicOpen r) = X.basicOpen r $$$
Lean4
@[simp]
theorem homOfLE_app {U V : X.Opens} (e : U ≤ V) (W : Opens V) :
(X.homOfLE e).app W = X.presheaf.map (homOfLE <| X.ι_image_homOfLE_le_ι_image e W).op :=
by
have e₁ := Scheme.congr_app (X.homOfLE_ι e) (V.ι ''ᵁ W)
have : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W := W.map_functor_eq (U := V)
have e₂ := (X.homOfLE e).naturality (eqToIso this).hom.op
have e₃ := e₂.symm.trans e₁
dsimp at e₃ ⊢
rw [← IsIso.eq_comp_inv, ← Functor.map_inv, ← Functor.map_comp] at e₃
rw [e₃, ← Functor.map_comp]
congr 1
