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.

source

instance StarSubalgebra.instTopologicalSemiringSubtypeMem {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) :

TopologicalSemiring ↥s

Equations

⋯ = ⋯

source

theorem StarSubalgebra.isEmbedding_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₂) :

IsEmbedding ⇑(StarSubalgebra.inclusion h)

The StarSubalgebra.inclusion of a star subalgebra is an Embedding.

source

@[deprecated StarSubalgebra.isEmbedding_inclusion]

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₂) :

IsEmbedding ⇑(StarSubalgebra.inclusion h)

Alias of StarSubalgebra.isEmbedding_inclusion.

The StarSubalgebra.inclusion of a star subalgebra is an Embedding.

source

theorem StarSubalgebra.isClosedEmbedding_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₁) :

IsClosedEmbedding ⇑(StarSubalgebra.inclusion h)

The StarSubalgebra.inclusion of a closed star subalgebra is a IsClosedEmbedding.

source

@[deprecated StarSubalgebra.isClosedEmbedding_inclusion]

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₁) :

IsClosedEmbedding ⇑(StarSubalgebra.inclusion h)

Alias of StarSubalgebra.isClosedEmbedding_inclusion.

The StarSubalgebra.inclusion of a closed star subalgebra is a IsClosedEmbedding.

source

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

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

Instances For

source

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) :

s.topologicalClosure.toSubalgebra = s.topologicalClosure

source

@[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) :

↑s.topologicalClosure = closure ↑s

source

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) :

s ≤ s.topologicalClosure

source

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) :

IsClosed ↑s.topologicalClosure

source

instance StarSubalgebra.instCompleteSpaceSubtypeMemTopologicalClosure {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} :

CompleteSpace ↥S.topologicalClosure

Equations

⋯ = ⋯

source

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) :

s.topologicalClosure ≤ t

source

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

source

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 ⇑φ) :

(StarSubalgebra.map φ s).topologicalClosure ≤ StarSubalgebra.map φ s.topologicalClosure

source

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 ⇑φ) :

StarSubalgebra.map φ s.topologicalClosure ≤ (StarSubalgebra.map φ s).topologicalClosure

source

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φ : IsClosedEmbedding ⇑φ) :

(StarSubalgebra.map φ s).topologicalClosure = StarSubalgebra.map φ s.topologicalClosure

source

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) :

(star s).topologicalClosure = star s.topologicalClosure

source

@[reducible, inline]

abbrev 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) :

CommSemiring ↥s.topologicalClosure

If a star subalgebra of a topological star algebra is commutative, then so is its topological closure. See note [reducible non-instances].

Equations

s.commSemiringTopologicalClosure hs = s.commSemiringTopologicalClosure hs

Instances For

source

@[reducible, inline]

abbrev 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) :

CommRing ↥s.topologicalClosure

If a star subalgebra of a topological star algebra is commutative, then so is its topological closure. See note [reducible non-instances].

Equations

s.commRingTopologicalClosure hs = s.commRingTopologicalClosure hs

Instances For

source

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} {φ : ↥S.topologicalClosure →⋆ₐ[R] B} {ψ : ↥S.topologicalClosure →⋆ₐ[R] B} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ.comp (StarSubalgebra.inclusion ⋯) = ψ.comp (StarSubalgebra.inclusion ⋯)) :

φ = ψ

Continuous StarAlgHoms from the topological closure of a StarSubalgebra whose compositions with the StarSubalgebra.inclusion map agree are, in fact, equal.

source

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 (↥S.topologicalClosure) B] [AlgHomClass F R (↥S.topologicalClosure) B] [StarHomClass F (↥S.topologicalClosure) B] {φ : F} {ψ : F} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : ∀ (x : ↥S), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x)) :

φ = ψ

source

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

elementalStarAlgebra R x = (StarAlgebra.adjoin R {x}).topologicalClosure

Instances For

source

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

source

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

source

instance elementalStarAlgebra.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal (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.

Equations

elementalStarAlgebra.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal R = (StarAlgebra.adjoin R {x}).commSemiringTopologicalClosure ⋯

source

instance elementalStarAlgebra.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal {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

elementalStarAlgebra.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal = (StarAlgebra.adjoin R {x}).commRingTopologicalClosure ⋯

source

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)

source

instance elementalStarAlgebra.instCompleteSpaceSubtypeMemStarSubalgebra (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) :

CompleteSpace ↥(elementalStarAlgebra R x)

Equations

⋯ = ⋯

source

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

source

theorem elementalStarAlgebra.isClosedEmbedding_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) :

IsClosedEmbedding Subtype.val

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

source

@[deprecated elementalStarAlgebra.isClosedEmbedding_coe]

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) :

IsClosedEmbedding Subtype.val

Alias of elementalStarAlgebra.isClosedEmbedding_coe.

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

source

theorem elementalStarAlgebra.induction_on (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} {y : A} (hy : y ∈ elementalStarAlgebra R x) {P : (u : A) → u ∈ elementalStarAlgebra R x → Prop} (self : P x ⋯) (star_self : P (star x) ⋯) (algebraMap : ∀ (r : R), P ((_root_.algebraMap R A) r) ⋯) (add : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u + v) ⋯) (mul : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u * v) ⋯) (closure : ∀ (s : Set A) (hs : s ⊆ ↑(elementalStarAlgebra R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ _root_.closure s), P v ⋯) :

P y hy

source

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] [StarHomClass F (↥(elementalStarAlgebra R a)) B] {φ : F} {ψ : F} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩) :

φ = ψ

Documentation

Mathlib.Topology.Algebra.StarSubalgebra

Topological star (sub)algebras #

Results #