Construction of M^~

Given any commutative ring R and R-module M, we construct the sheaf M^~ of 𝒪_SpecR-modules such that M^~(U) is the set of dependent functions that are locally fractions.

Main definitions

• AlgebraicGeometry.tilde : M^~ as a sheaf of 𝒪_{Spec R}-modules.
• AlgebraicGeometry.tilde.adjunction : ~ is left adjoint to taking global sections.

noncomputable def AlgebraicGeometry.modulesSpecToSheaf {R : CommRingCat} : CategoryTheory.Functor (Spec R).Modules (TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace)

The forgetful functor from 𝒪_{Spec R} modules to sheaves of R-modules.

noncomputable def AlgebraicGeometry.moduleSpecΓFunctor {R : CommRingCat} : CategoryTheory.Functor (Spec (CommRingCat.of ↑R)).Modules (ModuleCat ↑R)

The global section functor for 𝒪_{Spec R} modules

def AlgebraicGeometry.SpecModulesToSheafFullyFaithful {R : CommRingCat} : modulesSpecToSheaf.FullyFaithful

The forgetful functor from 𝒪_{Spec R} modules to sheaves of R-modules is fully faithful.

noncomputable def AlgebraicGeometry.tilde {R : CommRingCat} (M : ModuleCat ↑R) : (Spec R).Modules

M^~ as a sheaf of 𝒪_{Spec R}-modules

noncomputable def AlgebraicGeometry.tilde.modulesSpecToSheafIso {R : CommRingCat} (M : ModuleCat ↑R) : (modulesSpecToSheaf.obj (tilde M)).obj ≅ structurePresheafInModuleCat ↑R ↑M

(Implementation). The image of tilde under modulesSpecToSheaf is isomorphic to structurePresheafInModuleCat. They are defeq as types but the Smul instance are not defeq.

noncomputable def AlgebraicGeometry.tilde.toOpen {R : CommRingCat} (M : ModuleCat ↑R) (U : (Spec R).Opens) : M ⟶ (modulesSpecToSheaf.obj (tilde M)).presheaf.obj (Opposite.op U)

The map from M to Γ(M, U). This is a localization map when U = D(f).

@[simp]

theorem AlgebraicGeometry.tilde.toOpen_res {R : CommRingCat} (M : ModuleCat ↑R) (U V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑R)) (i : V ⟶ U) : CategoryTheory.CategoryStruct.comp (toOpen M U) ((modulesSpecToSheaf.obj (tilde M)).presheaf.map i.op) = toOpen M V

@[simp]

theorem AlgebraicGeometry.tilde.toOpen_res_assoc {R : CommRingCat} (M : ModuleCat ↑R) (U V : TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑R)) (i : V ⟶ U) {Z : ModuleCat ↑R} (h : (modulesSpecToSheaf.obj (tilde M)).presheaf.obj (Opposite.op V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toOpen M U) (CategoryTheory.CategoryStruct.comp ((modulesSpecToSheaf.obj (tilde M)).presheaf.map i.op) h) = CategoryTheory.CategoryStruct.comp (toOpen M V) h

instance AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R) : IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (toOpen M (PrimeSpectrum.basicOpen f)))

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.tilde.instModuleCarrierCarrierStalkAbPresheaf {R : CommRingCat} (M : ModuleCat ↑R) (x : ↑(PrimeSpectrum.Top ↑R)) : Module ↑R ↑((tilde M).presheaf.stalk x)

noncomputable def AlgebraicGeometry.tilde.toStalk {R : CommRingCat} (M : ModuleCat ↑R) (x : ↑(PrimeSpectrum.Top ↑R)) : ModuleCat.of ↑R ↑M ⟶ ModuleCat.of ↑R ↑((tilde M).presheaf.stalk x)

If x is a point of Spec R, this is the morphism of R-modules from M to the stalk of M^~ at x.

instance AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk {R : CommRingCat} (M : ModuleCat ↑R) (x : ↑(PrimeSpectrum.Top ↑R)) : IsLocalizedModule x.asIdeal.primeCompl (ModuleCat.Hom.hom (toStalk M x))

noncomputable def AlgebraicGeometry.tilde.map {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N) : tilde M ⟶ tilde N

The tilde construction is functorial.

@[simp]

