basicOpenIsoAway — Mathlib

English

There is a canonical isomorphism between the degree-zero part of the away localization (A away) and the global sections on Proj of the basic open D_+(f).

Русский

Существует канонический изоморфизм между нулевой степенью локализации Away и глобальными секциями на Proj в базовом открытом D_+(f).

LaTeX

$$$(A_f)_0 \cong \Gamma( \operatorname{Proj}(\mathcal{A}), D_+(f) )$$$

Lean4

/-- The canonical isomorphism `(A_f)₀ ≅ Γ(Proj A, D₊(f))`
when `f` is homogeneous of positive degree. -/
@[simps! -isSimp hom]
noncomputable def basicOpenIsoAway : CommRingCat.of (Away 𝒜 f) ≅ Γ(Proj 𝒜, basicOpen 𝒜 f) :=
  have : IsIso (awayToSection 𝒜 f) := by
    have := basicOpenToSpec_app_top 𝒜 f
    rw [← Iso.inv_comp_eq, Iso.eq_comp_inv] at this
    rw [← this, ← basicOpenIsoSpec_hom 𝒜 f f_deg hm]
    infer_instance
  asIso (awayToSection 𝒜 f)

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