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.instIsTopologicalSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring A] (s : NonUnitalSubalgebra R A) : IsTopologicalSemiring ↥s

def NonUnitalSubalgebra.topologicalClosure {R : Type u_1} {A : Type u_2} [CommSemiring R] [TopologicalSpace A] [NonUnitalSemiring A] [Module R A] [IsTopologicalSemiring 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] [IsTopologicalSemiring 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] [IsTopologicalSemiring 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] [IsTopologicalSemiring 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] [IsTopologicalSemiring 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.instIsTopologicalRing {R : Type u_1} {A : Type u_2} [CommRing R] [TopologicalSpace A] [NonUnitalRing A] [Module R A] [IsTopologicalRing A] (s : NonUnitalSubalgebra R A) : IsTopologicalRing ↥s

@[reducible, inline]

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

def NonUnitalAlgebra.elemental (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] (x : A) : NonUnitalSubalgebra R A

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

Equations

• NonUnitalAlgebra.elemental R x = (NonUnitalAlgebra.adjoin R {x}).topologicalClosure

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

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

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

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

instance NonUnitalAlgebra.elemental.instNonUnitalCommSemiringSubtypeMemNonUnitalSubalgebraOfT2Space (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] [T2Space A] {x : A} : NonUnitalCommSemiring ↥(elemental R x)

Equations

• NonUnitalAlgebra.elemental.instNonUnitalCommSemiringSubtypeMemNonUnitalSubalgebraOfT2Space R = (NonUnitalAlgebra.adjoin R {x}).nonUnitalCommSemiringTopologicalClosure ⋯

instance NonUnitalAlgebra.elemental.instNonUnitalCommRingSubtypeMemNonUnitalSubalgebraOfT2Space {R : Type u_3} {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [TopologicalSpace A] [IsTopologicalRing A] [ContinuousConstSMul R A] [T2Space A] {x : A} : NonUnitalCommRing ↥(elemental R x)

Equations

• NonUnitalAlgebra.elemental.instNonUnitalCommRingSubtypeMemNonUnitalSubalgebraOfT2Space = NonUnitalCommRing.mk ⋯

instance NonUnitalAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalSubalgebra (R : Type u_1) [CommSemiring R] {A : Type u_3} [UniformSpace A] [CompleteSpace A] [NonUnitalSemiring A] [IsTopologicalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [ContinuousConstSMul R A] (x : A) : CompleteSpace ↥(elemental R x)

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

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