Non-unital topological (sub)algebras

A non-unital topological algebra over a topological semiring R is a topological (non-unital) semiring with a compatible continuous scalar multiplication by elements of R. We reuse typeclass ContinuousSMul to express the latter condition.

Results

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

instance NonUnitalSubalgebra.instTopologicalSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [NonUnitalSemiring A] [Module R A] [TopologicalSemiring A] (s : NonUnitalSubalgebra R A) : TopologicalSemiring ↥s

Equations

• ⋯ = ⋯

def NonUnitalSubalgebra.topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [NonUnitalSemiring A] [Module R A] [TopologicalSemiring A] [ContinuousConstSMul R A] (s : NonUnitalSubalgebra R A) : NonUnitalSubalgebra R A

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

Equations

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

theorem NonUnitalSubalgebra.le_topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [NonUnitalSemiring A] [Module R A] [TopologicalSemiring A] [ContinuousConstSMul R A] (s : NonUnitalSubalgebra R A) : s ≤ s.topologicalClosure

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

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

@[reducible, inline]

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

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

See note [reducible non-instances].

Equations

• s.nonUnitalCommSemiringTopologicalClosure hs = s.nonUnitalCommSemiringTopologicalClosure hs

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

Equations

• ⋯ = ⋯

@[reducible, inline]

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

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

See note [reducible non-instances].

Equations

• s.nonUnitalCommRingTopologicalClosure hs = NonUnitalCommRing.mk ⋯