If V
has limits of shape J
, so does Action V G
.
If V
has colimits of shape J
, so does Action V G
.
F : C ⥤ Action V G
preserves the limit of some K : J ⥤ C
if
if it does after postcomposing with the forgetful functor Action V G ⥤ V
.
F : C ⥤ Action V G
preserves limits of some shape J
if it does after postcomposing with the forgetful functor Action V G ⥤ V
.
F : C ⥤ Action V G
preserves limits of some size
if it does after postcomposing with the forgetful functor Action V G ⥤ V
.
F : C ⥤ Action V G
preserves the colimit of some K : J ⥤ C
if
if it does after postcomposing with the forgetful functor Action V G ⥤ V
.
F : C ⥤ Action V G
preserves colimits of some shape J
if it does after postcomposing with the forgetful functor Action V G ⥤ V
.
F : C ⥤ Action V G
preserves colimits of some size
if it does after postcomposing with the forgetful functor Action V G ⥤ V
.
Equations
- Action.instZeroHom = { zero := { hom := 0, comm := ⋯ } }
Equations
- Action.instHasZeroMorphisms = { zero := fun (X Y : Action V G) => Action.instZeroHom, comp_zero := ⋯, zero_comp := ⋯ }
Equations
- Action.instNegHom = { neg := fun (f : X ⟶ Y) => { hom := -f.hom, comm := ⋯ } }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Auxiliary construction for the Abelian (Action V G)
instance.