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

theorem continuous_algebraMap (R : Type u_1) (A : Type u) [] [] [Algebra R A] [] [] [] :
theorem continuous_algebraMap_iff_smul (R : Type u_1) (A : Type u) [] [] [Algebra R A] [] [] :
Continuous () Continuous fun (p : R × A) => p.1 p.2
theorem continuousSMul_of_algebraMap (R : Type u_1) (A : Type u) [] [] [Algebra R A] [] [] (h : Continuous ()) :
@[simp]
theorem algebraMapCLM_apply (R : Type u_1) (A : Type u) [] [] [Algebra R A] [] [] [] (a : R) :
() a = () a
@[simp]
theorem algebraMapCLM_toFun (R : Type u_1) (A : Type u) [] [] [Algebra R A] [] [] [] (a : R) :
() a = () a
def algebraMapCLM (R : Type u_1) (A : Type u) [] [] [Algebra R A] [] [] [] :
R →L[R] A

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

Equations
• = let __src := ; { toFun := (), map_add' := , map_smul' := , cont := }
Instances For
theorem algebraMapCLM_coe (R : Type u_1) (A : Type u) [] [] [Algebra R A] [] [] [] :
() = ()
theorem algebraMapCLM_toLinearMap (R : Type u_1) (A : Type u) [] [] [Algebra R A] [] [] [] :
() =
def Subalgebra.topologicalClosure {R : Type u_1} [] {A : Type u} [] [] [Algebra R A] (s : ) :

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

Equations
• s.topologicalClosure = let __src := s.topologicalClosure; { carrier := closure s, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
Instances For
@[simp]
theorem Subalgebra.topologicalClosure_coe {R : Type u_1} [] {A : Type u} [] [] [Algebra R A] (s : ) :
s.topologicalClosure = closure s
instance Subalgebra.topologicalSemiring {R : Type u_1} [] {A : Type u} [] [] [Algebra R A] (s : ) :
Equations
• =
theorem Subalgebra.le_topologicalClosure {R : Type u_1} [] {A : Type u} [] [] [Algebra R A] (s : ) :
s s.topologicalClosure
theorem Subalgebra.isClosed_topologicalClosure {R : Type u_1} [] {A : Type u} [] [] [Algebra R A] (s : ) :
IsClosed s.topologicalClosure
theorem Subalgebra.topologicalClosure_minimal {R : Type u_1} [] {A : Type u} [] [] [Algebra R A] (s : ) {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
def Subalgebra.commSemiringTopologicalClosure {R : Type u_1} [] {A : Type u} [] [] [Algebra R A] [] (s : ) (hs : ∀ (x y : s), x * y = y * x) :
CommSemiring s.topologicalClosure

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;
Instances For
theorem Subalgebra.topologicalClosure_comap_homeomorph {R : Type u_1} [] {A : Type u} [] [] [Algebra R A] (s : ) {B : Type u_2} [] [Ring B] [] [Algebra R B] (f : B →ₐ[R] A) (f' : B ≃ₜ A) (w : f = f') :
Subalgebra.comap f s.topologicalClosure = ().topologicalClosure

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, inline]
abbrev Subalgebra.commRingTopologicalClosure {R : Type u_1} [] {A : Type u} [] [Ring A] [Algebra R A] [] [] (s : ) (hs : ∀ (x y : s), x * y = y * x) :
CommRing s.topologicalClosure

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;
Instances For
def Algebra.elementalAlgebra (R : Type u_1) [] {A : Type u} [] [Ring A] [Algebra R A] [] (x : A) :

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

Equations
Instances For
theorem Algebra.self_mem_elementalAlgebra (R : Type u_1) [] {A : Type u} [] [Ring A] [Algebra R A] [] (x : A) :
instance instCommRingSubtypeMemSubalgebraElementalAlgebraOfT2Space {R : Type u_1} [] {A : Type u} [] [Ring A] [Algebra R A] [] [] {x : A} :
Equations
• instCommRingSubtypeMemSubalgebraElementalAlgebraOfT2Space = (Algebra.adjoin R {x}).commRingTopologicalClosure
instance DivisionRing.continuousConstSMul_rat {A : Type u_1} [] [] [] [] :

The action induced by algebraRat is continuous.

Equations
• =