# 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 `ContinuousSMul`

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.

## Equations

- algebraMapCLM R A = let __src := Algebra.linearMap R A; { toFun := ⇑(algebraMap R A), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

## Instances For

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

## Equations

## Instances For

## Equations

- ⋯ = ⋯

If a subalgebra of a topological algebra is commutative, then so is its topological closure.

## Equations

- s.commSemiringTopologicalClosure hs = let __src := s.topologicalClosure.toSemiring; let __src_1 := s.commMonoidTopologicalClosure hs; CommSemiring.mk ⋯

## Instances For

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.

If a subalgebra of a topological algebra is commutative, then so is its topological closure. See note [reducible non-instances].

## Equations

- s.commRingTopologicalClosure hs = let __src := s.topologicalClosure.toRing; let __src_1 := s.commMonoidTopologicalClosure hs; CommRing.mk ⋯

## Instances For

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

## Equations

- Algebra.elementalAlgebra R x = (Algebra.adjoin R {x}).topologicalClosure

## Instances For

## Equations

- instCommRingSubtypeMemSubalgebraElementalAlgebraOfT2Space = (Algebra.adjoin R {x}).commRingTopologicalClosure ⋯

The action induced by `algebraRat`

is continuous.

## Equations

- ⋯ = ⋯