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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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