Affine-comparison bridges retained after the gluing proof moved upstream

Mathlib v4.32.1 contains the full quasi-coherent affine comparison as AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_of_isQuasicoherent, with its finite-cover presentation argument in AlgebraicGeometry/Modules/Tilde.lean. This file retains local bridges and does not reprove that comparison.

Only two local bridges remain:

• the linear equivalence identifying sections of a restriction to Spec R[1/g] with sections over D(g), used by the finite-generation argument; and
• stable wrappers connecting the upstream comparison instance to DerivedAlgGeo's localization and explicit-quasi-coherent-data APIs.

No gluing theorem is duplicated here.

noncomputable def AlgebraicGeometry.Scheme.Modules.basicOpenSpecMap {R : CommRingCat} (g : ↑R) : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec R

The canonical open immersion Spec R[1/g] ⟶ Spec R.

Equations

• AlgebraicGeometry.Scheme.Modules.basicOpenSpecMap g = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g)))

instance AlgebraicGeometry.Scheme.Modules.instIsOpenImmersionBasicOpenSpecMap {R : CommRingCat} (g : ↑R) : IsOpenImmersion (basicOpenSpecMap g)

theorem AlgebraicGeometry.Scheme.Modules.basicOpenSpecMap_opensRange {R : CommRingCat} (g : ↑R) : Hom.opensRange (basicOpenSpecMap g) = PrimeSpectrum.basicOpen g

The range of Spec R[1/g] ⟶ Spec R is D(g).

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictBasicOpenTopLinearEquiv {R : CommRingCat} (M : (Spec R).Modules) (g : ↑R) : ↑((ModuleCat.restrictScalars (algebraMap (↑R) (Localization.Away g))).obj ((modulesSpecToSheaf.obj (M.restrict (basicOpenSpecMap g))).presheaf.obj (Opposite.op ⊤))) ≃ₗ[↑R] ↑((modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen g)))

Identify sections of the restriction to Spec R[1/g] over its top open with sections of the original sheaf over D(g), after restricting scalars to R.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_of_isQuasicoherent {R : CommRingCat} (M : (Spec R).Modules) [SheafOfModules.IsQuasicoherent M] (f : ↑R) : IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (M.basicOpenRestriction f))

For a quasi-coherent sheaf on an affine scheme, restriction to every basic open is the corresponding module localization.

theorem AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_of_quasicoherentData {R : CommRingCat} (M : (Spec R).Modules) (q : SheafOfModules.QuasicoherentData M) : CategoryTheory.IsIso M.fromTildeΓ

Explicit quasi-coherent presentation data suffices for the upstream affine comparison.