# mathlibdocumentation

topology.algebra.algebra

# Topological (sub)algebras #

A topological algebra over a topological semiring R is a topological ring with a compatible continuous scalar multiplication by elements of R. We reuse typeclass has_continuous_smul for topological algebras.

## Results #

This is just a minimal stub for now!

The topological closure of a subalgebra is still a subalgebra, which as an algebra is a topological algebra.

theorem continuous_algebra_map_iff_smul (R : Type u_1) (A : Type u) [semiring A] [ A]  :
continuous A) continuous (λ (p : R × A), p.fst p.snd)
theorem continuous_algebra_map (R : Type u_1) (A : Type u) [semiring A] [ A] [ A] :
theorem has_continuous_smul_of_algebra_map (R : Type u_1) (A : Type u) [semiring A] [ A] (h : continuous A)) :
def subalgebra.topological_closure {R : Type u_1} {A : Type u} [semiring A] [ A] (s : A) :
A

The closure of a subalgebra in a topological algebra as a subalgebra.

Equations
@[simp]
theorem subalgebra.topological_closure_coe {R : Type u_1} {A : Type u} [semiring A] [ A] (s : A) :
@[instance]
def subalgebra.topological_closure_topological_ring {R : Type u_1} {A : Type u} [semiring A] [ A] (s : A) :
@[instance]
def subalgebra.topological_closure_topological_algebra {R : Type u_1} {A : Type u} [semiring A] [ A] [ A] (s : A) :
theorem subalgebra.subalgebra_topological_closure {R : Type u_1} {A : Type u} [semiring A] [ A] (s : A) :
theorem subalgebra.is_closed_topological_closure {R : Type u_1} {A : Type u} [semiring A] [ A] (s : A) :
theorem subalgebra.topological_closure_minimal {R : Type u_1} {A : Type u} [semiring A] [ A] (s : A) {t : A} (h : s t) (ht : is_closed t) :
theorem subalgebra.topological_closure_comap'_homeomorph {R : Type u_1} {A : Type u} [semiring A] [ A] (s : A) {B : Type u_2} [ring B] [ B] (f : B →ₐ[R] A) (f' : B ≃ₜ A) (w : f = f') :

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.