English
There exists a free topological module functor TopCat → TopModuleCat R sending a space X to the free topological R-module on X.
Русский
Существует функтор свободного топологического модуля от TopCat к TopModuleCat R, отправляющий пространство X в свободный топологический R-модуль на X.
LaTeX
$$$\\mathrm{freeObj}_R(X) = X \\to (\\text{free topological module on } X)$$$
Lean4
/-- The free topological module over a topological space. -/
noncomputable def freeObj (X : TopCat.{v}) : TopModuleCat.{max v u} R :=
letI : TopologicalSpace (X →₀ R) :=
sInf {t | @ContinuousSMul R _ _ _ t ∧ @ContinuousAdd _ t _ ∧ X.str.coinduced (Finsupp.single · 1) ≤ t}
letI : ContinuousAdd (X →₀ R) := continuousAdd_sInf fun _ h ↦ h.2.1
letI : ContinuousSMul R (X →₀ R) := continuousSMul_sInf fun _ h ↦ h.1
of R (X →₀ R)
