elementalStarAlgebra.isUnit_of_isUnit_of_isStarNormal
theorem elementalStarAlgebra.isUnit_of_isUnit_of_isStarNormal :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : CstarRing A]
[inst_4 : StarModule ℂ A] [inst_5 : CompleteSpace A] {a : A} [inst_6 : IsStarNormal a],
IsUnit a → IsUnit ⟨a, ⋯⟩
This theorem, which is one of the key steps towards establishing spectral permanence for C*-algebras, states that for any element `a` of a normed ring `A` that is a normed algebra over the complex numbers and has additional structures of a star ring, a C*-ring, a star module over the complex numbers, and is a complete space, if `a` is also a star-normal element and is a unit (meaning it has a two-sided inverse), then the pair comprising `a` and an unspecified element (represented by `⋯`) is also a unit. This theorem is succeeded by `StarSubalgebra.coe_isUnit`, which doesn't require `a` to be star-normal and holds true for any closed star subalgebra.
More concisely: If `a` is a star-normal, unit element in a complete, normed C*-ring `A` over the complex numbers, then `(a, ⋯)` is a unit in `A`.
|
StarSubalgebra.spectrum_eq
theorem StarSubalgebra.spectrum_eq :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : CstarRing A]
[inst_4 : StarModule ℂ A] [inst_5 : CompleteSpace A] {S : StarSubalgebra ℂ A},
IsClosed ↑S → ∀ (x : ↥S), spectrum ℂ x = spectrum ℂ ↑x
This theorem is known as **Spectral permanence**, which states that the spectrum of an element is invariant of the (closed) `StarSubalgebra` in which it is contained. Specifically, given a normed ring `A` with a normed algebra over the complex numbers, a `StarRing`, a `CstarRing`, a `StarModule`, and a complete space structure, if we have a closed `StarSubalgebra` `S` of `A`, then for any element `x` in `S`, the spectrum of `x` in the complex numbers is the same whether we consider `x` as an element of `S` or as an element of `A`.
More concisely: The spectrum of an element in a closed `StarSubalgebra` of a normed ring remains unchanged.
|
spectrum_star_mul_self_of_isStarNormal
theorem spectrum_star_mul_self_of_isStarNormal :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : CstarRing A]
[inst_4 : StarModule ℂ A] [inst_5 : CompleteSpace A] (a : A) [inst_6 : IsStarNormal a],
spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
This lemma states that for any element `a` in a complete normed algebra `A` over the complex numbers with additional structures of a star ring, a C*-ring, and a star module, given that `a` is star-normal, the spectrum of the product `star a * a` is a subset of the closed interval from 0 to the norm of `star a * a`. This lemma is used in the proof of a theorem about the permanence of the spectrum in star subalgebras, which is part of the theory of the continuous functional calculus. In the context of the continuous functional calculus, this lemma could potentially be replaced by a similar statement that does not require `a` to be star-normal.
More concisely: If `a` is a star-normal element in a complete normed star C*-algebra over the complex numbers, then the spectrum of `star a * a` is contained in the closed interval [0, ||star a * a||].
|
StarSubalgebra.coe_isUnit
theorem StarSubalgebra.coe_isUnit :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : CstarRing A]
[inst_4 : StarModule ℂ A] [inst_5 : CompleteSpace A] {S : StarSubalgebra ℂ A},
IsClosed ↑S → ∀ {x : ↥S}, IsUnit ↑x ↔ IsUnit x
This theorem states that for a unital C*-subalgebra `S` of a type `A` (where `A` forms a normed ring, a normed algebra over the complex numbers, a star ring, a C*-ring, a star module over the complex numbers, and a complete space), if an element `x` of `S` (considered as an element of `A` by applying the coercion function `↑`) is a unit in `A` (i.e., it has a two-sided inverse in `A`), then `x` is also a unit in `S`. This theorem is true if `S` is a closed set. Conversely, if `x` is a unit in `S`, then `x` is a unit in `A` when considered as an element of `A`.
In other words, an element of the subalgebra is invertible in the subalgebra if and only if it is invertible in the larger algebra, assuming that the subspace is closed.
More concisely: A unital C*-subalgebra `S` of a normed ring `A` contains the invertible elements of `A` as invertible elements if and only if `S` is closed.
|
StarSubalgebra.isUnit_coe_inv_mem
theorem StarSubalgebra.isUnit_coe_inv_mem :
∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : CstarRing A]
[inst_4 : StarModule ℂ A] [inst_5 : CompleteSpace A] {S : StarSubalgebra ℂ A},
IsClosed ↑S → ∀ {x : A} (h : IsUnit x), x ∈ S → ↑h.unit⁻¹ ∈ S
This theorem states that for a given element 'x' of type 'A' and is invertible in the algebra 'A', its inverse resides within any unital C*-subalgebra 'S' that also contains 'x'. This is under the conditions that 'A' has the structure of a normed ring, a normed algebra over the complex numbers, a star ring, a C*-ring, and a star module over the complex numbers, and is a complete space. Further, the subalgebra 'S' is required to be closed.
More concisely: If 'x' is an invertible element in the unital C*-subalgebra 'S' of the complete, normed, complex C*-ring and star module 'A', then 'x'' exists in 'S'.
|