English
There is a limit for a diagram F in TopModuleCat provided the corresponding diagram after forgetting has a limit in ModuleCat.
Русский
Существуют пределы диаграммы в TopModuleCat при условии существования предела у забытой диаграммы в ModuleCat.
LaTeX
$$$\\text{HasLimit}(F) \\Leftarrow \\text{HasLimit}(F \\circ forget₂)$$$
Lean4
/-- The functor equipping a module over a topological ring with the finest possible
topology making it into a topological module. This is left adjoint to the forgetful functor. -/
def withModuleTopology : ModuleCat R ⥤ TopModuleCat R
where
obj
X :=
letI := moduleTopology R X
letI := IsModuleTopology.topologicalAddGroup R X
.of R X
map {X Y}
f :=
letI := moduleTopology R X
letI := moduleTopology R Y
letI := IsModuleTopology.topologicalAddGroup R Y
⟨f.hom, IsModuleTopology.continuous_of_linearMap f.hom⟩
