English
There exists a forgetful functor from the category of topological commutative rings to the category of topological spaces, sending each ring to its underlying topological space and each continuous ring homomorphism to its underlying continuous map.
Русский
Существует функтор забывания из категории топологических коммутативных колец в категорию топологических пространств, отправляющий каждый кольцо в его базовое топологическое пространство и каждое непрерывное кольцевое гомоморфизм — в соответствующую непрерывную карту.
LaTeX
$$$\exists F:\mathbf{TopCommRingCat}\to \mathbf{TopCat},\quad F(R)=\mathrm{TopCat.of}(R),\quad F(f)=\mathrm{TopCat.ofHom}(\langle f.1, f.2\rangle).$$$
Lean4
/-- The forgetful functor to `TopCat`. -/
instance hasForgetToTopCat : HasForget₂ TopCommRingCat TopCat :=
HasForget₂.mk' (fun R => TopCat.of R) (fun _ => rfl) (fun f => TopCat.ofHom ⟨⇑f.1, f.2⟩) HEq.rfl
