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

• ModuleCat.tildeInType : M^~ as a sheaf of types groups.
• ModuleCat.tilde : M^~ as a sheaf of 𝒪_{Spec R}-modules.
• ModuleCat.tilde.stalkIso: The isomorphism of R-modules from the stalk of M^~ at x to the localization of M at the prime ideal corresponding to x.

Technical note

To get the R-module structure on the stalks on M^~, we had to define ModuleCat.tildeInModuleCat, which is M^~ seen as sheaf of R-modules. We get it by applying a forgetful functor to ModuleCat.tilde M.

@[reducible, inline]

abbrev ModuleCat.Tilde.Localizations {R : Type u} [CommRing R] (M : ModuleCat R) (P : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : Type u

For an R-module M and a point P in Spec R, Localizations P is the localized module M at the prime ideal P.

Equations

• ModuleCat.Tilde.Localizations M P = LocalizedModule P.asIdeal.primeCompl ↑M

def ModuleCat.Tilde.isFraction {R : Type u} [CommRing R] (M : ModuleCat R) {U : TopologicalSpace.Opens (PrimeSpectrum R)} (f : (𝔭 : ↥U) → Localizations M ↑𝔭) : Prop

For any open subset U ⊆ Spec R, IsFraction is the predicate expressing that a function f : ∏_{x ∈ U}, Mₓ is such that for any 𝔭 ∈ U, f 𝔭 = m / s for some m : M and s ∉ 𝔭. In short f is a fraction on U.

Equations

• ModuleCat.Tilde.isFraction M f = ∃ (m : ↑M) (s : R), ∀ (x : ↥U), s ∉ (↑x).asIdeal ∧ s • f x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) m

def ModuleCat.Tilde.isFractionPrelocal {R : Type u} [CommRing R] (M : ModuleCat R) : TopCat.PrelocalPredicate (Localizations M)

The property of a function f : ∏_{x ∈ U}, Mₓ being a fraction is stable under restriction.

Equations

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

def ModuleCat.Tilde.isLocallyFraction {R : Type u} [CommRing R] (M : ModuleCat R) : TopCat.LocalPredicate (Localizations M)

For any open subset U ⊆ Spec R, IsLocallyFraction is the predicate expressing that a function f : ∏_{x ∈ U}, Mₓ is such that for any 𝔭 ∈ U, there exists an open neighbourhood V ∋ 𝔭, such that for any 𝔮 ∈ V, f 𝔮 = m / s for some m : M and s ∉ 𝔮. In short f is locally a fraction on U.

Equations

• ModuleCat.Tilde.isLocallyFraction M = (ModuleCat.Tilde.isFractionPrelocal M).sheafify

@[simp]

theorem ModuleCat.Tilde.isLocallyFraction_pred {R : Type u} [CommRing R] (M : ModuleCat R) {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} (f : (x : ↥U) → Localizations M ↑x) : (isLocallyFraction M).pred f = ∀ (y : ↥U), ∃ (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (_ : ↑y ∈ V) (i : V ⟶ U) (m : ↑M) (s : R), ∀ (x : ↥V), s ∉ (↑x).asIdeal ∧ s • f (i x) = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) m

noncomputable instance ModuleCat.Tilde.instModuleCarrierObjOppositeOpensCarrierTopCommRingCatValStructureSheafLocalizationsValMemUnop {R : Type u} [CommRing R] (M : ModuleCat R) (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) (x : ↥(Opposite.unop U)) : Module (↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj U)) (Localizations M ↑x)

Equations

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

@[simp]

theorem ModuleCat.Tilde.sections_smul_localizations_def {R : Type u} [CommRing R] (M : ModuleCat R) {U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ} (x : ↥(Opposite.unop U)) (r : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj U)) (m : Localizations M ↑x) : r • m = ↑r x • m

noncomputable def ModuleCat.Tilde.sectionsSubmodule {R : Type u} [CommRing R] (M : ModuleCat R) (U : (TopologicalSpace.Opens (PrimeSpectrum R))ᵒᵖ) : Submodule (↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj U)) ((x : ↥(Opposite.unop U)) → Localizations M ↑x)

For any R-module M and any open subset U ⊆ Spec R, M^~(U) is an 𝒪_{Spec R}(U)-submodule of ∏_{𝔭 ∈ U} M_𝔭.

Equations

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

def ModuleCat.tildeInType {R : Type u} [CommRing R] (M : ModuleCat R) : TopCat.Sheaf (Type u) (AlgebraicGeometry.PrimeSpectrum.Top R)

For any R-module M, TildeInType R M is the sheaf of set on Spec R whose sections on U are the dependent functions that are locally fractions. This is often denoted by M^~.

See also Tilde.isLocallyFraction.

Equations

• M.tildeInType = TopCat.subsheafToTypes (ModuleCat.Tilde.isLocallyFraction M)

noncomputable instance ModuleCat.instAddCommGroupObjOppositeOpensCarrierTopValTildeInType {R : Type u} [CommRing R] (M : ModuleCat R) (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) : AddCommGroup (M.tildeInType.val.obj U)

