Preservation of (co)limits in `Action V G`

Stream: Is there code for X?

[Christian Merten]

Is there somewhere the statement: If a functor to Action V G composed with the forgetful functor to V preserves (co)limits, then also the functor itself preserves (co)limits?

I.e. something like

import Mathlib.RepresentationTheory.Action.Basic
import Mathlib.CategoryTheory.Limits.Preserves.Basic

universe u v w v₁ u₁ u₂ w₂ w₁

open CategoryTheory Limits Functor

variable {C : Type u} [Category.{v, u} C] (V : Type (w + 1)) [LargeCategory.{w} V] [ConcreteCategory V] (G : MonCat.{w})

private def SingleObj.preservesColimit (F : C ⥤ SingleObj G ⥤ V)
    {J : Type w₁} [Category.{w₂, w₁} J] (K : J ⥤ C)
    (h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G)))
    : PreservesColimit K F := by
  apply preservesColimitOfEvaluation
  intro _
  exact h

def Action.preservesColimitOfPreserves (F : C ⥤ Action V G) {J : Type w₁}
    [Category.{w₂, w₁} J] (K : J ⥤ C)
    (h : PreservesColimit K (F ⋙ forget₂ (Action V G) V)) : PreservesColimit K F := by
  let F' : C ⥤ SingleObj G ⥤ V := F ⋙ (Action.functorCategoryEquivalence V G).functor
  let i : PreservesColimit K F' := by
    apply SingleObj.preservesColimit
    show PreservesColimit K (F ⋙ forget₂ (Action V G) V)
    assumption
  apply preservesColimitOfReflectsOfPreserves F (Action.functorCategoryEquivalence V G).functor

def Action.preservesColimitOfShapeOfPreserves (F : C ⥤ Action V G) {J : Type w₁}
    [Category.{w₂, w₁} J] (h : PreservesColimitsOfShape J (F ⋙ forget₂ (Action V G) V)) :
    PreservesColimitsOfShape J F := by
  constructor
  intro K
  apply Action.preservesColimitOfPreserves
  exact PreservesColimitsOfShape.preservesColimit

def Action.preservesColimitOfSizeOfPreserves (F : C ⥤ Action V G)
    (h : PreservesColimitsOfSize.{w₂, w₁} (F ⋙ forget₂ (Action V G) V)) :
    PreservesColimitsOfSize.{w₂, w₁} F := by
  constructor
  intro J _
  apply Action.preservesColimitOfShapeOfPreserves
  exact PreservesColimitsOfSize.preservesColimitsOfShape

[Kevin Buzzard]

Is this a statement about docs#CategoryTheory.ConcreteCategory s?

[Christian Merten]

I don't really think it is, it just uses the HasForget₂ instance which needs ConcreteCategory V, but forget₂ (Action V G) V could be just defined by hand as (evaluation (SingleObj G) V).obj (SingleObj.star G).

[Christian Merten]

Ah, maybe I misunderstood. Are you suggesting it could be generalized to the case of concrete categories?

[Christian Merten]

In my mind this is just a consequence of Action G V being a special functor category and how (co)limits in functor categories are computed.

[Adam Topaz]

you're looking or a "reflects colimits" kind of statement.

[Christian Merten]

Thanks! It seems to be some special version of docs#CategoryTheory.Limits.evaluationJointlyReflectsColimits

[Christian Merten]

Which in this setting can be formulated sligthly more compactly, because SingleObj G has only one object. The reformulation seems to be the snippet above.