Concrete action category

Stream: mathlib4

[Christian Merten]

I would like to generalise docs#Action.ofMulAction to more concrete categories other than Type. In particular I need this for FintypeCat, but I think one could generalise to any ConcreteCategory V where forget V is Full, i.e.

import Mathlib

open CategoryTheory

variable {V : Type (u + 1)} [LargeCategory V] {G : MonCat.{u}} [ConcreteCategory V]

@[simps]
def Concrete.MulAction.of [Full (forget V)] (X : V) [MulAction G ((forget _).obj X)] : Action V G where
  V := X
  ρ := MonCat.ofHom {
    toFun := by
      intro g
      let f : ((forget V).obj X) ⟶ ((forget V).obj X) := fun x => g • x
      exact Full.preimage f
    map_one' := by
      apply (forget V).map_injective
      ext
      simp only [one_smul, Full.witness, End.one_def, FunctorToTypes.map_id_apply]
    map_mul' := by
      intro g h
      apply (forget V).map_injective
      ext
      simp only [Full.witness, End.mul_def, FunctorToTypes.map_comp_apply, mul_smul]
  }

But I don't want this to make the usage of Action.ofMulAction worse. Currently

def Types.ofMulAction (X : Type u) [MulAction G X] : Action (Type u) G :=
  let i : MulAction G ((forget (Type u)).obj X) := by
    show MulAction G X
    infer_instance
  Concrete.MulAction.of X

example (X : Type u) [MulAction G X] (g : G) (x : X) : (Types.ofMulAction X).ρ g x = g • x := rfl

works, but has unwanted boilerplate code because Lean does not infer MulAction G X automatically, because it somehow can't see through (forget (Type u)).obj X.

[Christian Merten]

Do you think this is worth it or should one better introduce specialized ofMulActions for each full subcategory of Type u that one encounters?

[Adam Topaz]

I'm not sure how useful this would be since there aren't many concrete categories "in the wild" where the forgetful functor is full.

[Christian Merten]

So I just go with a specialized constructor Action.FintypeCat.ofMulAction?

[Adam Topaz]

Yes, I think so. If there ends up being another case which fits this model then it may be worth adding this general construction, but I can't think of a natural example.

[Christian Merten]

Follow up question: Where would this Action.FintypeCat.ofMulAction go? In RepresentationTheory.Action.Basic I would have to add an import for FintypeCat, do I add an extra file for this? Or do I just put this where I actually use it?

[Christian Merten]

Alternative suggestion: How about making a new file RepresentationTheory.Action.Concrete and move Action.ofMulAction and associated lemmas there.