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.

@[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) : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M)

(Implementation). The module structure on AddCommGrpCat.FilteredColimits.colimit.

Equations

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

@[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) : Module ↑cR.pt ↑cM.pt

Given a cofiltered diagram of rings R, and a module M over R, this is the colim R-module structure of colim M.

Equations

• CategoryTheory.Limits.IsColimit.module R M H hcR hcM = Module.compHom (↑cM.pt) (hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)).ringCatIsoToRingEquiv.toRingHom

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

@[instance_reducible]

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

@[instance_reducible]

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