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
.
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
Instances For
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
Instances For
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.
Instances For
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
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.
Instances For
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)
Instances For
Equations
- M.instAddCommGroupObjOppositeOpensαTopologicalSpaceTopValTildeInType U = inferInstanceAs (AddCommGroup ↥(ModuleCat.Tilde.sectionsSubmodule M U))
Equations
- One or more equations did not get rendered due to their size.
M^~
as a sheaf of 𝒪_{Spec R}
-modules
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is M^~
as a sheaf of R
-modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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)
Instances For
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) ⋯