English
The application map of fromSpecStalk to a given open U is described by the germ and the isomorphism ΓSpecIso; it is computed via a standard pushforward of germs along the inclusion.
Русский
Применение fromSpecStalk к открытому U описывается через germ и ΓSpecIso; вычисляется через перенос газонов вдоль вложения.
LaTeX
$$X.fromSpecStalk x).app U = X.presheaf.germ U x hxU ≫ (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE le_top).op$$
Lean4
@[reassoc (attr := simp)]
theorem Spec_map_stalkMap_fromSpecStalk {x} : Spec.map (f.stalkMap x) ≫ Y.fromSpecStalk _ = X.fromSpecStalk x ≫ f :=
by
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
(isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ (f.base x)) isOpen_univ
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).2
rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV, IsAffineOpen.fromSpecStalk, ←
Spec.map_comp_assoc, Scheme.stalkMap_germ f _ x hxU, IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ←
X.presheaf.germ_res (homOfLE hVU) x hxV, Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.Spec_map_appLE_fromSpec]
