Module stalks and pullback

This file equips stalks of scheme-module sheaves with their canonical local-ring module structure. These stalk functors preserve finite limits and coproducts and jointly reflect isomorphisms. Pullback followed by a module stalk is identified with the source stalk followed by extension of scalars along the local-ring map.

The pullback comparison is first constructed for presheaves via a private module-valued skyscraper adjunction, then transported through module sheafification. It assumes no flatness and does not assert that pullback along an arbitrary scheme morphism is exact.

Main definitions

AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor bundles a sheaf stalk over the local ring.

Main results

• AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_preservesSmallColimits preserves arbitrary small colimits; the existing coproduct theorem is its discrete-diagram specialization.
• AlgebraicGeometry.Scheme.Modules.preservesFiniteLimits_of_stalkwise reduces finite-limit preservation to module stalks.
• AlgebraicGeometry.Scheme.Modules.presheafModulePullbackStalkIso compares presheaf pullback with extension of scalars on stalks.
• AlgebraicGeometry.Scheme.Modules.pullbackStalkIso gives the corresponding comparison for module sheaves.
• AlgebraicGeometry.Scheme.Modules.exists_sheaf_with_stalk realizes any local-ring module as a sheaf stalk.

Implementation notes

The realization sheaf is the sheafification of the existing module skyscraper presheaf. The proof uses the module-stalk adjunction and its comparison with the underlying additive stalk.

References

The stalk and skyscraper constructions extend Mathlib's module-sheaf and topological-sheaf APIs at the pinned revision.

Tags

module stalk, scheme module sheaf, pullback, skyscraper

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.moduleStalkRingCocone (X : Scheme) (x : ↥X) : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion x).op.comp (CategoryTheory.Functor.comp X.presheaf (CategoryTheory.forget₂ CommRingCat RingCat)))

The cocone of underlying rings whose point is the local ring of X at x, specialized from the topological module-stalk construction.

Equations

• AlgebraicGeometry.Scheme.Modules.moduleStalkRingCocone X x = PresheafOfModules.stalkRingCocone (↑X.toPresheafedSpace) X.presheaf x

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.moduleStalkRingIsColimit (X : Scheme) (x : ↥X) : CategoryTheory.Limits.IsColimit (moduleStalkRingCocone X x)

Definitional specialization of PresheafOfModules.stalkRingIsColimit to the scheme's structure presheaf.

Equations

• AlgebraicGeometry.Scheme.Modules.moduleStalkRingIsColimit X x = PresheafOfModules.stalkRingIsColimit (↑X.toPresheafedSpace) X.presheaf x

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.neighborhoodModuleStalkFunctor (X : Scheme) (x : ↥X) : CategoryTheory.Functor (_root_.PresheafOfModules ((TopologicalSpace.OpenNhds.inclusion x).op.comp X.ringCatSheaf.obj)) (ModuleCat ↑(X.presheaf.stalk x))

Definitional specialization of PresheafOfModules.commNeighborhoodStalkFunctor, using the scheme's local ring as its scalar ring.

Equations

• AlgebraicGeometry.Scheme.Modules.neighborhoodModuleStalkFunctor X x = PresheafOfModules.commNeighborhoodStalkFunctor (↑X.toPresheafedSpace) X.presheaf x

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.presheafModuleStalkFunctor (X : Scheme) (x : ↥X) : CategoryTheory.Functor (_root_.PresheafOfModules X.ringCatSheaf.obj) (ModuleCat ↑(X.presheaf.stalk x))

The stalk of a presheaf of modules, bundled over the local ring.

Equations

• AlgebraicGeometry.Scheme.Modules.presheafModuleStalkFunctor X x = PresheafOfModules.commStalkFunctor (↑X.toPresheafedSpace) X.presheaf x

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor (X : Scheme) (x : ↥X) : CategoryTheory.Functor X.Modules (ModuleCat ↑(X.presheaf.stalk x))

The stalk of a sheaf of modules, bundled as a module over the local ring.

This refines the usual abelian-group-valued stalk functor with the canonical local-ring module structure.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.presheafModuleStalkToSheafificationApp (X : Scheme) (x : ↥X) (M : _root_.PresheafOfModules X.ringCatSheaf.obj) : (presheafModuleStalkFunctor X x).obj M ⟶ (moduleStalkFunctor X x).obj ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).obj M)

