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) → ModuleCat.Tilde.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 (ModuleCat.Tilde.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 (ModuleCat.Tilde.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) → ModuleCat.Tilde.Localizations M ↑x) : (ModuleCat.Tilde.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 ((fun (x : ↥V) => ⟨↑x, ⋯⟩) x) = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) m

noncomputable instance ModuleCat.Tilde.instModuleαCommRingObjOppositeOpensTopologicalSpaceTopCommRingCatValStructureSheafLocalizationsValMemUnop {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)) (ModuleCat.Tilde.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 : ModuleCat.Tilde.Localizations M ↑x) : r • m = ↑r x • m

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)) → ModuleCat.Tilde.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)

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

Equations

• M.instAddCommGroupObjOppositeOpensαTopologicalSpaceTopValTildeInType U = inferInstanceAs (AddCommGroup ↥(ModuleCat.Tilde.sectionsSubmodule M U))

noncomputable instance ModuleCat.instModuleαRingObjOppositeOpensTopologicalSpaceCarrierCommRingCatSpecOfRingCatValRingCatSheafTopTildeInType {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 : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V ⟶ U) (s : ↑(M.tildeInModuleCat.obj (Opposite.op U))) (x : ↥V) : ↑((M.tildeInModuleCat.map i.op) s) x = ↑s ((fun (x : ↥V) => ⟨↑x, ⋯⟩) 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

def ModuleCat.Tilde.toOpen {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : ModuleCat.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 : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V ⟶ U) : CategoryTheory.CategoryStruct.comp (ModuleCat.Tilde.toOpen M U) (M.tildeInModuleCat.map i.op) = ModuleCat.Tilde.toOpen M V

noncomputable def ModuleCat.Tilde.toStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : ModuleCat.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)) : ModuleCat.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 = LocalizedModule.lift x.asIdeal.primeCompl (ModuleCat.Tilde.toStalk M x) ⋯

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) ⟶ ModuleCat.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 = { 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 ⟶ ModuleCat.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) (ModuleCat.Tilde.stalkToFiberLinearMap M x) = ModuleCat.Tilde.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))) : (ModuleCat.Tilde.stalkToFiberLinearMap M x) ((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 (ModuleCat.Tilde.toOpen M U) (M.tildeInModuleCat.germ U x hx) = ModuleCat.Tilde.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 (ModuleCat.Tilde.toOpen M U) (CategoryTheory.CategoryStruct.comp (M.tildeInModuleCat.germ U x hx) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.Tilde.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.forget (ModuleCat R)).obj (ModuleCat.of R ↑M)) : (M.tildeInModuleCat.germ U x✝ hx) ((ModuleCat.Tilde.toOpen M U) x) = (ModuleCat.Tilde.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 (ModuleCat.Tilde.toStalk M x) (ModuleCat.Tilde.stalkToFiberLinearMap M x) = 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 : ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl ↑M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.Tilde.toStalk M x) (CategoryTheory.CategoryStruct.comp (ModuleCat.Tilde.stalkToFiberLinearMap M x) h) = CategoryTheory.CategoryStruct.comp (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) : (ModuleCat.Tilde.stalkToFiberLinearMap M x) ((ModuleCat.Tilde.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) : ↑(ModuleCat.Tilde.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), ModuleCat.Tilde.const M f g V hg = (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) : (M.tildeInModuleCat.map i) (ModuleCat.Tilde.const M f g U hu) = ModuleCat.Tilde.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) : (ModuleCat.Tilde.localizationToStalk M x) (LocalizedModule.mk f s) = (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯) (ModuleCat.Tilde.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 ≅ ModuleCat.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)) : (ModuleCat.Tilde.stalkIso M x).inv = ModuleCat.Tilde.localizationToStalk M x

@[simp]

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

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

Equations

• ⋯ = ⋯