Categorical properties of Action V G

We show:

• When V has (co)limits so does Action V G.
• When V is preadditive, linear, or abelian so is Action V G.

instance Action.instHasFiniteProductsActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasFiniteProducts V] : CategoryTheory.Limits.HasFiniteProducts (Action V G)

Equations

• ⋯ = ⋯

instance Action.instHasFiniteLimitsActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasFiniteLimits V] : CategoryTheory.Limits.HasFiniteLimits (Action V G)

Equations

• ⋯ = ⋯

instance Action.instHasLimitsActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasLimits V] : CategoryTheory.Limits.HasLimits (Action V G)

Equations

• ⋯ = ⋯

instance Action.hasLimitsOfShape {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] [CategoryTheory.Limits.HasLimitsOfShape J V] : CategoryTheory.Limits.HasLimitsOfShape J (Action V G)

If V has limits of shape J, so does Action V G.

Equations

• ⋯ = ⋯

instance Action.instHasFiniteCoproductsActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasFiniteCoproducts V] : CategoryTheory.Limits.HasFiniteCoproducts (Action V G)

Equations

• ⋯ = ⋯

instance Action.instHasFiniteColimitsActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasFiniteColimits V] : CategoryTheory.Limits.HasFiniteColimits (Action V G)

Equations

• ⋯ = ⋯

instance Action.instHasColimitsActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasColimits V] : CategoryTheory.Limits.HasColimits (Action V G)

Equations

• ⋯ = ⋯

instance Action.hasColimitsOfShape {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] [CategoryTheory.Limits.HasColimitsOfShape J V] : CategoryTheory.Limits.HasColimitsOfShape J (Action V G)

If V has colimits of shape J, so does Action V G.

Equations

• ⋯ = ⋯

noncomputable def Action.preservesLimitOfPreserves {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {C : Type t₁} [CategoryTheory.Category.{t₂, t₁} C] (F : CategoryTheory.Functor C (Action V G)) {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] (K : CategoryTheory.Functor J C) (h : CategoryTheory.Limits.PreservesLimit K (CategoryTheory.Functor.comp F (Action.forget V G))) : CategoryTheory.Limits.PreservesLimit K F

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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Action.preservesLimitsOfShapeOfPreserves {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {C : Type t₁} [CategoryTheory.Category.{t₂, t₁} C] (F : CategoryTheory.Functor C (Action V G)) {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] (h : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Functor.comp F (Action.forget V G))) : CategoryTheory.Limits.PreservesLimitsOfShape J F

F : C ⥤ Action V G preserves limits of some shape J if it does after postcomposing with the forgetful functor Action V G ⥤ V.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Action.preservesLimitsOfSizeOfPreserves {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {C : Type t₁} [CategoryTheory.Category.{t₂, t₁} C] (F : CategoryTheory.Functor C (Action V G)) (h : CategoryTheory.Limits.PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (CategoryTheory.Functor.comp F (Action.forget V G))) : CategoryTheory.Limits.PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} F

F : C ⥤ Action V G preserves limits of some size if it does after postcomposing with the forgetful functor Action V G ⥤ V.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Action.preservesColimitOfPreserves {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {C : Type t₁} [CategoryTheory.Category.{t₂, t₁} C] (F : CategoryTheory.Functor C (Action V G)) {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] (K : CategoryTheory.Functor J C) (h : CategoryTheory.Limits.PreservesColimit K (CategoryTheory.Functor.comp F (Action.forget V G))) : CategoryTheory.Limits.PreservesColimit K F

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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Action.preservesColimitsOfShapeOfPreserves {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {C : Type t₁} [CategoryTheory.Category.{t₂, t₁} C] (F : CategoryTheory.Functor C (Action V G)) {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] (h : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Functor.comp F (Action.forget V G))) : CategoryTheory.Limits.PreservesColimitsOfShape J F

F : C ⥤ Action V G preserves colimits of some shape J if it does after postcomposing with the forgetful functor Action V G ⥤ V.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Action.preservesColimitsOfSizeOfPreserves {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {C : Type t₁} [CategoryTheory.Category.{t₂, t₁} C] (F : CategoryTheory.Functor C (Action V G)) (h : CategoryTheory.Limits.PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (CategoryTheory.Functor.comp F (Action.forget V G))) : CategoryTheory.Limits.PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} F

F : C ⥤ Action V G preserves colimits of some size if it does after postcomposing with the forgetful functor Action V G ⥤ V.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Action.instPreservesLimitsOfShapeActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] [CategoryTheory.Limits.HasLimitsOfShape J V] : CategoryTheory.Limits.PreservesLimitsOfShape J (Action.forget V G)

Equations

• Action.instPreservesLimitsOfShapeActionInstCategoryActionForget = let_fun this := inferInstance; this

noncomputable instance Action.instPreservesColimitsOfShapeActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] [CategoryTheory.Limits.HasColimitsOfShape J V] : CategoryTheory.Limits.PreservesColimitsOfShape J (Action.forget V G)

