Γ_restrict_isLocalization — Mathlib

English

Final formulation: when i: V ⟶ U with V = X.basicOpen f, the Away map identifies with the localization to V.

Русский

Окончательная формулировка: когда i: V ⟶ U с V = X.basicOpen f, Away map идентифицируется с локализацией к V.

LaTeX

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

Lean4

instance _root_.AlgebraicGeometry.Γ_restrict_isLocalization (X : Scheme.{u}) [IsAffine X] (r : Γ(X, ⊤)) :
    IsLocalization.Away r Γ(X.basicOpen r, ⊤) :=
  (isAffineOpen_top X).isLocalization_of_eq_basicOpen r _ (Opens.isOpenEmbedding_obj_top _)

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