Equations

• M.instAddCommGroupObjOppositeOpensCarrierTopValTildeInType U = inferInstanceAs (AddCommGroup ↥(ModuleCat.Tilde.sectionsSubmodule M U))

noncomputable instance ModuleCat.instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecOfRingCatValRingCatSheafTopTildeInType {R : Type u} [CommRing R] (M : ModuleCat R) (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) : Module (↑((AlgebraicGeometry.Spec (CommRingCat.of R)).ringCatSheaf.val.obj U)) (M.tildeInType.val.obj U)

Equations

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

noncomputable def ModuleCat.tilde {R : Type u} [CommRing R] (M : ModuleCat R) : (AlgebraicGeometry.Spec (CommRingCat.of R)).Modules

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

Equations

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

noncomputable def ModuleCat.tildeInModuleCat {R : Type u} [CommRing R] (M : ModuleCat R) : TopCat.Presheaf (ModuleCat R) (AlgebraicGeometry.PrimeSpectrum.Top R)

This is M^~ as a sheaf of R-modules.

Equations

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

@[simp]

theorem ModuleCat.Tilde.res_apply {R : Type u} [CommRing R] (M : ModuleCat R) (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V ⟶ U) (s : ↑(M.tildeInModuleCat.obj (Opposite.op U))) (x : ↥V) : ↑((CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.map i.op)) s) x = ↑s (i x)

