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.

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) ⋯