English
Restriction preserves the compatibility of fromSpecStalkOfMem: applying restrict to f and evaluating at hx yields the same as evaluating at hU' hx on the original f.
Русский
Ограничение сохраняет совместимость fromSpecStalkOfMem: при применении restrict к f и обращении к hx получается то же самое, что в оригинальном f на hx через hU'.
LaTeX
$$$$ (f.restrict U hU hU').fromSpecStalkOfMem hx = f.fromSpecStalkOfMem (hU' hx) $$$$
Lean4
theorem fromSpecStalkOfMem_restrict (f : X.PartialMap Y) {U : X.Opens} (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) {x}
(hx : x ∈ U) : (f.restrict U hU hU').fromSpecStalkOfMem hx = f.fromSpecStalkOfMem (hU' hx) :=
by
dsimp only [fromSpecStalkOfMem, restrict, Scheme.Opens.fromSpecStalkOfMem]
have e : ⟨x, hU' hx⟩ = (X.homOfLE hU').base ⟨x, hx⟩ :=
by
rw [Scheme.homOfLE_base]
rfl
rw [Category.assoc, ← Spec_map_stalkMap_fromSpecStalk_assoc, ←
Spec_map_stalkSpecializes_fromSpecStalk (Inseparable.of_eq e).specializes, ←
TopCat.Presheaf.stalkCongr_inv _ (Inseparable.of_eq e)]
simp only [← Category.assoc, ← Spec.map_comp]
congr 3
rw [Iso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq, IsIso.eq_inv_comp,
stalkMap_congr_hom _ _ (X.homOfLE_ι hU').symm]
simp only [TopCat.Presheaf.stalkCongr_hom]
rw [← stalkSpecializes_stalkMap_assoc, stalkMap_comp]
