English
The elemental construction of an algebra is defined as the topological closure of the subalgebra generated by a single element.
Русский
Конструкция elemental алгебры определяется как топологическое замыкание подалгебры, порожденной одним элементом.
LaTeX
$$Algebra.elemental(R)(x) = (Algebra.adjoin R ({ x } : Set A)).topologicalClosure$$
Lean4
/-- This is really a statement about topological algebra isomorphisms,
but we don't have those, so we use the clunky approach of talking about
an algebra homomorphism, and a separate homeomorphism,
along with a witness that as functions they are the same.
-/
theorem topologicalClosure_comap_homeomorph (s : Subalgebra R A) {B : Type*} [TopologicalSpace B] [Ring B]
[IsTopologicalRing B] [Algebra R B] (f : B →ₐ[R] A) (f' : B ≃ₜ A) (w : (f : B → A) = f') :
s.topologicalClosure.comap f = (s.comap f).topologicalClosure :=
by
apply SetLike.ext'
simp only [Subalgebra.topologicalClosure_coe]
simp only [Subalgebra.coe_comap]
rw [w]
exact f'.preimage_closure _
