Lean4
/-- A functor to an `R`-linear category lifts to a functor from its `R`-linear completion.
-/
@[simps]
def lift (F : C ⥤ D) : Free R C ⥤ D where
obj X := F.obj X
map {_ _} f := f.sum fun f' r => r • F.map f'
map_id := by dsimp [CategoryTheory.categoryFree]; simp
map_comp {X Y Z} f
g := by
induction f using Finsupp.induction_linear with
| zero => simp
| add f₁ f₂ w₁ w₂ =>
rw [add_comp]
rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
· simp only [w₁, w₂, add_comp]
· intros; rw [zero_smul]
· intros; simp only [add_smul]
· intros; rw [zero_smul]
· intros; simp only [add_smul]
| single f' r =>
induction g using Finsupp.induction_linear with
| zero => simp
| add f₁ f₂ w₁ w₂ =>
rw [comp_add]
rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
· simp only [w₁, w₂, comp_add]
· intros; rw [zero_smul]
· intros; simp only [add_smul]
· intros; rw [zero_smul]
· intros; simp only [add_smul]
| single g' s =>
rw [single_comp_single _ _ f' g' r s]
simp [mul_comm r s, mul_smul]
