English
Given affine opens X, Y and a morphism f: X ⟶ Y, the Spec.map of the appLE morphism is compatible with fromSpec and f; i.e., Spec.map (X.presheaf.map f) ≫ hU.fromSpec equals hV.fromSpec ≫ f in the appropriate setting.
Русский
Для аффинных открытых подмножеств X, Y и морфизма f: X ⟶ Y, отображение Spec.map совместимо с fromSpec и f; то есть Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec ≫ f в соответствующей конфигурации.
LaTeX
$$Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec ≫ f$$
Lean4
@[reassoc]
theorem Spec_map_appLE_fromSpec (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V)
(i : V ≤ f ⁻¹ᵁ U) : Spec.map (f.appLE U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f :=
by
have : IsAffine U := hU
simp only [IsAffineOpen.fromSpec, Category.assoc, isoSpec_inv]
simp_rw [← Scheme.homOfLE_ι _ i]
rw [Category.assoc, ← morphismRestrict_ι, ← Category.assoc _ (f ∣_ U) U.ι, ← @Scheme.isoSpec_inv_naturality_assoc, ←
Spec.map_comp_assoc, ← Spec.map_comp_assoc, Scheme.comp_appTop, morphismRestrict_appTop, Scheme.homOfLE_appTop,
Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map, Scheme.Hom.appLE_map, Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]
