lift_app — Mathlib

English

For an open immersion f: X → Y, there is a canonical isomorphism between the global sections on X with the whole top open set and the sections on Y over opensRange f.

Русский

Для открытого вложения f: X → Y существует каноническое изоморфизм глобальных секций X над ⊤ и секций Y над opensRange f.

LaTeX

$$$ \Gamma(X, \top) \cong \Gamma(Y, f.opensRange) $$$

Lean4

theorem lift_app {X Y U : Scheme.{u}} (f : U ⟶ Y) (g : X ⟶ Y) [IsOpenImmersion f] (H) (V : U.Opens) :
    (IsOpenImmersion.lift f g H).app V =
      (f.appIso V).inv ≫
        g.app (f ''ᵁ V) ≫
          X.presheaf.map
            (eqToHom <|
                IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux _ _ _ (IsOpenImmersion.lift_fac f g H).symm V).op :=
  IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq _ _ _ (lift_fac _ _ _).symm _

Похожие утверждения