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} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [TopologicalSemiring A] (s : StarSubalgebra R A) : TopologicalSemiring ↥s

Equations

• ⋯ = ⋯

theorem StarSubalgebra.embedding_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₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) : Embedding ⇑(StarSubalgebra.inclusion h)

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

theorem StarSubalgebra.closedEmbedding_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₁ : StarSubalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) (hS₁ : IsClosed ↑S₁) : ClosedEmbedding ⇑(StarSubalgebra.inclusion h)

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

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] [TopologicalSemiring 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 = let __src := s.topologicalClosure; { carrier := closure ↑s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, star_mem' := ⋯ }

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] [TopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) : s.topologicalClosure.toSubalgebra = s.topologicalClosure

@[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] [TopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) : ↑s.topologicalClosure = closure ↑s

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] [TopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) : s ≤ s.topologicalClosure

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] [TopologicalSemiring A] [ContinuousStar A] (s : StarSubalgebra R A) : IsClosed ↑s.topologicalClosure

instance StarSubalgebra.instCompleteSpaceSubtypeMemTopologicalClosure {R : Type u_1} [CommSemiring R] [StarRing R] {A : Type u_4} [UniformSpace A] [CompleteSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} : CompleteSpace ↥S.topologicalClosure

Equations

• ⋯ = ⋯

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] [TopologicalSemiring A] [ContinuousStar A] {s : StarSubalgebra R A} {t : StarSubalgebra R A} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

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] [TopologicalSemiring A] [ContinuousStar A] : Monotone StarSubalgebra.topologicalClosure

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] [TopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [TopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap ⇑φ) : (StarSubalgebra.map φ s).topologicalClosure ≤ StarSubalgebra.map φ s.topologicalClosure

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] [TopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [TopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : Continuous ⇑φ) : StarSubalgebra.map φ s.topologicalClosure ≤ (StarSubalgebra.map φ s).topologicalClosure

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] [TopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [TopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : ClosedEmbedding ⇑φ) : (StarSubalgebra.map φ s).topologicalClosure = StarSubalgebra.map φ s.topologicalClosure

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] [TopologicalSemiring A] [ContinuousStar A] (s : Subalgebra R A) : (star s).topologicalClosure = star s.topologicalClosure

@[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] [TopologicalSemiring 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

@[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] [TopologicalRing 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

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] [TopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [T2Space B] {S : StarSubalgebra R A} {φ : ↥S.topologicalClosure →⋆ₐ[R] B} {ψ : ↥S.topologicalClosure →⋆ₐ[R] B} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ.comp (StarSubalgebra.inclusion ⋯) = ψ.comp (StarSubalgebra.inclusion ⋯)) : φ = ψ

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} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [TopologicalSemiring 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] [StarAlgHomClass F R (↥S.topologicalClosure) B] {φ : F} {ψ : F} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : ∀ (x : ↥S), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x)) : φ = ψ

def elementalStarAlgebra (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) : StarSubalgebra R A

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

Equations

• elementalStarAlgebra R x = (StarAlgebra.adjoin R {x}).topologicalClosure

theorem elementalStarAlgebra.self_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) : x ∈ elementalStarAlgebra R x

theorem elementalStarAlgebra.star_self_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) : star x ∈ elementalStarAlgebra R x

instance elementalStarAlgebra.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] [T2Space A] {x : A} [IsStarNormal x] : CommSemiring ↥(elementalStarAlgebra R x)

The elementalStarAlgebra generated by a normal element is commutative.

Equations

• elementalStarAlgebra.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal R = (StarAlgebra.adjoin R {x}).commSemiringTopologicalClosure ⋯

instance elementalStarAlgebra.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] [TopologicalRing A] [ContinuousStar A] [T2Space A] {x : A} [IsStarNormal x] : CommRing ↥(elementalStarAlgebra R x)

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} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) : IsClosed ↑(elementalStarAlgebra R x)

instance elementalStarAlgebra.instCompleteSpaceSubtypeMemStarSubalgebra (R : Type u_1) [CommSemiring R] [StarRing R] {A : Type u_4} [UniformSpace A] [CompleteSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) : CompleteSpace ↥(elementalStarAlgebra R x)

Equations

• ⋯ = ⋯

theorem elementalStarAlgebra.le_of_isClosed_of_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} (hS : IsClosed ↑S) {x : A} (hx : x ∈ S) : elementalStarAlgebra R x ≤ S

theorem elementalStarAlgebra.closedEmbedding_coe (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule 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} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {x : A} {y : A} (hy : y ∈ elementalStarAlgebra R x) {P : (u : A) → u ∈ elementalStarAlgebra R x → Prop} (self : P x ⋯) (star_self : P (star x) ⋯) (algebraMap : ∀ (r : R), P ((_root_.algebraMap R A) r) ⋯) (add : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u + v) ⋯) (mul : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u * v) ⋯) (closure : ∀ (s : Set A) (hs : s ⊆ ↑(elementalStarAlgebra R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ _root_.closure s), P v ⋯) : P y hy

theorem elementalStarAlgebra.starAlgHomClass_ext (R : Type u_1) {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring 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 (↥(elementalStarAlgebra R a)) B] [AlgHomClass F R (↥(elementalStarAlgebra R a)) B] [StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B] {φ : F} {ψ : F} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩) : φ = ψ