English
If a map has dense range and a subalgebra s has topologicalClosure = ⊤, then its image subalgebra also has topologicalClosure = ⊤.
Русский
Если непрерывное отображение имеет плотный образ, и подалгебра имеет замыкание = ⊤, то образ подалгебры также плотен в топологической оболочке.
LaTeX
$$hf' : DenseRange f → (s.topologicalClosure = ⊤) → (s.map f).topologicalClosure = ⊤$$
Lean4
/-- Under a dense continuous algebra map, a subalgebra
whose `TopologicalClosure` is `⊤` is sent to another such submodule.
That is, the image of a dense subalgebra under a map with dense range is dense.
-/
theorem _root_.DenseRange.topologicalClosure_map_subalgebra [IsTopologicalSemiring B] {f : A →A[R] B}
(hf' : DenseRange f) {s : Subalgebra R A} (hs : s.topologicalClosure = ⊤) :
(s.map (f : A →ₐ[R] B)).topologicalClosure = ⊤ :=
by
rw [SetLike.ext'_iff] at hs ⊢
simp only [Subalgebra.topologicalClosure_coe, coe_top, ← dense_iff_closure_eq, Subalgebra.coe_map,
AlgHom.coe_coe] at hs ⊢
exact hf'.dense_image f.continuous hs
