The category of R-modules has all colimits. #
From the existence of colimits in AddCommGrpCat, we deduce the existence of colimits
in ModuleCat R. This way, we get for free that the functor
forget₂ (ModuleCat R) AddCommGrpCat 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.
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 (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
The induced scalar multiplication on
colimit (F ⋙ forget₂ _ AddCommGrpCat).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
(r : R)
:
(coconePointSMul F) r = CategoryTheory.Limits.colimMap { app := fun (j : J) => (F.obj j).smul r, naturality := ⋯ }
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 (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
The cocone for F constructed from the colimit of
(F ⋙ forget₂ (ModuleCat R) AddCommGrpCat).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ModuleCat.HasColimit.colimitCocone_pt_isModule
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
@[simp]
theorem
ModuleCat.HasColimit.colimitCocone_pt_carrier
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
@[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 (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
(j : J)
:
(colimitCocone F).ι.app j = homMk (CategoryTheory.Limits.colimit.ι (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)) j) ⋯
@[simp]
theorem
ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
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 (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
The cocone for F constructed from the colimit of
(F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) is a colimit cocone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
ModuleCat.HasColimit.instHasColimit
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
instance
ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
instance
ModuleCat.HasColimit.reflectsColimit
{R : Type w}
[Ring R]
{J : Type u}
[CategoryTheory.Category.{v, u} J]
(F : CategoryTheory.Functor J (ModuleCat R))
[CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))]
:
instance
ModuleCat.hasColimitsOfShape
(R : Type w)
[Ring R]
(J : Type u)
[CategoryTheory.Category.{v, u} J]
[CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat]
:
instance
ModuleCat.reflectsColimitsOfShape
(R : Type w)
[Ring R]
(J : Type u)
[CategoryTheory.Category.{v, u} J]
[CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat]
:
noncomputable def
ModuleCat.finsuppCocone
(R : Type w)
[CommRing R]
(M ι : Type u)
[AddCommGroup M]
[Module R M]
:
CategoryTheory.Limits.Cofan fun (x : ι) => of R M
The coproduct cone induced by the concrete coproduct.
Equations
- ModuleCat.finsuppCocone R M ι = CategoryTheory.Limits.Cofan.mk (ModuleCat.of R (ι →₀ M)) fun (i : ι) => ModuleCat.ofHom (Finsupp.lsingle i)
Instances For
noncomputable def
ModuleCat.finsuppCoconeIsColimit
(R : Type w)
[CommRing R]
(M ι : Type u)
[AddCommGroup M]
[Module R M]
:
The concrete cocoproduct cone is colimiting.
Equations
- One or more equations did not get rendered due to their size.