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.

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.

Equations

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

noncomputable def AlgebraicGeometry.moduleSpecΓFunctor {R : CommRingCat} : CategoryTheory.Functor (Spec { carrier := ↑R, commRing := R.commRing }).Modules (ModuleCat ↑R)

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

Equations

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

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

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

Equations

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

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

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

Equations

• AlgebraicGeometry.tilde M = { val := AlgebraicGeometry.moduleStructurePresheaf ↑R ↑M, isSheaf := ⋯ }

noncomputable def AlgebraicGeometry.tilde.modulesSpecToSheafIso {R : CommRingCat} (M : ModuleCat ↑R) : (modulesSpecToSheaf.obj (tilde M)).val ≅ 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.

Equations

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

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 localiation map when U = D(f).

Equations

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

@[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)))

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

Equations

• AlgebraicGeometry.tilde.instModuleCarrierCarrierStalkAbPresheaf M x = inferInstanceAs (Module ↑R ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.moduleStructurePresheaf ↑R ↑M).presheaf 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.

Equations

• AlgebraicGeometry.tilde.toStalk M x = ModuleCat.ofHom (AlgebraicGeometry.StructureSheaf.toStalkₗ (↑R) (↑M) 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.

Equations

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

@[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)).val.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)).val.obj (Opposite.op U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toOpen M U) (CategoryTheory.CategoryStruct.comp ((modulesSpecToSheaf.map (tilde.map f)).val.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 { carrier := ↑R, commRing := R.commRing }).Modules

Tilde as a functor

Equations

• AlgebraicGeometry.tilde.functor R = { obj := AlgebraicGeometry.tilde, map := fun {X Y : ModuleCat ↑R} => AlgebraicGeometry.tilde.map, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

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.

Equations

• AlgebraicGeometry.tilde.isoTop M = CategoryTheory.asIso (AlgebraicGeometry.tilde.toOpen 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 { carrier := ↑R, commRing := R.commRing }).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 { carrier := ↑R, commRing := R.commRing }).Modules) : tilde ((modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)) ⟶ M

This is the counit of the tilde-Gamma adjunction.

Equations

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

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

theorem AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc {R : CommRingCat} (M : (Spec { carrier := ↑R, commRing := R.commRing }).Modules) (U : (Spec { carrier := ↑R, commRing := R.commRing }).Opens) {Z : ModuleCat ↑R} (h : (modulesSpecToSheaf.obj M).val.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Γ).val.app (Opposite.op U)) h) = CategoryTheory.CategoryStruct.comp ((modulesSpecToSheaf.obj M).val.map (CategoryTheory.homOfLE ⋯).op) h

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

This is the counit of the tilde-Gamma adjunction.

Equations

• AlgebraicGeometry.Scheme.Modules.fromTildeΓNatTrans = { app := AlgebraicGeometry.Scheme.Modules.fromTildeΓ, naturality := ⋯ }

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.

Equations

• AlgebraicGeometry.tilde.toTildeΓNatIso = CategoryTheory.NatIso.ofComponents AlgebraicGeometry.tilde.isoTop ⋯

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

The tilde-Gamma adjuntion.

Equations

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

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

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.

Equations

• AlgebraicGeometry.tilde.fullyFaithfulFunctor = AlgebraicGeometry.tilde.adjunction.fullyFaithfulLOfIsIsoUnit

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

@[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

Equations

• @ModuleCat.tilde = @AlgebraicGeometry.tilde

@[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 localiation map when U = D(f).

Equations

• @ModuleCat.Tilde.toOpen = @AlgebraicGeometry.tilde.toOpen

@[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.

Equations

• @ModuleCat.Tilde.toStalk = @AlgebraicGeometry.tilde.toStalk