∀ {k G : Type u} [inst : CommRing k] [inst_1 : Monoid G] {α : Type u} (A : Rep k G) (f : α → ↑A.V),
  (A.freeLift f).hom =
    ModuleCat.ofHom ((Finsupp.linearCombination k fun x => (A.ρ x.2) (f x.1)) ∘ₗ ↑(Finsupp.curryLinearEquiv k).symm)