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.instTopologicalSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [TopologicalSemiring A] (s : NonUnitalStarSubalgebra R A) : TopologicalSemiring ↥s

Equations

• ⋯ = ⋯

def NonUnitalStarSubalgebra.topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [TopologicalSemiring 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.

Equations

• s.topologicalClosure = { carrier := closure ↑s, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯, star_mem' := ⋯ }

theorem NonUnitalStarSubalgebra.le_topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [Star A] [NonUnitalSemiring A] [Module R A] [TopologicalSemiring 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] [TopologicalSemiring 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] [TopologicalSemiring 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] [TopologicalSemiring 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]

Equations

• s.nonUnitalCommSemiringTopologicalClosure hs = s.nonUnitalCommSemiringTopologicalClosure hs

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

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev NonUnitalStarSubalgebra.nonUnitalCommRingTopologicalClosure {R : Type u_1} {A : Type u_2} [CommRing R] [TopologicalSpace A] [NonUnitalRing A] [Module R A] [Star A] [TopologicalRing 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].

Equations

• s.nonUnitalCommRingTopologicalClosure hs = NonUnitalCommRing.mk ⋯