Module structure on stalks #
Let M be a presheaf of R-modules on a topological space. We endow M.presheaf.stalk x with
an R.stalk x-module structure.
The key characterizing lemma is PresheafOfModules.germ_smul, which describes the compatibility
of the scalar action and TopCat.Presheaf.germ.
noncomputable def
CategoryTheory.Limits.colimit.smul
{C : Type u_1}
[SmallCategory C]
[IsFiltered C]
(R : Functor C RingCat)
(M : Functor C Ab)
[(i : C) β Module β(R.obj i) β(M.obj i)]
(H :
β {i j : C} (f : i βΆ j) (r : β(R.obj i)) (m : β(M.obj i)),
(ConcreteCategory.hom (M.map f)) (r β’ m) = (ConcreteCategory.hom (R.map f)) r β’ (ConcreteCategory.hom (M.map f)) m)
(r : (R.comp (forget RingCat)).ColimitType)
(m : (M.comp (forget Ab)).ColimitType)
:
(M.comp (forget Ab)).ColimitType
(Implementation). The scalar multiplication function on ColimitType.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.filteredColimitsModule
{C : Type u_1}
[SmallCategory C]
[IsFiltered C]
(R : Functor C RingCat)
(M : Functor C Ab)
[(i : C) β Module β(R.obj i) β(M.obj i)]
(H :
β {i j : C} (f : i βΆ j) (r : β(R.obj i)) (m : β(M.obj i)),
(ConcreteCategory.hom (M.map f)) (r β’ m) = (ConcreteCategory.hom (R.map f)) r β’ (ConcreteCategory.hom (M.map f)) m)
:
(Implementation). The module structure on AddCommGrpCat.FilteredColimits.colimit.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.IsColimit.module
{C : Type u_1}
[SmallCategory C]
[IsFiltered C]
(R : Functor C RingCat)
(M : Functor C Ab)
[(i : C) β Module β(R.obj i) β(M.obj i)]
(H :
β {i j : C} (f : i βΆ j) (r : β(R.obj i)) (m : β(M.obj i)),
(ConcreteCategory.hom (M.map f)) (r β’ m) = (ConcreteCategory.hom (R.map f)) r β’ (ConcreteCategory.hom (M.map f)) m)
{cR : Cocone R}
(hcR : IsColimit cR)
{cM : Cocone M}
(hcM : IsColimit cM)
:
Given a cofiltered diagram of rings R, and a module M over R,
this is the colim R-module structure of colim M.
Equations
Instances For
theorem
CategoryTheory.Limits.IsColimit.ΞΉ_smul
{C : Type u_1}
[SmallCategory C]
[IsFiltered C]
(R : Functor C RingCat)
(M : Functor C Ab)
[(i : C) β Module β(R.obj i) β(M.obj i)]
(H :
β {i j : C} (f : i βΆ j) (r : β(R.obj i)) (m : β(M.obj i)),
(ConcreteCategory.hom (M.map f)) (r β’ m) = (ConcreteCategory.hom (R.map f)) r β’ (ConcreteCategory.hom (M.map f)) m)
{cR : Cocone R}
(hcR : IsColimit cR)
{cM : Cocone M}
(hcM : IsColimit cM)
(i : C)
(r : β(R.obj i))
(m : β(M.obj i))
:
(ConcreteCategory.hom (cM.ΞΉ.app i)) (r β’ m) = (ConcreteCategory.hom (cR.ΞΉ.app i)) r β’ (ConcreteCategory.hom (cM.ΞΉ.app i)) m
noncomputable instance
PresheafOfModules.instModuleCarrierStalkRingCatCarrierAbPresheafOpensCarrier
{X : TopCat}
{R : TopCat.Presheaf RingCat X}
(M : PresheafOfModules R)
(x : βX)
:
Module β(R.stalk x) β(TopCat.Presheaf.stalk M.presheaf x)
Equations
theorem
PresheafOfModules.germ_ringCat_smul
{X : TopCat}
{R : TopCat.Presheaf RingCat X}
(M : PresheafOfModules R)
(x : βX)
(U : TopologicalSpace.Opens βX)
(hx : x β U)
(r : β(R.obj (Opposite.op U)))
(m : β(M.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) (r β’ m) = (CategoryTheory.ConcreteCategory.hom (R.germ U x hx)) r β’ (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) m
noncomputable instance
PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
{X : TopCat}
{R : TopCat.Presheaf CommRingCat X}
(M : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forgetβ CommRingCat RingCat)))
(x : βX)
:
Module β(R.stalk x) β(TopCat.Presheaf.stalk M.presheaf x)
Equations
theorem
PresheafOfModules.germ_smul
{X : TopCat}
{R : TopCat.Presheaf CommRingCat X}
(M : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forgetβ CommRingCat RingCat)))
(x : βX)
(U : TopologicalSpace.Opens βX)
(hx : x β U)
(r : β(R.obj (Opposite.op U)))
(m : β(M.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) (r β’ m) = (CategoryTheory.ConcreteCategory.hom (R.germ U x hx)) r β’ (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) m