theorem ModuleCat.Tilde.smul_section_apply {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (s : ↑(M.tildeInModuleCat.obj (Opposite.op U))) (x : ↥U) : ↑(r • s) x = r • ↑s x

theorem ModuleCat.Tilde.smul_stalk_no_nonzero_divisor {R : Type u} [CommRing R] (M : ModuleCat R) {x : PrimeSpectrum R} (r : ↥x.asIdeal.primeCompl) (st : ↑(M.tildeInModuleCat.stalk x)) (hst : ↑r • st = 0) : st = 0

noncomputable def ModuleCat.Tilde.toOpen {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : of R ↑M ⟶ M.tildeInModuleCat.obj (Opposite.op U)

If U is an open subset of Spec R, this is the morphism of R-modules from M to M^~(U).

Equations

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

@[simp]

theorem ModuleCat.Tilde.toOpen_res {R : Type u} [CommRing R] (M : ModuleCat R) (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V ⟶ U) : CategoryTheory.CategoryStruct.comp (toOpen M U) (M.tildeInModuleCat.map i.op) = toOpen M V

noncomputable def ModuleCat.Tilde.toStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : of R ↑M ⟶ M.tildeInModuleCat.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

• ModuleCat.Tilde.toStalk M x = CategoryTheory.CategoryStruct.comp (ModuleCat.Tilde.toOpen M ⊤) (M.tildeInModuleCat.germ ⊤ x True.intro)

theorem ModuleCat.Tilde.isUnit_toStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (r : ↥x.asIdeal.primeCompl) : IsUnit ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r)

noncomputable def ModuleCat.Tilde.localizationToStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : of R (LocalizedModule x.asIdeal.primeCompl ↑M) ⟶ M.tildeInModuleCat.stalk x

The morphism of R-modules from the localization of M at the prime ideal corresponding to x to the stalk of M^~ at x.

Equations

• ModuleCat.Tilde.localizationToStalk M x = ModuleCat.ofHom (LocalizedModule.lift x.asIdeal.primeCompl (ModuleCat.Hom.hom (ModuleCat.Tilde.toStalk M x)) ⋯)

noncomputable def ModuleCat.Tilde.openToLocalization {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens (PrimeSpectrum R)) (x : PrimeSpectrum R) (hx : x ∈ U) : M.tildeInModuleCat.obj (Opposite.op U) ⟶ of R (LocalizedModule x.asIdeal.primeCompl ↑M)

The ring homomorphism that takes a section of the structure sheaf of R on the open set U, implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates the section on the point corresponding to a given prime ideal.

Equations

• ModuleCat.Tilde.openToLocalization M U x hx = ModuleCat.ofHom { toFun := fun (s : ↑(M.tildeInModuleCat.obj (Opposite.op U))) => ↑s ⟨x, hx⟩, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ModuleCat.Tilde.stalkToFiberLinearMap {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : M.tildeInModuleCat.stalk x ⟶ of R (LocalizedModule x.asIdeal.primeCompl ↑M)

The morphism of R-modules from the stalk of M^~ at x to the localization of M at the prime ideal of R corresponding to x.

Equations

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

@[simp]

theorem ModuleCat.Tilde.germ_comp_stalkToFiberLinearMap {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (M.tildeInModuleCat.germ U x hx) (stalkToFiberLinearMap M x) = openToLocalization M U x hx

@[simp]

theorem ModuleCat.Tilde.stalkToFiberLinearMap_germ {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x ∈ U) (s : ↑(M.tildeInModuleCat.obj (Opposite.op U))) : (Hom.hom (stalkToFiberLinearMap M x)) ((CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.germ U x hx)) s) = ↑s ⟨x, hx⟩

@[simp]

theorem ModuleCat.Tilde.toOpen_germ {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (toOpen M U) (M.tildeInModuleCat.germ U x hx) = toStalk M x

@[simp]

theorem ModuleCat.Tilde.toOpen_germ_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x ∈ U) {Z : ModuleCat R} (h : M.tildeInModuleCat.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (toOpen M U) (CategoryTheory.CategoryStruct.comp (M.tildeInModuleCat.germ U x hx) h) = CategoryTheory.CategoryStruct.comp (toStalk M x) h

@[simp]

theorem ModuleCat.Tilde.toOpen_germ_apply {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x ∈ U) (x✝ : CategoryTheory.ToType (of R ↑M)) : (CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (toOpen M U)) x✝) = (CategoryTheory.ConcreteCategory.hom (toStalk M x)) x✝

@[simp]

theorem ModuleCat.Tilde.toStalk_comp_stalkToFiberLinearMap {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : CategoryTheory.CategoryStruct.comp (toStalk M x) (stalkToFiberLinearMap M x) = ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl ↑M)

@[simp]

theorem ModuleCat.Tilde.toStalk_comp_stalkToFiberLinearMap_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) {Z : ModuleCat R} (h : of R (LocalizedModule x.asIdeal.primeCompl ↑M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toStalk M x) (CategoryTheory.CategoryStruct.comp (stalkToFiberLinearMap M x) h) = CategoryTheory.CategoryStruct.comp (ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl ↑M)) h

theorem ModuleCat.Tilde.stalkToFiberLinearMap_toStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (m : ↑M) : (Hom.hom (stalkToFiberLinearMap M x)) ((CategoryTheory.ConcreteCategory.hom (toStalk M x)) m) = LocalizedModule.mk m 1

def ModuleCat.Tilde.const {R : Type u} [CommRing R] (M : ModuleCat R) (m : ↑M) (r : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, r ∈ x.asIdeal.primeCompl) : ↑(M.tildeInModuleCat.obj (Opposite.op U))

If U is an open subset of Spec R, m is an element of M and r is an element of R that is invertible on U (i.e. does not belong to any prime ideal corresponding to a point in U), this is m / r seen as a section of M^~ over U.

Equations

• ModuleCat.Tilde.const M m r U hu = ⟨fun (x : ↥(Opposite.unop (Opposite.op U))) => LocalizedModule.mk m ⟨r, ⋯⟩, ⋯⟩

@[simp]

theorem ModuleCat.Tilde.const_apply {R : Type u} [CommRing R] (M : ModuleCat R) (m : ↑M) (r : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, r ∈ x.asIdeal.primeCompl) (x : ↥U) : ↑(const M m r U hu) x = LocalizedModule.mk m ⟨r, ⋯⟩

theorem ModuleCat.Tilde.exists_const {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (s : ↑(M.tildeInModuleCat.obj (Opposite.op U))) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x ∈ U) : ∃ (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (_ : x ∈ V) (i : V ⟶ U) (f : ↑M) (g : R) (hg : ∀ x ∈ V, g ∈ x.asIdeal.primeCompl), const M f g V hg = (CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.map i.op)) s

@[simp]

theorem ModuleCat.Tilde.res_const {R : Type u} [CommRing R] (M : ModuleCat R) (f : ↑M) (g : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl) (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hv : ∀ x ∈ V, g ∈ x.asIdeal.primeCompl) (i : Opposite.op U ⟶ Opposite.op V) : (CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.map i)) (const M f g U hu) = const M f g V hv

@[simp]

theorem ModuleCat.Tilde.localizationToStalk_mk {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (f : ↑M) (s : ↥x.asIdeal.primeCompl) : (Hom.hom (localizationToStalk M x)) (LocalizedModule.mk f s) = (CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯)) (const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

noncomputable def ModuleCat.Tilde.stalkIso {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : M.tildeInModuleCat.stalk x ≅ of R (LocalizedModule x.asIdeal.primeCompl ↑M)

The isomorphism of R-modules from the stalk of M^~ at x to the localization of M at the prime ideal corresponding to x.

Equations

• ModuleCat.Tilde.stalkIso M x = { hom := ModuleCat.Tilde.stalkToFiberLinearMap M x, inv := ModuleCat.Tilde.localizationToStalk M x, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem ModuleCat.Tilde.stalkIso_inv {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : (stalkIso M x).inv = localizationToStalk M x

@[simp]

theorem ModuleCat.Tilde.stalkIso_hom {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : (stalkIso M x).hom = stalkToFiberLinearMap M x

instance ModuleCat.Tilde.instIsLocalizedModulePrimeComplAsIdealCarrierOfStalkTildeInModuleCatHomToStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : IsLocalizedModule x.asIdeal.primeCompl (Hom.hom (toStalk M x))