The module map on stalks induced by the unit from a presheaf of modules to its module sheafification.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.presheafModuleStalkToSheafificationApp_isIso (X : Scheme) (x : ↥X) (M : _root_.PresheafOfModules X.ringCatSheaf.obj) : CategoryTheory.IsIso (presheafModuleStalkToSheafificationApp X x M)

Module sheafification induces an isomorphism on every module stalk.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.presheafModuleStalkSheafificationIso (X : Scheme) (x : ↥X) : presheafModuleStalkFunctor X x ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).comp (moduleStalkFunctor X x)

Taking a module stalk commutes naturally with module sheafification.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.moduleStalkForgetIso (X : Scheme) (x : ↥X) : (moduleStalkFunctor X x).comp (CategoryTheory.forget₂ (ModuleCat ↑(X.presheaf.stalk x)) AddCommGrpCat) ≅ (SheafOfModules.toSheaf X.ringCatSheaf).comp ((TopCat.Sheaf.forget AddCommGrpCat ↑X.toPresheafedSpace).comp (TopCat.Presheaf.stalkFunctor AddCommGrpCat x))

Forgetting the local-ring action on AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor recovers the usual stalk of the underlying sheaf of abelian groups.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_preservesSmallColimits (X : Scheme) (x : ↥X) (J : Type u) [CategoryTheory.Category.{u, u} J] : CategoryTheory.Limits.PreservesColimitsOfShape J (moduleStalkFunctor X x)

Arbitrary small colimits of module sheaves are preserved by the underlying additive sheaf stalk. The forgetful module functor reflects and preserves the corresponding module colimits.

theorem AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_preservesColimitsOfShape (X : Scheme) (x : ↥X) (I : Type u) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) (moduleStalkFunctor X x)

The established indexed-coproduct API is the discrete-diagram case of general small-colimit preservation.

theorem AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_preservesFiniteColimits (X : Scheme) (x : ↥X) : CategoryTheory.Limits.PreservesFiniteColimits (moduleStalkFunctor X x)

Finite colimits follow from the general small-colimit theorem after transporting a finite indexing category to the scheme's universe.

theorem AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_preservesFiniteLimits (X : Scheme) (x : ↥X) : CategoryTheory.Limits.PreservesFiniteLimits (moduleStalkFunctor X x)

Taking the stalk of a sheaf of modules preserves finite limits.

theorem AlgebraicGeometry.Scheme.Modules.moduleStalkFunctors_jointlyReflectIsomorphisms (X : Scheme) : CategoryTheory.JointlyReflectIsomorphisms (moduleStalkFunctor X)

The family of module-stalk functors over all points detects isomorphisms of sheaves of modules.

theorem AlgebraicGeometry.Scheme.Modules.preservesFiniteLimits_of_stalkwise {X Y : Scheme} (F : CategoryTheory.Functor Y.Modules X.Modules) (hF : ∀ (x : ↥X), CategoryTheory.Limits.PreservesFiniteLimits (F.comp (moduleStalkFunctor X x))) : CategoryTheory.Limits.PreservesFiniteLimits F

A functor between categories of module sheaves preserves finite limits as soon as all of its composites with module-stalk functors do.

def AlgebraicGeometry.Scheme.Modules.neighborhoodRingHom {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : (TopologicalSpace.OpenNhds.inclusion (f x)).op.comp Y.ringCatSheaf.obj ⟶ (TopologicalSpace.OpenNhds.map f.base x).op.comp ((TopologicalSpace.OpenNhds.inclusion x).op.comp X.ringCatSheaf.obj)

The ring map on neighborhood diagrams induced by a scheme morphism at a point. Its component over V ∋ f(x) is the restriction of the scheme map from Γ(V, 𝒪_Y) to Γ(f⁻¹(V), 𝒪_X).

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.neighborhoodModulePullback {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : CategoryTheory.Functor (_root_.PresheafOfModules ((TopologicalSpace.OpenNhds.inclusion (f x)).op.comp Y.ringCatSheaf.obj)) (_root_.PresheafOfModules ((TopologicalSpace.OpenNhds.inclusion x).op.comp X.ringCatSheaf.obj))

Pullback of modules along the induced map between the two neighborhood ring diagrams.

Equations

• AlgebraicGeometry.Scheme.Modules.neighborhoodModulePullback f x = PresheafOfModules.pullback (AlgebraicGeometry.Scheme.Modules.neighborhoodRingHom f x)

theorem AlgebraicGeometry.Scheme.Modules.neighborhoodRingHom_comp_stalkCocone {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) (V : (TopologicalSpace.OpenNhds (f x))ᵒᵖ) : CategoryTheory.CategoryStruct.comp ((moduleStalkRingCocone Y (f x)).ι.app V) ((CategoryTheory.forget₂ CommRingCat RingCat).map (Hom.stalkMap f x)) = CategoryTheory.CategoryStruct.comp ((neighborhoodRingHom f x).app V) ((moduleStalkRingCocone X x).ι.app ((TopologicalSpace.OpenNhds.map f.base x).op.obj V))

The neighborhood ring map commutes with the two stalk cocones through the scheme morphism's map on local rings.

noncomputable def AlgebraicGeometry.Scheme.Modules.constNeighborhoodPushforwardIsoApp {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) (N : ModuleCat ↑(X.presheaf.stalk x)) : ((PresheafOfModules.constFunctor (moduleStalkRingCocone X x)).comp (PresheafOfModules.pushforward (neighborhoodRingHom f x))).obj N ≅ ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.stalkMap f x))).comp (PresheafOfModules.constFunctor (moduleStalkRingCocone Y (f x)))).obj N

