Topological star (sub)algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 has_continuous_smul 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.
@[protected, instance]
def
star_subalgebra.has_continuous_smul
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_space R]
[has_continuous_smul R A]
(s : star_subalgebra R A) :
@[protected, instance]
def
star_subalgebra.topological_semiring
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
(s : star_subalgebra R A) :
theorem
star_subalgebra.embedding_inclusion
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
{S₁ S₂ : star_subalgebra R A}
(h : S₁ ≤ S₂) :
The star_subalgebra.inclusion of a star subalgebra is an embedding.
theorem
star_subalgebra.closed_embedding_inclusion
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
{S₁ S₂ : star_subalgebra R A}
(h : S₁ ≤ S₂)
(hS₁ : is_closed ↑S₁) :
The star_subalgebra.inclusion of a closed star subalgebra is a closed_embedding.
def
star_subalgebra.topological_closure
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A]
(s : star_subalgebra R A) :
star_subalgebra R A
The closure of a star subalgebra in a topological star algebra as a star subalgebra.
Equations
Instances for ↥star_subalgebra.topological_closure
@[simp]
theorem
star_subalgebra.topological_closure_coe
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A]
(s : star_subalgebra R A) :
↑(s.topological_closure) = closure ↑s
theorem
star_subalgebra.le_topological_closure
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A]
(s : star_subalgebra R A) :
s ≤ s.topological_closure
theorem
star_subalgebra.is_closed_topological_closure
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A]
(s : star_subalgebra R A) :
@[protected, instance]
def
star_subalgebra.topological_closure.complete_space
{R : Type u_1}
[comm_semiring R]
[star_ring R]
{A : Type u_2}
[uniform_space A]
[complete_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
{S : star_subalgebra R A} :
theorem
star_subalgebra.topological_closure_minimal
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A]
{s t : star_subalgebra R A}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
theorem
star_subalgebra.topological_closure_mono
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A] :
@[reducible]
def
star_subalgebra.comm_semiring_topological_closure
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A]
[t2_space A]
(s : star_subalgebra R A)
(hs : ∀ (x y : ↥s), x * y = y * x) :
If a star subalgebra of a topological star algebra is commutative, then so is its topological closure. See note [reducible non-instances].
Equations
@[reducible]
def
star_subalgebra.comm_ring_topological_closure
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[star_ring R]
[topological_space A]
[ring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_ring A]
[has_continuous_star A]
[t2_space A]
(s : star_subalgebra R A)
(hs : ∀ (x y : ↥s), x * y = y * x) :
If a star subalgebra of a topological star algebra is commutative, then so is its topological closure. See note [reducible non-instances].
Equations
theorem
star_alg_hom.ext_topological_closure
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A]
[topological_space B]
[semiring B]
[algebra R B]
[star_ring B]
[t2_space B]
{S : star_subalgebra R A}
{φ ψ : ↥(S.topological_closure) →⋆ₐ[R] B}
(hφ : continuous ⇑φ)
(hψ : continuous ⇑ψ)
(h : φ.comp (star_subalgebra.inclusion _) = ψ.comp (star_subalgebra.inclusion _)) :
φ = ψ
Continuous star_alg_homs from the the topological closure of a star_subalgebra whose
compositions with the star_subalgebra.inclusion map agree are, in fact, equal.
theorem
star_alg_hom_class.ext_topological_closure
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_semiring A]
[has_continuous_star A]
[topological_space B]
[semiring B]
[algebra R B]
[star_ring B]
[t2_space B]
{F : Type u_4}
{S : star_subalgebra R A}
[star_alg_hom_class F R ↥(S.topological_closure) B]
{φ ψ : F}
(hφ : continuous ⇑φ)
(hψ : continuous ⇑ψ)
(h : ∀ (x : ↥S), ⇑φ (⇑(star_subalgebra.inclusion _) x) = ⇑ψ (⇑(star_subalgebra.inclusion _) x)) :
φ = ψ
def
elemental_star_algebra
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
(x : A) :
star_subalgebra R A
The topological closure of the subalgebra generated by a single element.
Equations
Instances for ↥elemental_star_algebra
theorem
elemental_star_algebra.self_mem
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
(x : A) :
x ∈ elemental_star_algebra R x
theorem
elemental_star_algebra.star_self_mem
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
(x : A) :
@[protected, instance]
def
elemental_star_algebra.comm_semiring
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
[t2_space A]
{x : A}
[is_star_normal x] :
The elemental_star_algebra generated by a normal element is commutative.
Equations
@[protected, instance]
def
elemental_star_algebra.comm_ring
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[star_ring R]
[topological_space A]
[ring A]
[algebra R A]
[star_ring A]
[star_module R A]
[topological_ring A]
[has_continuous_star A]
[t2_space A]
{x : A}
[is_star_normal x] :
The elemental_star_algebra generated by a normal element is commutative.
Equations
- elemental_star_algebra.comm_ring = (star_subalgebra.adjoin R {x}).comm_ring_topological_closure elemental_star_algebra.comm_ring._proof_2
@[protected]
theorem
elemental_star_algebra.is_closed
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
(x : A) :
@[protected, instance]
def
elemental_star_algebra.complete_space
(R : Type u_1)
[comm_semiring R]
[star_ring R]
{A : Type u_2}
[uniform_space A]
[complete_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
(x : A) :
theorem
elemental_star_algebra.le_of_is_closed_of_mem
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
{S : star_subalgebra R A}
(hS : is_closed ↑S)
{x : A}
(hx : x ∈ S) :
elemental_star_algebra R x ≤ S
theorem
elemental_star_algebra.closed_embedding_coe
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
(x : A) :
The coercion from an elemental algebra to the full algebra as a closed_embedding.
theorem
elemental_star_algebra.star_alg_hom_class_ext
(R : Type u_1)
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[star_ring R]
[topological_space A]
[semiring A]
[star_ring A]
[topological_semiring A]
[has_continuous_star A]
[algebra R A]
[star_module R A]
[topological_space B]
[semiring B]
[star_ring B]
[algebra R B]
[t2_space B]
{F : Type u_4}
{a : A}
[star_alg_hom_class F R ↥(elemental_star_algebra R a) B]
{φ ψ : F}
(hφ : continuous ⇑φ)
(hψ : continuous ⇑ψ)
(h : ⇑φ ⟨a, _⟩ = ⇑ψ ⟨a, _⟩) :
φ = ψ