theorem AlgebraicGeometry.tilde.map_id {R : CommRingCat} {M : ModuleCat ↑R} : tilde.map (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (tilde M)

theorem AlgebraicGeometry.tilde.map_id_assoc {R : CommRingCat} {M : ModuleCat ↑R} {Z : (Spec R).Modules} (h : tilde M ⟶ Z) : CategoryTheory.CategoryStruct.comp (tilde.map (CategoryTheory.CategoryStruct.id M)) h = h

@[simp]

theorem AlgebraicGeometry.tilde.map_comp {R : CommRingCat} {M N P : ModuleCat ↑R} (f : M ⟶ N) (g : N ⟶ P) : tilde.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (tilde.map f) (tilde.map g)

theorem AlgebraicGeometry.tilde.map_comp_assoc {R : CommRingCat} {M N P : ModuleCat ↑R} (f : M ⟶ N) (g : N ⟶ P) {Z : (Spec R).Modules} (h : tilde P ⟶ Z) : CategoryTheory.CategoryStruct.comp (tilde.map (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (tilde.map f) (CategoryTheory.CategoryStruct.comp (tilde.map g) h)

@[simp]

theorem AlgebraicGeometry.tilde.toOpen_map_app {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N) (U : TopologicalSpace.Opens (PrimeSpectrum ↑R)) : CategoryTheory.CategoryStruct.comp (toOpen M U) ((modulesSpecToSheaf.map (tilde.map f)).hom.app (Opposite.op U)) = CategoryTheory.CategoryStruct.comp f (toOpen N U)

@[simp]

theorem AlgebraicGeometry.tilde.toOpen_map_app_assoc {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N) (U : TopologicalSpace.Opens (PrimeSpectrum ↑R)) {Z : ModuleCat ↑R} (h : (modulesSpecToSheaf.obj (tilde N)).obj.obj (Opposite.op U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toOpen M U) (CategoryTheory.CategoryStruct.comp ((modulesSpecToSheaf.map (tilde.map f)).hom.app (Opposite.op U)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (toOpen N U) h)

noncomputable def AlgebraicGeometry.tilde.functor (R : CommRingCat) : CategoryTheory.Functor (ModuleCat ↑R) (Spec (CommRingCat.of ↑R)).Modules

Tilde as a functor

@[simp]

theorem AlgebraicGeometry.tilde.functor_map (R : CommRingCat) {X✝ Y✝ : ModuleCat ↑R} (f : X✝ ⟶ Y✝) : (tilde.functor R).map f = tilde.map f

@[simp]

theorem AlgebraicGeometry.tilde.functor_obj (R : CommRingCat) (M : ModuleCat ↑R) : (tilde.functor R).obj M = tilde M

instance AlgebraicGeometry.tilde.isIso_toOpen_top {R : CommRingCat} {M : ModuleCat ↑R} : CategoryTheory.IsIso (toOpen M ⊤)

noncomputable def AlgebraicGeometry.tilde.isoTop {R : CommRingCat} (M : ModuleCat ↑R) : M ≅ (modulesSpecToSheaf.obj (tilde M)).presheaf.obj (Opposite.op ⊤)

The isomorphism between the global sections of M^~ and M.

@[simp]

theorem AlgebraicGeometry.tilde.isoTop_hom {R : CommRingCat} (M : ModuleCat ↑R) : (isoTop M).hom = toOpen M ⊤

theorem AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen {R : CommRingCat} (M : (Spec (CommRingCat.of ↑R)).Modules) (f : ↑R) : IsUnit ((algebraMap (↑R) (Module.End ↑R ↑((modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))))) f)

noncomputable def AlgebraicGeometry.Scheme.Modules.fromTildeΓ {R : CommRingCat} (M : (Spec (CommRingCat.of ↑R)).Modules) : tilde ((modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)) ⟶ M

This is the counit of the tilde-Gamma adjunction.

theorem AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app {R : CommRingCat} (M : (Spec (CommRingCat.of ↑R)).Modules) (U : (Spec (CommRingCat.of ↑R)).Opens) : CategoryTheory.CategoryStruct.comp (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)) U) ((modulesSpecToSheaf.map M.fromTildeΓ).hom.app (Opposite.op U)) = (modulesSpecToSheaf.obj M).obj.map (CategoryTheory.homOfLE ⋯).op

theorem AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc {R : CommRingCat} (M : (Spec (CommRingCat.of ↑R)).Modules) (U : (Spec (CommRingCat.of ↑R)).Opens) {Z : ModuleCat ↑R} (h : (modulesSpecToSheaf.obj M).obj.obj (Opposite.op U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)) U) (CategoryTheory.CategoryStruct.comp ((modulesSpecToSheaf.map M.fromTildeΓ).hom.app (Opposite.op U)) h) = CategoryTheory.CategoryStruct.comp ((modulesSpecToSheaf.obj M).obj.map (CategoryTheory.homOfLE ⋯).op) h

noncomputable def AlgebraicGeometry.Scheme.Modules.fromTildeΓNatTrans {R : CommRingCat} : moduleSpecΓFunctor.comp (tilde.functor R) ⟶ CategoryTheory.Functor.id (Spec (CommRingCat.of ↑R)).Modules

This is the counit of the tilde-Gamma adjunction.

noncomputable def AlgebraicGeometry.tilde.toTildeΓNatIso {R : CommRingCat} : CategoryTheory.Functor.id (ModuleCat ↑R) ≅ (tilde.functor R).comp moduleSpecΓFunctor

tilde.isoTop bundled as a natural isomorphism. This is the unit of the tilde-Gamma adjunction.

noncomputable def AlgebraicGeometry.tilde.adjunction {R : CommRingCat} : tilde.functor R ⊣ moduleSpecΓFunctor

The tilde-Gamma adjunction.

instance AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction {R : CommRingCat} : CategoryTheory.IsIso tilde.adjunction.unit

noncomputable def AlgebraicGeometry.tilde.fullyFaithfulFunctor {R : CommRingCat} : (tilde.functor R).FullyFaithful

The tilde functor is fully faithful. We will later show that the essential image is exactly quasi-coherent modules.

instance AlgebraicGeometry.instFullModuleCatCarrierModulesSpecOfFunctor {R : CommRingCat} : (tilde.functor R).Full

instance AlgebraicGeometry.instFaithfulModuleCatCarrierModulesSpecOfFunctor {R : CommRingCat} : (tilde.functor R).Faithful

instance AlgebraicGeometry.instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor {R : CommRingCat} : (tilde.functor R).IsLeftAdjoint

instance AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor {R : CommRingCat} : (tilde.functor R).Additive

@[simp]

theorem AlgebraicGeometry.tilde.map_zero {R : CommRingCat} {M N : ModuleCat ↑R} : tilde.map 0 = 0

@[simp]

theorem AlgebraicGeometry.tilde.map_add {R : CommRingCat} {M N : ModuleCat ↑R} (f g : M ⟶ N) : tilde.map (f + g) = tilde.map f + tilde.map g

@[simp]

theorem AlgebraicGeometry.tilde.map_sub {R : CommRingCat} {M N : ModuleCat ↑R} (f g : M ⟶ N) : tilde.map (f - g) = tilde.map f - tilde.map g

@[simp]

theorem AlgebraicGeometry.tilde.map_neg {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N) : tilde.map (-f) = -tilde.map f

theorem AlgebraicGeometry.isIso_fromTildeΓ_iff {R : CommRingCat} {M : (Spec R).Modules} : CategoryTheory.IsIso M.fromTildeΓ ↔ (tilde.functor R).essImage M

noncomputable def AlgebraicGeometry.tildeSelf {R : CommRingCat} : tilde (ModuleCat.of ↑R ↑R) ≅ SheafOfModules.unit (Spec R).ringCatSheaf

Tilde of R as an R-module is isomorphic to the structure sheaf 𝒪_{Spec R}.

instance AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf {R : CommRingCat} : CategoryTheory.IsIso (Scheme.Modules.fromTildeΓ (SheafOfModules.unit (Spec R).ringCatSheaf))

noncomputable def AlgebraicGeometry.tildeFinsupp {R : CommRingCat} (ι : Type u) : tilde (ModuleCat.of (↑R) (ι →₀ ↑R)) ≅ SheafOfModules.free ι

Tilde of direct sums of R as an R-module is isomorphic to the free sheaf.

instance AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat {R : CommRingCat} (ι : Type u) : CategoryTheory.IsIso (Scheme.Modules.fromTildeΓ (SheafOfModules.free ι))

noncomputable def AlgebraicGeometry.presentationTilde {R : CommRingCat} (M : ModuleCat ↑R) (s : Set ↑M) (hs : Submodule.span (↑R) s = ⊤) (t : Set (↑s →₀ ↑R)) (ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker) : SheafOfModules.Presentation (tilde M)

Given a presentation of a module M, we may construct an associated presentation of M^~.

instance AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde {R : CommRingCat} (M : ModuleCat ↑R) : SheafOfModules.IsQuasicoherent (tilde M)

theorem AlgebraicGeometry.isIso_fromTildeΓ_of_presentation {R : CommRingCat} (M : (Spec R).Modules) (P : SheafOfModules.Presentation M) : CategoryTheory.IsIso M.fromTildeΓ

@[deprecated AlgebraicGeometry.tilde (since := "2026-02-11")]

def ModuleCat.tilde {R : CommRingCat} (M : ModuleCat ↑R) : (AlgebraicGeometry.Spec R).Modules

Alias of AlgebraicGeometry.tilde.

---

M^~ as a sheaf of 𝒪_{Spec R}-modules

@[deprecated AlgebraicGeometry.tilde.toOpen (since := "2026-02-11")]

def ModuleCat.Tilde.toOpen {R : CommRingCat} (M : ModuleCat ↑R) (U : (AlgebraicGeometry.Spec R).Opens) : M ⟶ (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.obj (Opposite.op U)

Alias of AlgebraicGeometry.tilde.toOpen.

---

The map from M to Γ(M, U). This is a localization map when U = D(f).

@[deprecated AlgebraicGeometry.tilde.toOpen_res (since := "2026-02-11")]

theorem ModuleCat.Tilde.toOpen_res {R : CommRingCat} (M : ModuleCat ↑R) (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R)) (i : V ⟶ U) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen M U) ((AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.map i.op) = AlgebraicGeometry.tilde.toOpen M V

Alias of AlgebraicGeometry.tilde.toOpen_res.

@[deprecated AlgebraicGeometry.tilde.toStalk (since := "2026-02-11")]

def ModuleCat.Tilde.toStalk {R : CommRingCat} (M : ModuleCat ↑R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R)) : of ↑R ↑M ⟶ of ↑R ↑((AlgebraicGeometry.tilde M).presheaf.stalk x)

Alias of AlgebraicGeometry.tilde.toStalk.

---

If x is a point of Spec R, this is the morphism of R-modules from M to the stalk of M^~ at x.