English
The indiscrete topology functor is right adjoint to the forgetful functor.
Русский
Indiscrete-функтор является правым сопряженным забыванию функтору.
LaTeX
$$$indiscrete \\dashv forget₂$$$
Lean4
/-- The functor equipping a module with the indiscrete topology.
This is right adjoint to the forgetful functor. -/
def indiscrete : ModuleCat.{v} R ⥤ TopModuleCat.{v} R
where
obj
X :=
letI : TopologicalSpace X := ⊤
haveI : ContinuousAdd X := ⟨by rw [continuous_iff_coinduced_le]; exact le_top⟩
haveI : ContinuousSMul R X := ⟨by rw [continuous_iff_coinduced_le]; exact le_top⟩
.of R X
map {X Y}
f :=
letI : TopologicalSpace X := ⊤
letI : TopologicalSpace Y := ⊤
ConcreteCategory.ofHom (C := TopModuleCat R) ⟨f.hom, by rw [continuous_iff_coinduced_le]; exact le_top⟩
