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.tildeInAddCommGrp : M^~ as a sheaf of abelian groups.
• ModuleCat.tilde : M^~ as a sheaf of 𝒪_{Spec R}-modules.

@[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αCommRingObjOppositeOpensTopologicalSpaceTopCommRingCatValStructureSheafLocalizationsValMemSetCoeUnop {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))

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

M^~ as a presheaf of abelian groups over Spec R

Equations

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

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

M^~ as a sheaf of abelian groups over Spec R

Equations

• M.tildeInAddCommGrp = { val := M.preTildeInAddCommGrp, cond := ⋯ }

noncomputable instance ModuleCat.instModuleαRingObjOppositeOpensTopologicalSpaceCarrierCommRingCatSpecOfRingCatValRingCatSheafAddCommGroupTopAddCommGrpTildeInAddCommGrp {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.tildeInAddCommGrp.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

• M.tilde = { val := { presheaf := M.tildeInAddCommGrp.val, module := inferInstance, map_smul := ⋯ }, isSheaf := ⋯ }