Equations

• Action.instPreservesColimitsOfShapeActionInstCategoryActionForget = let_fun this := inferInstance; this

noncomputable instance Action.instPreservesFiniteLimitsActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasFiniteLimits V] : CategoryTheory.Limits.PreservesFiniteLimits (Action.forget V G)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Action.instPreservesFiniteColimitsActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasFiniteColimits V] : CategoryTheory.Limits.PreservesFiniteColimits (Action.forget V G)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Action.instReflectsLimitActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] (F : CategoryTheory.Functor J (Action V G)) : CategoryTheory.Limits.ReflectsLimit F (Action.forget V G)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Action.instReflectsLimitsOfShapeActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] : CategoryTheory.Limits.ReflectsLimitsOfShape J (Action.forget V G)

Equations

• Action.instReflectsLimitsOfShapeActionInstCategoryActionForget = { reflectsLimit := fun {K : CategoryTheory.Functor J (Action V G)} => inferInstance }

noncomputable instance Action.instReflectsLimitsActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Limits.ReflectsLimits (Action.forget V G)

Equations

• Action.instReflectsLimitsActionInstCategoryActionForget = { reflectsLimitsOfShape := fun {J : Type u} [CategoryTheory.Category.{u, u} J] => inferInstance }

noncomputable instance Action.instReflectsColimitActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] (F : CategoryTheory.Functor J (Action V G)) : CategoryTheory.Limits.ReflectsColimit F (Action.forget V G)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Action.instReflectsColimitsOfShapeActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] : CategoryTheory.Limits.ReflectsColimitsOfShape J (Action.forget V G)

Equations

• Action.instReflectsColimitsOfShapeActionInstCategoryActionForget = { reflectsColimit := fun {K : CategoryTheory.Functor J (Action V G)} => inferInstance }

noncomputable instance Action.instReflectsColimitsActionInstCategoryActionForget {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Limits.ReflectsColimits (Action.forget V G)

Equations

• Action.instReflectsColimitsActionInstCategoryActionForget = { reflectsColimitsOfShape := fun {J : Type u} [CategoryTheory.Category.{u, u} J] => inferInstance }

instance Action.instZeroHomActionToQuiverToCategoryStructInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] {X : Action V G} {Y : Action V G} : Zero (X ⟶ Y)

Equations

• Action.instZeroHomActionToQuiverToCategoryStructInstCategoryAction = { zero := { hom := 0, comm := ⋯ } }

@[simp]

theorem Action.zero_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] {X : Action V G} {Y : Action V G} : 0.hom = 0

instance Action.instHasZeroMorphismsActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Limits.HasZeroMorphisms (Action V G)

Equations

• Action.instHasZeroMorphismsActionInstCategoryAction = CategoryTheory.Limits.HasZeroMorphisms.mk ⋯ ⋯

instance Action.forget_preservesZeroMorphisms {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor.PreservesZeroMorphisms (Action.forget V G)

Equations

• ⋯ = ⋯

instance Action.forget₂_preservesZeroMorphisms {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.ConcreteCategory V] : CategoryTheory.Functor.PreservesZeroMorphisms (CategoryTheory.forget₂ (Action V G) V)

Equations

• ⋯ = ⋯

instance Action.functorCategoryEquivalence_preservesZeroMorphisms {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor.PreservesZeroMorphisms (Action.functorCategoryEquivalence V G).functor

Equations

• ⋯ = ⋯

instance Action.instAddHomActionToQuiverToCategoryStructInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} : Add (X ⟶ Y)

Equations

• Action.instAddHomActionToQuiverToCategoryStructInstCategoryAction = { add := fun (f g : X ⟶ Y) => { hom := f.hom + g.hom, comm := ⋯ } }

instance Action.instNegHomActionToQuiverToCategoryStructInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} : Neg (X ⟶ Y)

