# mathlibdocumentation

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.

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)
@[continuity]
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)) :
@[protected, instance]
def subalgebra.has_continuous_smul {R : Type u_1} {A : Type u} [semiring A] [ A] [ A] (s : 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) :
@[protected, instance]
def subalgebra.topological_semiring {R : Type u_1} {A : Type u} [semiring 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) :
def subalgebra.comm_semiring_topological_closure {R : Type u_1} {A : Type u} [semiring A] [ A] [t2_space A] (s : A) (hs : ∀ (x y : s), x * y = y * x) :

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

Equations
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.

@[reducible]
def subalgebra.comm_ring_topological_closure {R : Type u_1} [comm_ring R] {A : Type u} [ring A] [ A] [t2_space A] (s : A) (hs : ∀ (x y : s), x * y = y * x) :

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

Equations
def algebra.elemental_algebra (R : Type u_1) [comm_ring R] {A : Type u} [ring A] [ A] (x : A) :
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} [ring A] [ A] (x : A) :
@[protected, instance]
def algebra.elemental_algebra.comm_ring {R : Type u_1} [comm_ring R] {A : Type u} [ring A] [ A] [t2_space A] {x : A} :
Equations
@[protected, instance]

The action induced by algebra_rat is continuous.