Objectwise comparison between the two right adjoints used to compute pullback followed by the neighborhood colimit.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.constNeighborhoodPushforwardIso {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : (PresheafOfModules.constFunctor (moduleStalkRingCocone X x)).comp (PresheafOfModules.pushforward (neighborhoodRingHom f x)) ≅ (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.stalkMap f x))).comp (PresheafOfModules.constFunctor (moduleStalkRingCocone Y (f x)))

Natural comparison between constant neighborhood modules followed by pushforward and restriction of scalars followed by constant modules.

Equations

• AlgebraicGeometry.Scheme.Modules.constNeighborhoodPushforwardIso f x = CategoryTheory.NatIso.ofComponents (AlgebraicGeometry.Scheme.Modules.constNeighborhoodPushforwardIsoApp f x) ⋯

noncomputable def AlgebraicGeometry.Scheme.Modules.neighborhoodModulePullbackStalkIso {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : (neighborhoodModulePullback f x).comp (neighborhoodModuleStalkFunctor X x) ≅ (neighborhoodModuleStalkFunctor Y (f x)).comp (ModuleCat.extendScalars (CommRingCat.Hom.hom (Hom.stalkMap f x)))

Pulling a module diagram back from neighborhoods of f(x) and taking its neighborhood colimit agrees with first taking the stalk at f(x) and then extending scalars along the local-ring map at x.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackStalkPresheafIso {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : (pullback f).comp (moduleStalkFunctor X x) ≅ (toPresheafOfModules Y).comp ((PresheafOfModules.pullback (Hom.toRingCatSheafHom f).hom).comp (presheafModuleStalkFunctor X x))

After taking a stalk, module-sheaf pullback reduces canonically to presheaf-module pullback. The sheafification step disappears because it induces an isomorphism on every module stalk.

Equations

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

The presheaf pullback-to-stalk comparison

The implementation constructs the module-valued skyscraper presheaf at a point, proves that it is right adjoint to the module stalk functor, and uses uniqueness of left adjoints to identify pullback followed by a stalk with extension of scalars along the induced local-ring map. The construction is kept private; the resulting canonical comparison is exposed below.

noncomputable def AlgebraicGeometry.Scheme.Modules.presheafModulePullbackStalkIso {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : (PresheafOfModules.pullback (Hom.toRingCatSheafHom f).hom).comp (presheafModuleStalkFunctor X x) ≅ (presheafModuleStalkFunctor Y (f x)).comp (ModuleCat.extendScalars (CommRingCat.Hom.hom (Hom.stalkMap f x)))

Pulling back a presheaf of modules and then taking its stalk agrees with first taking the stalk at the image point and extending scalars along the induced local-ring map.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackStalkIso {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : (pullback f).comp (moduleStalkFunctor X x) ≅ (moduleStalkFunctor Y (f x)).comp (ModuleCat.extendScalars (CommRingCat.Hom.hom (Hom.stalkMap f x)))

Pulling back a sheaf of modules and then taking its stalk agrees with first taking the stalk at the image point and extending scalars along the induced local-ring map.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.exists_sheaf_with_stalk (X : Scheme) (x : ↥X) (N : ModuleCat ↑(X.presheaf.stalk x)) : ∃ (M : X.Modules), Nonempty ((moduleStalkFunctor X x).obj M ≅ N)

Every module over the local ring at a point is the stalk of some sheaf of modules. The sheaf is obtained by sheafifying the existing module skyscraper presheaf.