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 ofR
-modules from the stalk ofM^~
atx
to the localization ofM
at the prime ideal corresponding tox
.
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 = ModuleCat.ofHom (LocalizedModule.lift x.asIdeal.primeCompl (ModuleCat.Tilde.toStalk M x).hom ⋯)
Instances For
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' := ⋯ }
Instances For
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.
Instances For
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, ⋯⟩, ⋯⟩
Instances For
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 := ⋯ }