The localisation criterion for the affine comparison theorem

For a commutative ring R, the affine comparison identifies a quasi-coherent sheaf on Spec R with the sheaf associated to its global sections. This is Stacks 01IA. The pinned Mathlib v4.32.1 supplies the quasi-coherent case as AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_of_isQuasicoherent in Mathlib/AlgebraicGeometry/Modules/Tilde.lean.

Mathlib also defines AlgebraicGeometry.IsLocalizing and proves AlgebraicGeometry.isIso_fromTildeΓ_iff_isLocalizing for arbitrary module sheaves. This file retains the explicit map AlgebraicGeometry.Scheme.Modules.basicOpenRestriction and states the same criterion as AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_iff_isLocalizedModule. The latter is a definitional restatement of the upstream criterion, not a second general theorem.

Main definitions

• AlgebraicGeometry.Scheme.Modules.basicOpenRestriction is restriction of global sections to the basic open D(f).

Main results

• AlgebraicGeometry.isIso_fromTildeΓ_app_basicOpen — the component of the counit at D(f) is an isomorphism under the hypothesis that restriction is a localisation at the powers of f.
• AlgebraicGeometry.isIso_fromTildeΓ_of_isLocalizedModule — the implication from localization of every basic-open restriction to invertibility of the counit (the right-to-left direction of the upstream criterion).
• AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_tilde — the base case, M = N^~, where that hypothesis holds. It is both the starting point of the general argument and the check that the hypothesis is satisfiable rather than vacuous.
• AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_of_isIso — the converse of the reduction, obtained by transporting the base case along the counit.
• AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_of_presentation — a presentation on Spec R makes restriction to each basic open a localization.
• AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_iff_isLocalizedModule — the upstream AlgebraicGeometry.isIso_fromTildeΓ_iff_isLocalizing restated using AlgebraicGeometry.Scheme.Modules.basicOpenRestriction. Its statement is IsIso M.fromTildeΓ ↔ ∀ f, IsLocalizedModule (powers f) (restriction to D(f)). This is the statement to quote when using the local restriction map.

Implementation notes

Mathlib's AlgebraicGeometry.IsLocalizing is defined on AlgebraicGeometry.modulesSpecToSheaf.obj M; its condition is definitionally equal to the quantified AlgebraicGeometry.Scheme.Modules.basicOpenRestriction condition. Mathlib's AlgebraicGeometry.isIso_fromTildeΓ_iff_isLocalizing proves the equivalence for that predicate. AlgebraicGeometry.Scheme.Modules.fromTildeΓ is built by TopCat.Sheaf.restrictHomEquivHom along PrimeSpectrum.isBasis_basic_opens, with its component at D(f) given by IsLocalizedModule.lift. Mathlib's AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app records the resulting triangle: the component composed with AlgebraicGeometry.tilde.toOpen is the restriction map. Since AlgebraicGeometry.tilde.toOpen at D(f) is a localisation at Submonoid.powers f — Mathlib supplies that instance — the component is the comparison map between two candidate localisations. Under the localization hypothesis, the component theorem proves this map is an isomorphism. The separate converse and if-and-only-if statement concern the whole counit, not an unconditional equivalence for a single component. The whole-counit result is AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_iff_isLocalizedModule.

Neither Mathlib's general criterion nor the local-map restatement needs quasi-coherence. Mathlib states AlgebraicGeometry.Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen for an arbitrary M : (AlgebraicGeometry.Spec R).Modules, not only for tildes. The quasi-coherent application is provided by Mathlib's pinned instance; the local-map formulation remains available when a caller supplies the localization hypotheses directly.

Relation to the local bridges

AlgebraicGeometry.Modules.Affine.Gluing documents the current division of work: Mathlib owns the finite-cover proof of the quasi-coherent comparison, while the local file retains the restriction-to-chart linear equivalence and wrappers for DerivedAlgGeo's explicit quasi-coherent-data and localization APIs. The local whole-counit theorem restates the upstream AlgebraicGeometry.isIso_fromTildeΓ_iff_isLocalizing using this file's restriction map. In particular, AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_of_isQuasicoherent is a bridge to the upstream result, not a second proof of it. The scheme/slice transport used by these local bridges is in AlgebraicGeometry.Modules.Restriction.OpenImmersion.

References

• Stacks, Tag 01IA.
• See the affine and projective spectrum placement map for pinned Mathlib source links.

Tags

affine scheme, quasi-coherent modules, global sections, basic-open localization, tilde, counit

noncomputable def AlgebraicGeometry.Scheme.Modules.basicOpenRestriction {R : CommRingCat} (M : (Spec R).Modules) (f : ↑R) : (modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤) ⟶ (modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))

Restriction of the global sections of an 𝒪_{Spec R}-module to the basic open D(f).

This is the map the affine comparison theorem asserts to be a localisation at Submonoid.powers f.

Equations

