appBasicOpenIsoAwayMap — Mathlib

English

If there is an inclusion i: V -> U with V = X.basicOpen f, then the localization is the same as localization at V.

Русский

Если существует вложение i: V → U и V = X.basicOpen f, то локализация совпадает с локализацией на V.

LaTeX

$$$@IsLocalization.Away\ f (X.presheaf.obj{ unop := V }).carrier$$$

Lean4

/-- `f.app (Y.basicOpen r)` is isomorphic to map induced on localizations
`Γ(Y, Y.basicOpen r) ⟶ Γ(X, X.basicOpen (f.app U r))` -/
def appBasicOpenIsoAwayMap {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (hU : IsAffineOpen U)
    (h : IsAffineOpen (f ⁻¹ᵁ U)) (r : Γ(Y, U)) :
    haveI := hU.isLocalization_basicOpen r
    haveI := h.isLocalization_basicOpen (f.app U r)
    Arrow.mk (f.app (Y.basicOpen r)) ≅
      Arrow.mk
        (CommRingCat.ofHom
          (IsLocalization.Away.map Γ(Y, Y.basicOpen r) Γ(X, X.basicOpen (f.app U r)) (f.app U).hom r)) :=
  Arrow.isoMk (Iso.refl _) (X.presheaf.mapIso (eqToIso (by simp)).op) <| by simp [hU.app_basicOpen_eq_away_map f h]

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