English
There is a functor free: TopCat → TopModuleCat(R) whose action on objects is the free topological R-module on a space, and on morphisms is the induced map. This functor is left adjoint to the forgetful functor from TopModuleCat(R) to TopCat.
Русский
Существуeт функтор free: TopCat → TopModuleCat(R), который отправляет пространство на свободный топологический R-модуль над ним, а отображения — на индуцированные отображения. Этот функтор является левой относительно функтору забывания.
LaTeX
$$$\mathrm{free}: \mathrm{TopCat} \to \mathrm{TopModuleCat}(R) \quad\text{is left adjoint to}\quad \mathrm{forget}_{\mathrm{TopModuleCat}(R) \to \mathrm{TopCat}}.$$$
Lean4
/-- The free topological module over a topological space as a functor.
This is left adjoint to the forgetful functor. -/
@[simps]
noncomputable def free : TopCat.{v} ⥤ TopModuleCat.{max v u} R :=
{ obj := freeObj R
map f := freeMap R f
map_id M := by ext x; exact DFunLike.congr_fun (Finsupp.lmapDomain_id _ _) x
map_comp f g := by ext; exact DFunLike.congr_fun (Finsupp.lmapDomain_comp _ _ f.hom g.hom) _ }
