The category of R-modules has all colimits. #
From the existence of colimits in AddCommGroupCat, we deduce the existence of colimits
in ModuleCat R. This way, we get for free that the functor
forget₂ (ModuleCat R) AddCommGroupCat commutes with colimits.
Note that finite colimits can already be obtained from the instance Abelian (Module R).
TODO:
In fact, in ModuleCat R there is a much nicer model of colimits as quotients
of finitely supported functions, and we really should implement this as well.
@[simp]
theorem
ModuleCat.HasColimit.coconePointSMul_apply
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))]
(r : R)
:
(ModuleCat.HasColimit.coconePointSMul F) r = CategoryTheory.Limits.colimMap (CategoryTheory.NatTrans.mk fun (j : J) => (ModuleCat.smul (F.toPrefunctor.obj j)) r)
noncomputable def
ModuleCat.HasColimit.coconePointSMul
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))]
:
The induced scalar multiplication on
colimit (F ⋙ forget₂ _ AddCommGroupCat).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ModuleCat.HasColimit.colimitCocone_ι_app
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))]
(j : J)
:
(ModuleCat.HasColimit.colimitCocone F).ι.app j = ModuleCat.homMk
(CategoryTheory.Limits.colimit.ι
(CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)) j)
(_ :
∀ (r : R),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι
(CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)) j)
((ModuleCat.smul
(((CategoryTheory.Functor.const J).toPrefunctor.obj
(ModuleCat.mkOfSMul (ModuleCat.HasColimit.coconePointSMul F))).toPrefunctor.obj
j))
r) = CategoryTheory.CategoryStruct.comp ((ModuleCat.smul (F.toPrefunctor.obj j)) r)
(CategoryTheory.Limits.colimit.ι
(CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)) j))
@[simp]
theorem
ModuleCat.HasColimit.colimitCocone_pt
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))]
:
noncomputable def
ModuleCat.HasColimit.colimitCocone
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))]
:
The cocone for F constructed from the colimit of
(F ⋙ forget₂ (ModuleCat R) AddCommGroupCat).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
ModuleCat.HasColimit.isColimitColimitCocone
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))]
:
The cocone for F constructed from the colimit of
(F ⋙ forget₂ (ModuleCat R) AddCommGroupCat) is a colimit cocone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
ModuleCat.HasColimit.instHasColimitModuleCatModuleCategory
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))]
:
Equations
- (_ : CategoryTheory.Limits.HasColimit F) = (_ : CategoryTheory.Limits.HasColimit F)
noncomputable instance
ModuleCat.HasColimit.instPreservesColimitModuleCatModuleCategoryAddCommGroupCatInstAddCommGroupCatLargeCategoryForget₂ModuleConcreteCategoryConcreteCategoryHasForgetToAddCommGroup
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))]
:
Equations
- One or more equations did not get rendered due to their size.
instance
ModuleCat.hasColimitsOfShape
(R : Type w)
[Ring R]
(J : Type u)
[CategoryTheory.Category.{v, u} J]
[CategoryTheory.Limits.HasColimitsOfShape J AddCommGroupCat]
:
Equations
- (_ : CategoryTheory.Limits.HasColimitsOfShape J (ModuleCat R)) = (_ : CategoryTheory.Limits.HasColimitsOfShape J (ModuleCat R))
instance
ModuleCat.hasColimitsOfSize
(R : Type w)
[Ring R]
[CategoryTheory.Limits.HasColimitsOfSize.{v, u, w', w' + 1} AddCommGroupCat]
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
ModuleCat.forget₂PreservesColimitsOfShape
(R : Type w)
[Ring R]
(J : Type u)
[CategoryTheory.Category.{v, u} J]
[CategoryTheory.Limits.HasColimitsOfShape J AddCommGroupCat]
:
Equations
- ModuleCat.forget₂PreservesColimitsOfShape R J = CategoryTheory.Limits.PreservesColimitsOfShape.mk
noncomputable instance
ModuleCat.forget₂PreservesColimitsOfSize
(R : Type w)
[Ring R]
[CategoryTheory.Limits.HasColimitsOfSize.{u, v, w', w' + 1} AddCommGroupCat]
:
Equations
- ModuleCat.forget₂PreservesColimitsOfSize R = CategoryTheory.Limits.PreservesColimitsOfSize.mk
noncomputable instance
ModuleCat.instPreservesColimitsOfSizeModuleCatMaxModuleCategoryAddCommGroupCatInstAddCommGroupCatLargeCategoryForget₂ModuleConcreteCategoryConcreteCategoryHasForgetToAddCommGroup
(R : Type w)
[Ring R]
[CategoryTheory.Limits.HasColimitsOfSize.{u, v, max w w', max (w + 1) (w' + 1)} AddCommGroupCatMax]
:
Equations
- One or more equations did not get rendered due to their size.