# Topological star (sub)algebras #

A topological star algebra over a topological semiring R is a topological semiring with a compatible continuous scalar multiplication by elements of R and a continuous star operation. We reuse typeclass ContinuousSMul for topological algebras.

## Results #

This is just a minimal stub for now!

The topological closure of a star subalgebra is still a star subalgebra, which as a star algebra is a topological star algebra.

instance StarSubalgebra.instTopologicalSemiringSubtypeMem {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] (s : ) :
Equations
• =
theorem StarSubalgebra.embedding_inclusion {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] {S₁ : } {S₂ : } (h : S₁ S₂) :

The StarSubalgebra.inclusion of a star subalgebra is an Embedding.

theorem StarSubalgebra.closedEmbedding_inclusion {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] {S₁ : } {S₂ : } (h : S₁ S₂) (hS₁ : IsClosed S₁) :

The StarSubalgebra.inclusion of a closed star subalgebra is a ClosedEmbedding.

def StarSubalgebra.topologicalClosure {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] (s : ) :

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

Equations
• s.topologicalClosure = let __src := s.topologicalClosure; { carrier := closure s, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := , star_mem' := }
Instances For
theorem StarSubalgebra.topologicalClosure_toSubalgebra_comm {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] (s : ) :
s.topologicalClosure.toSubalgebra = s.topologicalClosure
@[simp]
theorem StarSubalgebra.topologicalClosure_coe {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] (s : ) :
s.topologicalClosure = closure s
theorem StarSubalgebra.le_topologicalClosure {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] (s : ) :
s s.topologicalClosure
theorem StarSubalgebra.isClosed_topologicalClosure {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] (s : ) :
IsClosed s.topologicalClosure
instance StarSubalgebra.instCompleteSpaceSubtypeMemTopologicalClosure {R : Type u_1} [] [] {A : Type u_4} [] [] [] [] [] [Algebra R A] [] {S : } :
CompleteSpace S.topologicalClosure
Equations
• =
theorem StarSubalgebra.topologicalClosure_minimal {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] {s : } {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
theorem StarSubalgebra.topologicalClosure_mono {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] :
Monotone StarSubalgebra.topologicalClosure
theorem StarSubalgebra.topologicalClosure_map_le {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [Algebra R A] [] [] [] [] [] [Algebra R B] [] [] [] (s : ) (φ : A →⋆ₐ[R] B) (hφ : ) :
.topologicalClosure StarSubalgebra.map φ s.topologicalClosure
theorem StarSubalgebra.map_topologicalClosure_le {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [Algebra R A] [] [] [] [] [] [Algebra R B] [] [] [] (s : ) (φ : A →⋆ₐ[R] B) (hφ : ) :
StarSubalgebra.map φ s.topologicalClosure .topologicalClosure
theorem StarSubalgebra.topologicalClosure_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [Algebra R A] [] [] [] [] [] [Algebra R B] [] [] [] (s : ) (φ : A →⋆ₐ[R] B) (hφ : ) :
.topologicalClosure = StarSubalgebra.map φ s.topologicalClosure
theorem Subalgebra.topologicalClosure_star_comm {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] (s : ) :
(star s).topologicalClosure = star s.topologicalClosure
@[reducible, inline]
abbrev StarSubalgebra.commSemiringTopologicalClosure {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] [] [] [] (s : ) (hs : ∀ (x y : s), x * y = y * x) :
CommSemiring s.topologicalClosure

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

Equations
• s.commSemiringTopologicalClosure hs = s.commSemiringTopologicalClosure hs
Instances For
@[reducible, inline]
abbrev StarSubalgebra.commRingTopologicalClosure {R : Type u_4} {A : Type u_5} [] [] [] [Ring A] [Algebra R A] [] [] [] [] [] (s : ) (hs : ∀ (x y : s), x * y = y * x) :
CommRing s.topologicalClosure

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

Equations
• s.commRingTopologicalClosure hs = s.commRingTopologicalClosure hs
Instances For
theorem StarAlgHom.ext_topologicalClosure {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [Algebra R A] [] [] [] [] [] [Algebra R B] [] [] {S : } {φ : S.topologicalClosure →⋆ₐ[R] B} {ψ : S.topologicalClosure →⋆ₐ[R] B} (hφ : ) (hψ : ) (h : φ.comp = ψ.comp ) :
φ = ψ

Continuous StarAlgHoms from the topological closure of a StarSubalgebra whose compositions with the StarSubalgebra.inclusion map agree are, in fact, equal.

theorem StarAlgHomClass.ext_topologicalClosure {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [Algebra R A] [] [] [] [] [] [Algebra R B] [] [] {F : Type u_4} {S : } [FunLike F (↥S.topologicalClosure) B] [AlgHomClass F R (↥S.topologicalClosure) B] [StarAlgHomClass F R (↥S.topologicalClosure) B] {φ : F} {ψ : F} (hφ : ) (hψ : ) (h : ∀ (x : S), φ ( x) = ψ ( x)) :
φ = ψ
def elementalStarAlgebra (R : Type u_1) {A : Type u_2} [] [] [] [] [] [] [Algebra R A] [] (x : A) :

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

Equations
Instances For
theorem elementalStarAlgebra.self_mem (R : Type u_1) {A : Type u_2} [] [] [] [] [] [] [Algebra R A] [] (x : A) :
theorem elementalStarAlgebra.star_self_mem (R : Type u_1) {A : Type u_2} [] [] [] [] [] [] [Algebra R A] [] (x : A) :
instance elementalStarAlgebra.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal (R : Type u_1) {A : Type u_2} [] [] [] [] [] [] [Algebra R A] [] [] {x : A} [] :

The elementalStarAlgebra generated by a normal element is commutative.

Equations
instance elementalStarAlgebra.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal {R : Type u_4} {A : Type u_5} [] [] [] [Ring A] [Algebra R A] [] [] [] [] [] {x : A} [] :

The elementalStarAlgebra generated by a normal element is commutative.

Equations
• elementalStarAlgebra.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal = (StarAlgebra.adjoin R {x}).commRingTopologicalClosure
theorem elementalStarAlgebra.isClosed (R : Type u_1) {A : Type u_2} [] [] [] [] [] [] [Algebra R A] [] (x : A) :
instance elementalStarAlgebra.instCompleteSpaceSubtypeMemStarSubalgebra (R : Type u_1) [] [] {A : Type u_4} [] [] [] [] [] [Algebra R A] [] (x : A) :
Equations
• =
theorem elementalStarAlgebra.le_of_isClosed_of_mem (R : Type u_1) {A : Type u_2} [] [] [] [] [] [] [Algebra R A] [] {S : } (hS : IsClosed S) {x : A} (hx : x S) :
theorem elementalStarAlgebra.closedEmbedding_coe (R : Type u_1) {A : Type u_2} [] [] [] [] [] [] [Algebra R A] [] (x : A) :
ClosedEmbedding Subtype.val

The coercion from an elemental algebra to the full algebra as a ClosedEmbedding.

theorem elementalStarAlgebra.induction_on (R : Type u_1) {A : Type u_2} [] [] [] [] [] [] [Algebra R A] [] {x : A} {y : A} (hy : ) {P : (u : A) → Prop} (self : P x ) (star_self : P (star x) ) (algebraMap : ∀ (r : R), P ( r) ) (add : ∀ (u : A) (hu : ) (v : A) (hv : ), P u huP v hvP (u + v) ) (mul : ∀ (u : A) (hu : ) (v : A) (hv : ), P u huP v hvP (u * v) ) (closure : ∀ (s : Set A) (hs : s ), (∀ (u : A) (hu : u s), P u )∀ (v : A) (hv : ), P v ) :
P y hy
theorem elementalStarAlgebra.starAlgHomClass_ext (R : Type u_1) {A : Type u_2} {B : Type u_3} [] [] [] [] [] [] [Algebra R A] [] [] [] [] [Algebra R B] [] {F : Type u_4} {a : A} [FunLike F (↥) B] [AlgHomClass F R (↥) B] [StarAlgHomClass F R (↥) B] {φ : F} {ψ : F} (hφ : ) (hψ : ) (h : φ a, = ψ a, ) :
φ = ψ