English
Let A,B be R-algebras with the module topology. If φ: A →+* B is a ring homomorphism and the composite φ ∘ algebraMap R A is continuous, then φ is continuous as a map of topological spaces.
Русский
Пусть A, B — R-алгебры и есть модульная топология. Если φ: A →+* B—кольцевой гомоморфизм и композиция φ с алгебраическим отображением R в A непрерывна, то φ непрерывна как отображение множеств.
LaTeX
$$$\forall \varphi: A \to_{{R}} B, \\ (Continuous(\\varphi \\circ (algebraMap R A)) \\Rightarrow \\ Continuous(\\varphi)).$$$
Lean4
@[fun_prop, continuity]
theorem continuous_of_ringHom {R A B} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [TopologicalSpace R]
[TopologicalSpace A] [IsModuleTopology R A] [TopologicalSpace B] [IsTopologicalSemiring B] (φ : A →+* B)
(hφ : Continuous (φ.comp (algebraMap R A))) : Continuous φ :=
by
let inst := Module.compHom B (φ.comp (algebraMap R A))
let φ' : A →ₗ[R] B := ⟨φ, fun r m ↦ by simp [Algebra.smul_def]; rfl⟩
have : ContinuousSMul R B := ⟨(hφ.comp continuous_fst).mul continuous_snd⟩
exact continuous_of_linearMap φ'
