Functors out of `SingleObj G`

Stream: Is there code for X?

[Christian Merten]

Are there SingleObj analogs of Discrete.functor and Discrete.natTrans? I.e.

import Mathlib

open CategoryTheory

def SingleObj.functor {α : Type w} [Monoid α] {X : C} (f : α →* End X) :
    SingleObj α ⥤ C where
  obj _ := X
  map a := f a
  map_id _ := by
    show f 1 = 1
    rw [MonoidHom.map_one]
  map_comp a b := by
    show f (b * a) = f b * f a
    rw [MonoidHom.map_mul]

def SingleObj.natTrans {α : Type w} [Monoid α] {F G : SingleObj α ⥤ C}
    (u : F.obj (SingleObj.star α) ⟶ G.obj (SingleObj.star α))
    (h : ∀ a : α, F.map a ≫ u = u ≫ G.map a)
    : F ⟶ G where
  app _ := u
  naturality _ _ a := h a

[Yury G. Kudryashov]

It looks like we have docs#MonoidHom.toFunctor but not this version.

[Christian Merten]

Should this be in the MonoidHom namespace, i.e. MonoidHom.functor or as in docs#CategoryTheory.Discrete SingleObj.functor?

[Johan Commelin]

MonoidHom.functor would make it possible to use dot notation, so I would go for that.

[Johan Commelin]

The downside is that it might be easily confused with MonoidHom.toFunctor.

[Johan Commelin]

Also, your SingleObj.natTrans doesn't really make sense in the MonoidHom namespace. So maybe your current names are in fact the best.

[Christian Merten]

#9586

[Johan Commelin]

It looks like this file could at some point also use a little clean up, introducing some variable lines.

[Johan Commelin]

Once the definition is in place, there should just be a monoid M, a group G, and a category C in scope.

[Christian Merten]

Johan Commelin said:

It looks like this file could at some point also use a little clean up, introducing some variable lines.

See #9696