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.instHasFiniteProducts {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasFiniteProducts V] : CategoryTheory.Limits.HasFiniteProducts (Action V G)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Action.instHasLimits {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.instHasFiniteCoproducts {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasFiniteCoproducts V] : CategoryTheory.Limits.HasFiniteCoproducts (Action V G)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Action.instHasColimits {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

• ⋯ = ⋯

theorem Action.preservesLimit_of_preserves {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 (F.comp (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.

theorem Action.preservesLimitsOfShape_of_preserves {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 (F.comp (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.

theorem Action.preservesLimitsOfSize_of_preserves {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} (F.comp (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.

theorem Action.preservesColimit_of_preserves {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 (F.comp (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.

theorem Action.preservesColimitsOfShape_of_preserves {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 (F.comp (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.

theorem Action.preservesColimitsOfSize_of_preserves {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} (F.comp (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.

noncomputable instance Action.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape {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

• ⋯ = ⋯

noncomputable instance Action.instPreservesColimitsOfShapeForgetOfHasColimitsOfShape {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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Action.instReflectsLimitForget {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

• ⋯ = ⋯

instance Action.instReflectsLimitsOfShapeForget {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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Action.instReflectsColimitForget {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

• ⋯ = ⋯

noncomputable instance Action.instReflectsColimitsOfShapeForget {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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

@[simp]

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

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

Equations

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

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

Equations

• Action.instPreadditive = { 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] : (Action.forget V G).Additive

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem Action.neg_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X 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 Y : Action V G} (f 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 Y : Action V G} {ι : Type u_1} (f : ι → (X ⟶ Y)) (s : Finset ι) : (s.sum f).hom = ∑ i ∈ s, (f i).hom

instance Action.instLinear {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.instLinear = { 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 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) : (Action.res V f).Additive

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.ULift.equivalence.congrLeft

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

Equations

• Action.instAbelian = 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] [F.Additive] : (F.mapAction G).Additive

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] [F.Additive] [CategoryTheory.Functor.Linear R F] : CategoryTheory.Functor.Linear R (F.mapAction G)

Equations

• ⋯ = ⋯