forget₂ (FGModuleCat K) (ModuleCat K) creates all finite colimits. #
And hence FGModuleCat K has all finite colimits.
instance
FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite
{k : Type u}
[Ring k]
{J : Type}
[Finite J]
(Z : J → ModuleCat k)
[∀ (j : J), Module.Finite k ↑(Z j)]
:
Module.Finite k ↑(∐ fun (j : J) => Z j)
instance
FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂
{J : Type}
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
{k : Type u}
[Ring k]
(F : CategoryTheory.Functor J (FGModuleCat k))
:
Module.Finite k ↑(CategoryTheory.Limits.colimit (F.comp (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))
Finite colimits of finite modules are finite, because we can realise them as quotients of a finite coproduct.
def
FGModuleCat.forget₂CreatesColimit
{J : Type}
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
{k : Type u}
[Ring k]
(F : CategoryTheory.Functor J (FGModuleCat k))
:
The forgetful functor from FGModuleCat k to ModuleCat k creates all finite colimits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
FGModuleCat.instCreatesColimitsOfShapeModuleCatForget₂
{J : Type}
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
{k : Type u}
[Ring k]
:
Equations
- FGModuleCat.instCreatesColimitsOfShapeModuleCatForget₂ = { CreatesColimit := fun {F : CategoryTheory.Functor J (FGModuleCat k)} => FGModuleCat.forget₂CreatesColimit F }
instance
FGModuleCat.instHasColimitsOfShapeOfFinCategory
{k : Type u}
[Ring k]
(J : Type)
[CategoryTheory.Category.{0, 0} J]
[CategoryTheory.FinCategory J]
: