English
For an open immersion f: X → Y and an open set U in Y, there is a canonical isomorphism between the global sections on X restricted to f⁻¹(U) and the sections of Y on U restricted to opensRange f.
Русский
Для открытого вложения f: X → Y и открытого множества U в Y существует каноническое изоморфизм между глобальными секциями X над f⁻¹(U) и секциями Y над U, ограниченными opensRange f.
LaTeX
$$$ \Gamma(X, f^{-1}U) \cong \Gamma(Y, f.opensRange \cap U) $$$
Lean4
/-- The `fg` argument is to avoid nasty stuff about dependent types. -/
theorem app_eq_appIso_inv_app_of_comp_eq {X Y U : Scheme.{u}} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X) (H : fg = f ≫ g)
[h : IsOpenImmersion g] (V : U.Opens) :
f.app V =
(g.appIso V).inv ≫
fg.app (g ''ᵁ V) ≫ Y.presheaf.map (eqToHom <| IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux f g fg H V).op :=
by
subst H
rw [Scheme.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc, ← Functor.map_comp, ←
op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans, eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id,
Category.comp_id]
