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.instIsTopologicalSemiringSubtypeMem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] (s : StarSubalgebra R A) :

IsTopologicalSemiring ↥s

source

instance StarSubalgebra.instIsSemitopologicalSemiringSubtypeMem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsSemitopologicalSemiring A] (s : StarSubalgebra R A) :

IsSemitopologicalSemiring ↥s

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₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) :

Topology.IsEmbedding ⇑(inclusion h)

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₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) (hS₁ : IsClosed ↑S₁) :

Topology.IsClosedEmbedding ⇑(inclusion h)

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] [IsSemitopologicalSemiring 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] [IsSemitopologicalSemiring 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] [IsSemitopologicalSemiring 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] [IsSemitopologicalSemiring 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] [IsSemitopologicalSemiring 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] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} :

CompleteSpace ↥S.topologicalClosure

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] [IsSemitopologicalSemiring A] [ContinuousStar A] {s 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] [IsSemitopologicalSemiring A] [ContinuousStar A] :

Monotone 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] [IsSemitopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsSemitopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap ⇑φ) :

(map φ s).topologicalClosure ≤ 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] [IsSemitopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsSemitopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : Continuous ⇑φ) :

map φ s.topologicalClosure ≤ (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] [IsSemitopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsSemitopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap ⇑φ) (hφ' : Continuous ⇑φ) :

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

source

theorem StarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsSemitopologicalSemiring A] [ContinuousStar A] [T2Space A] (s : Set A) :

(StarAlgebra.adjoin R s).topologicalClosure ≤ centralizer R ↑(centralizer R s)

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] [IsSemitopologicalSemiring 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] [IsSemitopologicalSemiring 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 = { toSemiring := SubsemiringClass.toSemiring s.topologicalClosure, mul_comm := ⋯ }

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] [IsSemitopologicalRing 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 = { toRing := SubringClass.toRing s.topologicalClosure, mul_comm := ⋯ }

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] [IsSemitopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [T2Space B] {S : StarSubalgebra R A} {φ ψ : ↥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] [IsSemitopologicalSemiring 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} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : ∀ (x : ↥S), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x)) :

φ = ψ

source

def StarAlgebra.elemental (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :

StarSubalgebra R A

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

Equations

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

Instances For

source

@[simp]

theorem StarAlgebra.elemental.self_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :

x ∈ elemental R x

source

@[simp]

theorem StarAlgebra.elemental.star_self_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :

star x ∈ elemental R x

source

@[instance_reducible]

instance StarAlgebra.elemental.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] [T2Space A] {x : A} [IsStarNormal x] :

CommSemiring ↥(elemental R x)

The elemental star subalgebra generated by a normal element is commutative.

Equations

StarAlgebra.elemental.instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal R = { toSemiring := SubsemiringClass.toSemiring (StarAlgebra.elemental R x), mul_comm := ⋯ }

source

@[instance_reducible]

instance StarAlgebra.elemental.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] [IsSemitopologicalRing A] [ContinuousStar A] [T2Space A] {x : A} [IsStarNormal x] :

CommRing ↥(elemental R x)

The elemental generated by a normal element is commutative.

Equations

StarAlgebra.elemental.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal = { toRing := SubringClass.toRing (StarAlgebra.elemental R x), mul_comm := ⋯ }

source

theorem StarAlgebra.elemental.isClosed (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :

IsClosed ↑(elemental R x)

source

instance StarAlgebra.elemental.instCompleteSpaceSubtypeMemStarSubalgebra (R : Type u_1) [CommSemiring R] [StarRing R] {A : Type u_4} [UniformSpace A] [CompleteSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :

CompleteSpace ↥(elemental R x)

source

theorem StarAlgebra.elemental.le_of_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {S : StarSubalgebra R A} (hS : IsClosed ↑S) {x : A} (hx : x ∈ S) :

elemental R x ≤ S

source

theorem StarAlgebra.elemental.le_iff_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {x : A} {s : StarSubalgebra R A} (hs : IsClosed ↑s) :

elemental R x ≤ s ↔ x ∈ s

source

theorem StarAlgebra.elemental.isClosedEmbedding_coe (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] (x : A) :

Topology.IsClosedEmbedding Subtype.val

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

source

theorem StarAlgebra.elemental.le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] [T2Space A] (x : A) :

elemental R x ≤ StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R {x})

source

theorem StarAlgebra.elemental.induction_on (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {x y : A} (hy : y ∈ elemental R x) {P : (u : A) → u ∈ elemental R x → Prop} (self : P x ⋯) (star_self : P (star x) ⋯) (algebraMap : ∀ (r : R), P ((algebraMap R A) r) ⋯) (add : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u + v) ⋯) (mul : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u * v) ⋯) (closure : ∀ (s : Set A) (hs : s ⊆ ↑(elemental R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure s), P v ⋯) :

P y hy

source

theorem StarAlgebra.elemental.starAlgHomClass_ext (R : Type u_1) {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring 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 (↥(elemental R a)) B] [AlgHomClass F R (↥(elemental R a)) B] [StarHomClass F (↥(elemental R a)) B] {φ ψ : F} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩) :

φ = ψ

Documentation

Mathlib.Topology.Algebra.StarSubalgebra

Topological star (sub)algebras #

Results #