mathlib3 documentation


Topological (sub)algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A topological algebra over a topological semiring R is a topological semiring 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.

The inclusion of the base ring in a topological algebra as a continuous linear map.


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


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.

def algebra.elemental_algebra (R : Type u_1) [comm_ring R] {A : Type u} [topological_space A] [ring A] [algebra R A] [topological_ring A] (x : A) :

The topological closure of the subalgebra generated by a single element.

Instances for algebra.elemental_algebra
@[protected, instance]
@[protected, instance]

The action induced by algebra_rat is continuous.