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)
:
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₂)
:
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₁)
:
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.
Instances For
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)
:
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)
:
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)
:
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}
:
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)
:
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 ⇑φ)
:
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 ⇑φ)
:
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 ⇑φ)
:
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)
:
@[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)
:
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
Instances For
@[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)
:
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
Instances For
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 ⋯) = StarAlgHom.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 (↥(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 ⋯) 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
Instances For
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.
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)
:
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.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 := ⋯ } = ψ { val := a, property := ⋯ })
:
φ = ψ