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.instTopologicalSemiringSubtypeMemStarSubalgebraInstMembershipSetLikeInstTopologicalSpaceSubtypeToNonUnitalNonAssocSemiringToNonAssocSemiringToNonAssocSemiringToSubsemiringToSubalgebra {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

• (_ : TopologicalSemiring ↥s) = (_ : TopologicalSemiring ↥s.toSubalgebra)

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

• One or more equations did not get rendered due to their size.

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) : (StarSubalgebra.topologicalClosure s).toSubalgebra = Subalgebra.topologicalClosure s.toSubalgebra

@[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) : ↑(StarSubalgebra.topologicalClosure s) = 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 ≤ StarSubalgebra.topologicalClosure s

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 ↑(StarSubalgebra.topologicalClosure s)

instance StarSubalgebra.instCompleteSpaceSubtypeMemStarSubalgebraInstMembershipSetLikeTopologicalClosureToTopologicalSpaceInstUniformSpaceSubtype {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 ↥(StarSubalgebra.topologicalClosure S)

Equations

• (_ : CompleteSpace ↥(StarSubalgebra.topologicalClosure S)) = (_ : CompleteSpace ↑(closure ↑S))

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) : StarSubalgebra.topologicalClosure s ≤ 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.topologicalClosure (StarSubalgebra.map φ s) ≤ StarSubalgebra.map φ (StarSubalgebra.topologicalClosure s)

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 φ (StarSubalgebra.topologicalClosure s) ≤ StarSubalgebra.topologicalClosure (StarSubalgebra.map φ s)

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.topologicalClosure (StarSubalgebra.map φ s) = StarSubalgebra.map φ (StarSubalgebra.topologicalClosure s)

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) : Subalgebra.topologicalClosure (star s) = star (Subalgebra.topologicalClosure s)

@[reducible]

def 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 ↥(StarSubalgebra.topologicalClosure s)

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

Equations

• StarSubalgebra.commSemiringTopologicalClosure s hs = Subalgebra.commSemiringTopologicalClosure s.toSubalgebra hs

@[reducible]

def 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 ↥(StarSubalgebra.topologicalClosure s)

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

Equations

• StarSubalgebra.commRingTopologicalClosure s hs = Subalgebra.commRingTopologicalClosure s.toSubalgebra 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} {φ : ↥(StarSubalgebra.topologicalClosure S) →⋆ₐ[R] B} {ψ : ↥(StarSubalgebra.topologicalClosure S) →⋆ₐ[R] B} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : StarAlgHom.comp φ (StarSubalgebra.inclusion (_ : S ≤ StarSubalgebra.topologicalClosure S)) = StarAlgHom.comp ψ (StarSubalgebra.inclusion (_ : S ≤ StarSubalgebra.topologicalClosure S))) : φ = ψ

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 (↥(StarSubalgebra.topologicalClosure S)) B] [AlgHomClass F R (↥(StarSubalgebra.topologicalClosure S)) B] [StarAlgHomClass F R (↥(StarSubalgebra.topologicalClosure S)) B] {φ : F} {ψ : F} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : ∀ (x : ↥S), φ ((StarSubalgebra.inclusion (_ : S ≤ StarSubalgebra.topologicalClosure S)) x) = ψ ((StarSubalgebra.inclusion (_ : S ≤ StarSubalgebra.topologicalClosure S)) 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 = StarSubalgebra.topologicalClosure (StarSubalgebra.adjoin R {x})

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.instCommSemiringSubtypeMemStarSubalgebraInstMembershipSetLikeElementalStarAlgebra (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

• One or more equations did not get rendered due to their size.

instance elementalStarAlgebra.instCommRingSubtypeMemStarSubalgebraToCommSemiringToSemiringInstMembershipSetLikeElementalStarAlgebraToTopologicalSemiringToNonUnitalNonAssocRingToNonAssocRing {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

• One or more equations did not get rendered due to their size.

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.instCompleteSpaceSubtypeMemStarSubalgebraInstMembershipSetLikeElementalStarAlgebraToTopologicalSpaceInstUniformSpaceSubtype (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

• (_ : CompleteSpace ↥(elementalStarAlgebra R x)) = (_ : CompleteSpace ↑(closure ↑(StarSubalgebra.adjoin R {x})))

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.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 : φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } = ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }) : φ = ψ