English
There is a free functor from Type to Mod_R which sends a set X to the free R-module on X, realized as the finitely supported functions X → R with formal basis elements corresponding to generators.
Русский
Существует свободный функтор из типа в Mod_R, который отправляет множество X в свободное R-модуль над X, реализованное как модуль видов X →₀ R с формальными базисами.
LaTeX
$$$F: \mathbf{Type}_u \to \mathrm{Mod}_R$, \; F(X) = X \to_{0} R \cong \bigoplus_{x\in X} R$$$
Lean4
/-- The free functor `Type u ⥤ ModuleCat R` sending a type `X` to the
free `R`-module with generators `x : X`, implemented as the type `X →₀ R`.
-/
def free : Type u ⥤ ModuleCat R where
obj X := ModuleCat.of R (X →₀ R)
map {_ _} f := ofHom <| Finsupp.lmapDomain _ _ f
map_id := by intros; ext : 1; exact Finsupp.lmapDomain_id _ _
map_comp := by intros; ext : 1; exact Finsupp.lmapDomain_comp _ _ _ _
