basicOpenSectionsToAffine — Mathlib

English

The image of PrimeSpectrum.basicOpen f under fromSpec is X.basicOpen f.

Русский

Образ PrimeSpectrum.basicOpen f под от fromSpec равен X.basicOpen f.

LaTeX

$$$h_U.fromSpec ''^U (\mathrm{PrimeSpectrum.basicOpen}(f)) = X.basicOpen f$$$

Lean4

/-- Given an affine open U and some `f : U`,
this is the canonical map `Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(f))`
This is an isomorphism, as witnessed by an `IsIso` instance. -/
def basicOpenSectionsToAffine : Γ(X, X.basicOpen f) ⟶ Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) :=
  hU.fromSpec.c.app (op <| X.basicOpen f) ≫
    (Spec Γ(X, U)).presheaf.map (eqToHom <| (hU.fromSpec_preimage_basicOpen f).symm).op

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