Equations

• Action.instNegHomActionToQuiverToCategoryStructInstCategoryAction = { neg := fun (f : X ⟶ Y) => { hom := -f.hom, comm := ⋯ } }

instance Action.instPreadditiveActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] : CategoryTheory.Preadditive (Action V G)

Equations

• Action.instPreadditiveActionInstCategoryAction = { homGroup := fun (X Y : Action V G) => AddCommGroup.mk ⋯, add_comp := ⋯, comp_add := ⋯ }

instance Action.forget_additive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] : CategoryTheory.Functor.Additive (Action.forget V G)

Equations

• ⋯ = ⋯

instance Action.forget₂_additive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] [CategoryTheory.ConcreteCategory V] : CategoryTheory.Functor.Additive (CategoryTheory.forget₂ (Action V G) V)

Equations

• ⋯ = ⋯

instance Action.functorCategoryEquivalence_additive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] : CategoryTheory.Functor.Additive (Action.functorCategoryEquivalence V G).functor

Equations

• ⋯ = ⋯

@[simp]

theorem Action.neg_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} (f : X ⟶ Y) : (-f).hom = -f.hom

@[simp]

theorem Action.add_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} (f : X ⟶ Y) (g : X ⟶ Y) : (f + g).hom = f.hom + g.hom

@[simp]

theorem Action.sum_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} {ι : Type u_1} (f : ι → (X ⟶ Y)) (s : Finset ι) : (Finset.sum s f).hom = Finset.sum s fun (i : ι) => (f i).hom

instance Action.instLinearActionInstCategoryActionInstPreadditiveActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] : CategoryTheory.Linear R (Action V G)

Equations

• Action.instLinearActionInstCategoryActionInstPreadditiveActionInstCategoryAction = { homModule := fun (X Y : Action V G) => Module.mk ⋯ ⋯, smul_comp := ⋯, comp_smul := ⋯ }

instance Action.forget_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] : CategoryTheory.Functor.Linear R (Action.forget V G)

Equations

• ⋯ = ⋯

instance Action.forget₂_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.ConcreteCategory V] : CategoryTheory.Functor.Linear R (CategoryTheory.forget₂ (Action V G) V)

Equations

• ⋯ = ⋯

instance Action.functorCategoryEquivalence_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] : CategoryTheory.Functor.Linear R (Action.functorCategoryEquivalence V G).functor

Equations

• ⋯ = ⋯

@[simp]

theorem Action.smul_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] {X : Action V G} {Y : Action V G} (r : R) (f : X ⟶ Y) : (r • f).hom = r • f.hom

instance Action.res_additive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {H : MonCat} (f : G ⟶ H) : CategoryTheory.Functor.Additive (Action.res V f)

Equations

• ⋯ = ⋯

instance Action.res_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] {H : MonCat} (f : G ⟶ H) : CategoryTheory.Functor.Linear R (Action.res V f)

Equations

• ⋯ = ⋯

def Action.abelianAux {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : Action V G ≌ CategoryTheory.Functor (ULift.{u, 0} (CategoryTheory.SingleObj ↑G)) V

Auxiliary construction for the Abelian (Action V G) instance.

Equations

• Action.abelianAux = (Action.functorCategoryEquivalence V G).trans (CategoryTheory.Equivalence.congrLeft CategoryTheory.ULift.equivalence)

noncomputable instance Action.instAbelianActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Abelian V] : CategoryTheory.Abelian (Action V G)

Equations

• Action.instAbelianActionInstCategoryAction = CategoryTheory.abelianOfEquivalence Action.abelianAux.functor

instance CategoryTheory.Functor.mapAction_preadditive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) [CategoryTheory.Preadditive V] [CategoryTheory.Preadditive W] [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor.Additive (CategoryTheory.Functor.mapAction F G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.mapAction_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) [CategoryTheory.Preadditive V] [CategoryTheory.Preadditive W] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.Linear R W] [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Linear R F] : CategoryTheory.Functor.Linear R (CategoryTheory.Functor.mapAction F G)

Equations

• ⋯ = ⋯