Limits of internal module objects

For a monoidal category acting on a category D, the forgetful functor from modules over a monoid object creates limits. The action on a limiting object is determined by its composites with the limit projections. No preservation of limits by the action functors is required. In particular, this constructs limits of spectra presented as modules over a sphere monoid in symmetric sequences.

The construction follows Monad.ForgetCreatesLimits in Mathlib's CategoryTheory/Monad/Limits: lift the action through the limiting cone, and verify its laws and the equivariance of cone lifts after composing with each projection.

def CategoryTheory.Mod.isLimitOfForget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone F) (hc : Limits.IsLimit ((forget A).mapCone c)) : Limits.IsLimit c

A cone of module objects is limiting whenever its underlying cone is limiting.

theorem CategoryTheory.Mod.isLimitOfForget_lift_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone F) (hc : Limits.IsLimit ((forget A).mapCone c)) (s : Limits.Cone F) : ((isLimitOfForget F c hc).lift s).hom = hc.lift ((forget A).mapCone s)

The universal lift is the lift of the underlying limiting cone.

@[instance_reducible]

def CategoryTheory.Mod.LimitConstruction.action {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone (F.comp (forget A))) (hc : Limits.IsLimit c) : ModObj A c.pt

The action on the point of an underlying limiting cone.

theorem CategoryTheory.Mod.LimitConstruction.action_smul_π {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone (F.comp (forget A))) (hc : Limits.IsLimit c) (j : J) : CategoryStruct.comp ModObj.smul (c.π.app j) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A (c.π.app j)) ModObj.smul

Each underlying projection is equivariant for the lifted action.

def CategoryTheory.Mod.LimitConstruction.cone {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone (F.comp (forget A))) (hc : Limits.IsLimit c) : Limits.Cone F

The module cone lifted from an underlying limiting cone.

theorem CategoryTheory.Mod.LimitConstruction.cone_pt_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone (F.comp (forget A))) (hc : Limits.IsLimit c) : (cone F c hc).pt.X = c.pt

The underlying object of the lifted cone is the specified limit object.

theorem CategoryTheory.Mod.LimitConstruction.cone_π_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone (F.comp (forget A))) (hc : Limits.IsLimit c) (j : J) : CategoryStruct.comp (eqToHom ⋯) ((cone F c hc).π.app j).hom = c.π.app j

The lifted projections agree with the specified projections after carrier transport.

def CategoryTheory.Mod.LimitConstruction.forgetConeIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone (F.comp (forget A))) (hc : Limits.IsLimit c) : (forget A).mapCone (cone F c hc) ≅ c

Forgetting the lifted cone recovers the specified underlying cone.

def CategoryTheory.Mod.LimitConstruction.isLimit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor J (Mod D A)) (c : Limits.Cone (F.comp (forget A))) (hc : Limits.IsLimit c) : Limits.IsLimit (cone F c hc)

The cone lifted from an underlying limit is itself a limit.

@[instance_reducible]

noncomputable instance CategoryTheory.Mod.forgetCreatesLimits {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] : CreatesLimitsOfSize.{v₃, u₃, v₂, v₂, max u₂ v₂, u₂} (forget A)

The forgetful functor creates limits for every monoidal left action.

instance CategoryTheory.Mod.hasLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {J : Type u₃} [Category.{v₃, u₃} J] [Limits.HasLimitsOfShape J D] : Limits.HasLimitsOfShape J (Mod D A)

Module objects inherit every shape of limits existing in their ambient category.

instance CategoryTheory.Mod.hasLimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] [Limits.HasLimitsOfSize.{v₃, u₃, v₂, u₂} D] : Limits.HasLimitsOfSize.{v₃, u₃, v₂, max u₂ v₂} (Mod D A)

Module objects inherit limits of every size existing in their ambient category.