Implementation of direct sum of functors

Stream: new members

[VayusElytra]

Hi, I've been working as an exercise on defining the direct sum of two functors recently. The idea is the following: if we have two functors F, G : C \funct D and D is well-behaved enough (for instance, abelian), then I'd like to define a functor F x G that maps X : Obj(C) to F(X) x G(X) and f : X -> Y to F(f) x G(f) : F(X) x G(X) -> F(Y) x G(Y) . In the following I worked with modules for simplicity.
Here's the code I have:

import Mathlib.Algebra.Category.ModuleCat.Abelian --ModuleCat is an abelian category
import Mathlib.Algebra.Module.LinearMap.Basic
import Mathlib.Algebra.DirectSum.Module
import Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
import Mathlib.Algebra.Module.Prod


open CategoryTheory

abbrev FunctCat (C : Type) [Category C] (K : Type) [DivisionRing K]
   := (C ⥤ ModuleCat K)

--Given R a field, C a category, X ∈ Obj(C) and F, G two functors
--C ⥤ Modules over R, this defines the product F(X) × G(X).
@[simp]
def ProductModule (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : FunctCat C R) (G : FunctCat C R) (X : C): ModuleCat R :=
  ModuleCat.of R ((F.obj X) × (G.obj X))

--Given R a field, C a category, X, Y ∈ Obj(C), f : X ⟶ Y a linear map
--and F, G two functors C ⥤ Modules over R, this defines the product map
--(F f, G f) : (F X × G X) ⟶ (F Y × G Y)
@[simp]
def ProductMapFunc (R : Type) [DivisionRing R] (C : Type) [Category C]
  {X Y : C} (f : (X ⟶ Y)) (F : FunctCat C R) (G : FunctCat C R)
  : ((F.obj X × G.obj X) →ₗ[R] (F.obj Y × G.obj Y)) where
  toFun x := by
    let x₁ := x.1
    let x₂ := x.2
    exact ⟨F.map f x₁, G.map f x₂⟩
  map_add' x y := by
    dsimp
    rw[LinearMap.map_add (F.map f) _ _, LinearMap.map_add (G.map f) _ _]
  map_smul' c x := by
    dsimp
    rw[LinearMap.map_smul (F.map f) _ _, LinearMap.map_smul (G.map f) _ _]

--Same as above, but written with the ProductModule objects for simplicity
@[simp]
def ProductModuleMap (R : Type) [DivisionRing R] (C : Type) [Category C]
  {X Y : C} (f : (X ⟶ Y)) (F : FunctCat C R) (G : FunctCat C R) :
  ((ProductModule R C F G X) ⟶ (ProductModule R C F G Y)) :=
  ProductMapFunc R C f F G

--The direct sum of the functors F and G.
noncomputable def FunctorDirSum (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : FunctCat C R) (G : FunctCat C R) : FunctCat C R where
  obj X := ProductModule R C F G X
  map f := ProductModuleMap R C f F G
  map_id := by
    intro X
    simp
    rfl
  map_comp := by
    intro X Y Z f g
    simp
    rfl

My questions about this are:

1) I don't really understand why rfl is able to close the map_id and map_comp proofs, particularly the former. The tactic state is very messy and I frankly had no idea how I was going to approach it before finding out that rfl worked. Assuming it hadn't, how would you approach, say, the proof of map_id?

2) Is it actually good practice to dump everything in definitions like "ProductMapFunc" or "ProductModuleMap"? What would a more proper approach to this implementation be?

[Joël Riou]

Another approach would be to use categorical binary products in the functor category, and then use the fact the the evaluation at each X : C commutes with the product, and that we know how products look like in ModuleCat.