English
Restricting the global-section morphism to a basic open yields a diagram that is canonically equivalent to the basic open construction using the corresponding basic-open map of global sections.
Русский
Ограничение морфизма глобальных секций до базовой открытой подмножества даёт каноническое эквивалентное диаграмме базовых открытых схем на основе соответствующего отображения базовой открытой области глобальных секций.
LaTeX
$$$\text{restr}_{\text{basicOpen}}(fromOfGlobalSections(...)) = \mathrm{hom}\;\circ\; toBasicOpenOfGlobalSections(...)$$$
Lean4
theorem fromOfGlobalSections_morphismRestrict {r : A} {n : ℕ} (hn : 0 < n) (hr : r ∈ 𝒜 n) :
(fromOfGlobalSections 𝒜 f hf) ∣_ (basicOpen 𝒜 r) =
(Scheme.isoOfEq _ (fromOfGlobalSections_preimage_basicOpen _ _ _ hn hr)).hom ≫
toBasicOpenOfGlobalSections 𝒜 f rfl hn hr :=
by
rw [← Iso.inv_comp_eq, ← cancel_mono (basicOpen 𝒜 r).ι]
simp only [Scheme.isoOfEq_inv, Category.assoc, morphismRestrict_ι, Scheme.homOfLE_ι_assoc, fromOfGlobalSections]
exact (openCoverOfMapIrrelevantEqTop 𝒜 f hf).ι_glueMorphisms _ _ ⟨_, _, hn, hr⟩
