English
For an affine open U and V with a relation h ≤ V, the appTop of hU.fromSpec at V equals the appropriate composite of presheaf maps and inverses of ΓSpecIso; this expresses how fromSpec behaves with respect to inclusions of opens.
Русский
Для аффинного открытого множества U и V с условием h ≤ V отображение appTop fromSpec на V задаёт соответствующую композицию отображений прешифса и обратного Γ-spec изоморфизма; выражает поведение fromSpec при вложениях открытых подмножеств.
LaTeX
$$hU.fromSpec.app V = X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec _).presheaf.map (homOfLE le_top).op$$
Lean4
theorem fromSpec_app_of_le (V : X.Opens) (h : U ≤ V) :
hU.fromSpec.app V =
X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec _).presheaf.map (homOfLE le_top).op :=
by
have : U.ι ⁻¹ᵁ V = ⊤ := eq_top_iff.mpr fun x _ ↦ h x.2
rw [IsAffineOpen.fromSpec, Scheme.comp_app, Scheme.Opens.ι_app, Scheme.app_eq _ this, ← Scheme.Hom.appTop,
IsAffineOpen.isoSpec_inv_appTop]
simp only [Scheme.Opens.toScheme_presheaf_map, Scheme.Opens.topIso_hom, Category.assoc, ← X.presheaf.map_comp_assoc]
rfl
