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

source
instance StarSubalgebra.instIsTopologicalSemiringSubtypeMem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] (s : StarSubalgebra R A) :
IsTopologicalSemiring ↥s
source
theorem StarSubalgebra.isEmbedding_inclusion {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) :
Topology.IsEmbedding ⇑(inclusion h)

The `StarSubalgebra.inclusion` of a star subalgebra is an embedding.

source
theorem StarSubalgebra.isClosedEmbedding_inclusion {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) (hS₁ : IsClosed ↑S₁) :
Topology.IsClosedEmbedding ⇑(inclusion h)

The `StarSubalgebra.inclusion` of a closed star subalgebra is a `IsClosedEmbedding`.

source
def StarSubalgebra.topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) :
StarSubalgebra R A

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

Equations

- s.topologicalClosure = { carrier := closure ↑s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, star_mem' := ⋯ }

Instances For

source
theorem StarSubalgebra.topologicalClosure_toSubalgebra_comm {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) :
s.topologicalClosure.toSubalgebra = s.topologicalClosure
source
@[simp]
theorem StarSubalgebra.topologicalClosure_coe {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) :
↑s.topologicalClosure = closure ↑s
source
theorem StarSubalgebra.le_topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) :
s ≤ s.topologicalClosure
source
theorem StarSubalgebra.isClosed_topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) :
IsClosed ↑s.topologicalClosure
source
instance StarSubalgebra.instCompleteSpaceSubtypeMemTopologicalClosure {R : Type u_1} [CommSemiring R] [StarRing R] {A : Type u_4} [UniformSpace A] [CompleteSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} :
CompleteSpace ↥S.topologicalClosure
source
theorem StarSubalgebra.topologicalClosure_minimal {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] {s t : StarSubalgebra R A} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
theorem StarSubalgebra.topologicalClosure_mono {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] :
Monotone topologicalClosure
source
theorem StarSubalgebra.topologicalClosure_map_le {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap ⇑φ) :
(map φ s).topologicalClosure ≤ map φ s.topologicalClosure
source
theorem StarSubalgebra.map_topologicalClosure_le {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : Continuous ⇑φ) :
map φ s.topologicalClosure ≤ (map φ s).topologicalClosure
source
theorem StarSubalgebra.topologicalClosure_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap ⇑φ) (hφ' : Continuous ⇑φ) :
(map φ s).topologicalClosure = map φ s.topologicalClosure
source
theorem StarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [T2Space A] (s : Set A) :
(StarAlgebra.adjoin R s).topologicalClosure ≤ centralizer R ↑(centralizer R s)
source
theorem Subalgebra.topologicalClosure_star_comm {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] (s : Subalgebra R A) :
(star s).topologicalClosure = star s.topologicalClosure
source
@[reducible, inline]
abbrev StarSubalgebra.commSemiringTopologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [T2Space A] (s : StarSubalgebra R A) (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

source
@[reducible, inline]
abbrev StarSubalgebra.commRingTopologicalClosure {R : Type u_4} {A : Type u_5} [CommRing R] [StarRing R] [TopologicalSpace A] [Ring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalRing A] [ContinuousStar A] [T2Space A] (s : StarSubalgebra R A) (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

source
theorem StarAlgHom.ext_topologicalClosure {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [T2Space B] {S : StarSubalgebra R A} {φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ.comp (StarSubalgebra.inclusion ⋯) = ψ.comp (StarSubalgebra.inclusion ⋯)) :
φ = ψ

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

source
theorem StarAlgHomClass.ext_topologicalClosure {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [T2Space B] {F : Type u_4} {S : StarSubalgebra R A} [FunLike F (↥S.topologicalClosure) B] [AlgHomClass F R (↥S.topologicalClosure) B] [StarHomClass F (↥S.topologicalClosure) B] {φ ψ : F} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : ∀ (x : ↥S), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x)) :
φ = ψ
source
def StarAlgebra.elemental (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :
StarSubalgebra R A

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

Equations

- StarAlgebra.elemental R x = (StarAlgebra.adjoin R {x}).topologicalClosure

Instances For

source
@[simp]
theorem StarAlgebra.elemental.self_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :
x ∈ elemental R x
source
@[simp]
theorem StarAlgebra.elemental.star_self_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :
star x ∈ elemental R x
source
instance StarAlgebra.elemental.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] [T2Space A] {x : A} [IsStarNormal x] :
CommSemiring ↥(elemental R x)

The `elemental` star subalgebra generated by a normal element is commutative.

Equations

- StarAlgebra.elemental.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal R = (StarAlgebra.adjoin R {x}).commSemiringTopologicalClosure ⋯

source
instance StarAlgebra.elemental.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal {R : Type u_4} {A : Type u_5} [CommRing R] [StarRing R] [TopologicalSpace A] [Ring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalRing A] [ContinuousStar A] [T2Space A] {x : A} [IsStarNormal x] :
CommRing ↥(elemental R x)

The `elemental` generated by a normal element is commutative.

Equations

- StarAlgebra.elemental.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal = (StarAlgebra.adjoin R {x}).commRingTopologicalClosure ⋯

source
theorem StarAlgebra.elemental.isClosed (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :
IsClosed ↑(elemental R x)
source
instance StarAlgebra.elemental.instCompleteSpaceSubtypeMemStarSubalgebra (R : Type u_1) [CommSemiring R] [StarRing R] {A : Type u_4} [UniformSpace A] [CompleteSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :
CompleteSpace ↥(elemental R x)
source
theorem StarAlgebra.elemental.le_of_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} (hS : IsClosed ↑S) {x : A} (hx : x ∈ S) :
elemental R x ≤ S
source
theorem StarAlgebra.elemental.le_iff_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {x : A} {s : StarSubalgebra R A} (hs : IsClosed ↑s) :
elemental R x ≤ s ↔ x ∈ s
source
theorem StarAlgebra.elemental.isClosedEmbedding_coe (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :
Topology.IsClosedEmbedding Subtype.val

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

source
theorem StarAlgebra.elemental.le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] [T2Space A] (x : A) :
elemental R x ≤ StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R {x})
source
theorem StarAlgebra.elemental.induction_on (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {x y : A} (hy : y ∈ elemental R x) {P : (u : A) → u ∈ elemental R x → Prop} (self : P x ⋯) (star_self : P (star x) ⋯) (algebraMap : ∀ (r : R), P ((algebraMap R A) r) ⋯) (add : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u + v) ⋯) (mul : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u * v) ⋯) (closure : ∀ (s : Set A) (hs : s ⊆ ↑(elemental R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure s), P v ⋯) :
P y hy
source
theorem StarAlgebra.elemental.starAlgHomClass_ext (R : Type u_1) {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] [TopologicalSpace B] [Semiring B] [StarRing B] [Algebra R B] [T2Space B] {F : Type u_4} {a : A} [FunLike F (↥(elemental R a)) B] [AlgHomClass F R (↥(elemental R a)) B] [StarHomClass F (↥(elemental R a)) B] {φ ψ : F} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩) :
φ = ψ