Non-unital topological star (sub)algebras

A non-unital topological star algebra over a topological semiring R is a topological (non-unital) semiring with a compatible continuous scalar multiplication by elements of R and a continuous star operation. We reuse typeclasses ContinuousSMul and ContinuousStar to express the latter two conditions.

Results

Any non-unital star subalgebra of a non-unital topological star algebra is itself a non-unital topological star algebra, and its closure is again a non-unital star subalgebra.

instance NonUnitalStarSubalgebra.instIsTopologicalSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] (s : NonUnitalStarSubalgebra R A) : IsTopologicalSemiring ↥s

def NonUnitalStarSubalgebra.topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousStar A] [ContinuousConstSMul R A] (s : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra R A

The (topological) closure of a non-unital star subalgebra of a non-unital topological star algebra is itself a non-unital star subalgebra.

theorem NonUnitalStarSubalgebra.le_topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousStar A] [ContinuousConstSMul R A] (s : NonUnitalStarSubalgebra R A) : s ≤ s.topologicalClosure

theorem NonUnitalStarSubalgebra.isClosed_topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousStar A] [ContinuousConstSMul R A] (s : NonUnitalStarSubalgebra R A) : IsClosed ↑s.topologicalClosure

theorem NonUnitalStarSubalgebra.topologicalClosure_minimal {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousStar A] [ContinuousConstSMul R A] (s : NonUnitalStarSubalgebra R A) {t : NonUnitalStarSubalgebra R A} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

@[reducible, inline]

abbrev NonUnitalStarSubalgebra.nonUnitalCommSemiringTopologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] [ContinuousStar A] [ContinuousConstSMul R A] [T2Space A] (s : NonUnitalStarSubalgebra R A) (hs : ∀ (x y : ↥s), x * y = y * x) : NonUnitalCommSemiring ↥s.topologicalClosure

If a non-unital star subalgebra of a non-unital topological star algebra is commutative, then so is its topological closure.

See note [reducible non-instances]

instance NonUnitalStarSubalgebra.instIsTopologicalRing {R : Type u_1} {A : Type u_2} [CommRing R] [TopologicalSpace A] [NonUnitalRing A] [Module R A] [Star A] [IsTopologicalRing A] (s : NonUnitalStarSubalgebra R A) : IsTopologicalRing ↥s

@[reducible, inline]

abbrev NonUnitalStarSubalgebra.nonUnitalCommRingTopologicalClosure {R : Type u_1} {A : Type u_2} [CommRing R] [TopologicalSpace A] [NonUnitalRing A] [Module R A] [Star A] [IsTopologicalRing A] [ContinuousStar A] [ContinuousConstSMul R A] [T2Space A] (s : NonUnitalStarSubalgebra R A) (hs : ∀ (x y : ↥s), x * y = y * x) : NonUnitalCommRing ↥s.topologicalClosure

If a non-unital star subalgebra of a non-unital topological star algebra is commutative, then so is its topological closure.

See note [reducible non-instances].

def NonUnitalStarAlgebra.elemental (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] (x : A) : NonUnitalStarSubalgebra R A

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

@[simp]

theorem NonUnitalStarAlgebra.elemental.self_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] (x : A) : x ∈ elemental R x

@[simp]

theorem NonUnitalStarAlgebra.elemental.star_self_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] (x : A) : star x ∈ elemental R x

theorem NonUnitalStarAlgebra.elemental.le_of_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] {x : A} {s : NonUnitalStarSubalgebra R A} (hs : IsClosed ↑s) (hx : x ∈ s) : elemental R x ≤ s

theorem NonUnitalStarAlgebra.elemental.le_iff_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] {x : A} {s : NonUnitalStarSubalgebra R A} (hs : IsClosed ↑s) : elemental R x ≤ s ↔ x ∈ s

instance NonUnitalStarAlgebra.elemental.isClosed (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] (x : A) : IsClosed ↑(elemental R x)

instance NonUnitalStarAlgebra.elemental.instNonUnitalCommSemiringSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] [T2Space A] {x : A} [IsStarNormal x] : NonUnitalCommSemiring ↥(elemental R x)

instance NonUnitalStarAlgebra.elemental.instNonUnitalCommRingSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal {R : Type u_3} {A : Type u_4} [CommRing R] [StarRing R] [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalRing A] [ContinuousConstSMul R A] [ContinuousStar A] [T2Space A] {x : A} [IsStarNormal x] : NonUnitalCommRing ↥(elemental R x)

instance NonUnitalStarAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra (R : Type u_1) [CommSemiring R] [StarRing R] {A : Type u_3} [UniformSpace A] [CompleteSpace A] [NonUnitalSemiring A] [StarRing A] [IsTopologicalSemiring A] [ContinuousStar A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [ContinuousConstSMul R A] (x : A) : CompleteSpace ↥(elemental R x)

theorem NonUnitalStarAlgebra.elemental.isClosedEmbedding_coe (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [ContinuousStar A] (x : A) : Topology.IsClosedEmbedding Subtype.val

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