• M.basicOpenRestriction f = (AlgebraicGeometry.modulesSpecToSheaf.obj M).presheaf.map (CategoryTheory.homOfLE ⋯).op

theorem AlgebraicGeometry.Scheme.Modules.toOpen_comp_fromTildeΓ_app {R : CommRingCat} (M : (Spec R).Modules) (f : ↑R) : CategoryTheory.CategoryStruct.comp (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)) (PrimeSpectrum.basicOpen f)) ((modulesSpecToSheaf.map M.fromTildeΓ).hom.app (Opposite.op (PrimeSpectrum.basicOpen f))) = M.basicOpenRestriction f

The counit composed with tilde.toOpen is restriction — Mathlib's toOpen_fromTildeΓ_app, phrased through basicOpenRestriction.

instance AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_tilde {R : CommRingCat} (N : ModuleCat ↑R) (f : ↑R) : IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom ((tilde N).basicOpenRestriction f))

The base case: for M = N^~ the restriction to D(f) is a localisation.

AlgebraicGeometry.tilde.toOpen N ⊤ is an isomorphism, and its composite with restriction to D(f) is AlgebraicGeometry.tilde.toOpen N D(f) by AlgebraicGeometry.tilde.toOpen_res. Thus the restriction inherits the localization property Mathlib proves for AlgebraicGeometry.tilde.toOpen N D(f).

This is what the general statement — the hypothesis of AlgebraicGeometry.isIso_fromTildeΓ_of_isLocalizedModule — has to be reduced to for a quasi-coherent M. It also checks that the hypothesis is satisfiable rather than vacuous: feeding this lemma to the reduction recovers CategoryTheory.IsIso (AlgebraicGeometry.tilde N).fromTildeΓ, which Mathlib knows independently.

theorem AlgebraicGeometry.isIso_fromTildeΓ_app_basicOpen {R : CommRingCat} (M : (Spec R).Modules) (f : ↑R) [IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (M.basicOpenRestriction f))] : CategoryTheory.IsIso ((modulesSpecToSheaf.map M.fromTildeΓ).hom.app (Opposite.op (PrimeSpectrum.basicOpen f)))

The component of the counit at D(f) is an isomorphism when restriction to D(f) is a localisation at the powers of f.

Both tilde.toOpen and the restriction are then localisations of Γ(M, ⊤) at the same submonoid, and the component is the comparison map between them.

theorem AlgebraicGeometry.isIso_fromTildeΓ_of_isLocalizedModule {R : CommRingCat} (M : (Spec R).Modules) (h : ∀ (f : ↑R), IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (M.basicOpenRestriction f))) : CategoryTheory.IsIso M.fromTildeΓ

The counit is an isomorphism as soon as restriction to every basic open is a localisation.

This is a basiswise reduction of the affine comparison. Mathlib's pinned quasi-coherent instance proves the comparison for quasi-coherent modules by a finite basic-open-cover argument; this criterion also applies to an arbitrary module sheaf when its localization hypotheses are supplied directly.

theorem AlgebraicGeometry.Scheme.Modules.basicOpenRestriction_naturality {R : CommRingCat} {M N : (Spec R).Modules} (φ : M ⟶ N) (f : ↑R) : CategoryTheory.CategoryStruct.comp (M.basicOpenRestriction f) ((modulesSpecToSheaf.map φ).hom.app (Opposite.op (PrimeSpectrum.basicOpen f))) = CategoryTheory.CategoryStruct.comp ((modulesSpecToSheaf.map φ).hom.app (Opposite.op ⊤)) (N.basicOpenRestriction f)

basicOpenRestriction is a presheaf restriction map, so it is natural in M.

theorem AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_of_isIso {R : CommRingCat} (M : (Spec R).Modules) [CategoryTheory.IsIso M.fromTildeΓ] (f : ↑R) : IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (M.basicOpenRestriction f))

The converse of AlgebraicGeometry.isIso_fromTildeΓ_of_isLocalizedModule.

If M is in the essential image of ~ — equivalently, if its counit is an isomorphism — then restriction to each basic open is a localisation, by transporting AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_tilde across that isomorphism.

theorem AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestriction_of_presentation {R : CommRingCat} (M : (Spec R).Modules) (P : SheafOfModules.Presentation M) (f : ↑R) : IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (M.basicOpenRestriction f))

A presentation on Spec R makes the counit an isomorphism by Mathlib's AlgebraicGeometry.isIso_fromTildeΓ_of_presentation; the localization criterion then shows that each basic-open restriction is a localization.

theorem AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_iff_isLocalizedModule {R : CommRingCat} (M : (Spec R).Modules) : CategoryTheory.IsIso M.fromTildeΓ ↔ ∀ (f : ↑R), IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (M.basicOpenRestriction f))

The affine comparison, as a characterisation.

The counit is an isomorphism exactly when restriction to every basic open is a localisation. Both directions are now available, so this is the statement to quote.