mathlib documentation

topology.algebra.algebra

Topological (sub)algebras #

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.

@[continuity]
@[simp]
theorem algebra_map_clm_coe_apply (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] (ᾰ : R) :
def algebra_map_clm (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] :
R →L[R] A

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

Equations
@[simp]
theorem algebra_map_clm_apply (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] (ᾰ : R) :
(algebra_map_clm R A) = (algebra_map R A)
@[protected, instance]
def subalgebra.topological_closure {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) :

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

Equations
@[protected, instance]
theorem subalgebra.topological_closure_minimal {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) {t : subalgebra R A} (h : s t) (ht : is_closed t) :

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.

Equations
Instances for algebra.elemental_algebra
theorem algebra.self_mem_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) :
@[protected, instance]
Equations
@[protected, instance]

The action induced by algebra_rat is continuous.