mathlib documentation

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.

def subalgebra.topological_closure {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_ring A] (s : subalgebra R A) :

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

Equations
@[simp]
theorem subalgebra.topological_closure_minimal {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_ring A] (s : subalgebra R A) {t : subalgebra R A} (h : s t) (ht : is_closed t) :
theorem subalgebra.topological_closure_comap'_homeomorph {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_ring A] (s : subalgebra R A) {B : Type u_2} [topological_space B] [ring B] [topological_ring B] [algebra R 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.