Documentation

DerivedAlgGeo.AlgebraicGeometry.Modules.Coherent.Affine.BasicOpen

Coherent pullback on an affine basic open #

The coherent pullback along the open immersion D(r) ↪ Spec R agrees, up to a natural isomorphism, with pullback along Spec (Localization.Away r) → Spec R followed by the equivalence induced by basicOpenIsoSpecAway r. This is an ordinary, underived functor comparison; it does not identify arbitrary ring localizations with open immersions.

source
noncomputable def AlgebraicGeometry.Coh.pullbackBasicOpenIsoSpecAway {R : CommRingCat} (r : ↑R) :
pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r)) ≅ (pullback (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))))).comp (pullback (basicOpenIsoSpecAway r).hom)

Restriction of coherent sheaves to D(r) is the affine localization-away pullback, transported across basicOpenIsoSpecAway r. No Noetherian hypothesis is needed for this comparison of ordinary pullback functors.

Equations
  • One or more equations did not get rendered due to their size.
Instances For