spectrum.gelfandTransform_eq
theorem spectrum.gelfandTransform_eq :
β {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra β A] [inst_2 : CompleteSpace A] (a : A),
spectrum β ((WeakDual.gelfandTransform β A) a) = spectrum β a
The theorem states that the Gelfand transform is spectrum-preserving, i.e., for any normed commutative ring `A`, which is also a normed algebra over the complex numbers `β` and a complete space, for any element `a` of `A`, the spectrum of the element `a` under the Gelfand transform is the same as the spectrum of `a` itself. This means that the Gelfand transform does not change the set of complex numbers `β` for which `r * 1 - a` is not a unit in the algebra `A`.
More concisely: The Gelfand transform preserves spectra of elements in a completeness commutative normed `β`-algebra `A`, that is, the spectrum of an element `a` under the Gelfand transform equals the spectrum of `a` in `A`.
|
WeakDual.CharacterSpace.homeoEval_naturality
theorem WeakDual.CharacterSpace.homeoEval_naturality :
β {X : Type u_1} {Y : Type u_2} {π : Type u_3} [inst : RCLike π] [inst_1 : TopologicalSpace X]
[inst_2 : CompactSpace X] [inst_3 : T2Space X] [inst_4 : TopologicalSpace Y] [inst_5 : CompactSpace Y]
[inst_6 : T2Space Y] (f : C(X, Y)),
(WeakDual.CharacterSpace.homeoEval Y π).toContinuousMap.comp f =
(WeakDual.CharacterSpace.compContinuousMap (ContinuousMap.compStarAlgHom' π π f)).comp
(WeakDual.CharacterSpace.homeoEval X π).toContinuousMap
This theorem, `WeakDual.CharacterSpace.homeoEval_naturality`, describes the natural isomorphism in the context of duality between the category of compact Hausdorff spaces and the category of commutative unital C*-algebras. Specifically, we consider two contravariant functors: `F : Cpct β CommCStarAlg` that assigns to each compact Hausdorff space `X` the C*-algebra of continuous complex-valued functions on `X`, and `G : CommCStarAlg β Cpct` that assigns to each commutative unital C*-algebra `A` the space of its characters. The actions of these functors on morphisms are given by `WeakDual.CharacterSpace.compContinuousMap` and `ContinuousMap.compStarAlgHom'`, respectively.
The natural isomorphism is given by the function `Ξ· : id β G β F := WeakDual.CharacterSpace.homeoEval`, which is a homeomorphism between a compact Hausdorff space `X` and the character space of the C*-algebra of continuous functions on `X`.
The theorem states the naturality of `Ξ·`, i.e., for any compact Hausdorff spaces `X` and `Y`, and any continuous function `f : C(X, Y)`, the following diagram commutes:
```
X -- Ξ· X --> characterSpace β C(X, β)
| |
f (G β F) f
| |
v v
Y -- Ξ· Y --> characterSpace β C(Y, β)
```
In other words, applying `Ξ·` after `f` is the same as first applying `(G β F) f` and then applying `Ξ·`.
More concisely: The natural transformation from the identity functor to the composition of the functors assigning the character space to a commutative unital C*-algebra and the C*-algebra of continuous functions to a compact Hausdorff space is a natural homeomorphism.
|
gelfandTransform_bijective
theorem gelfandTransform_bijective :
β (A : Type u_1) [inst : NormedCommRing A] [inst_1 : NormedAlgebra β A] [inst_2 : CompleteSpace A]
[inst_3 : StarRing A] [inst_4 : CstarRing A] [inst_5 : StarModule β A],
Function.Bijective β(WeakDual.gelfandTransform β A)
The theorem `gelfandTransform_bijective` states that for any type `A` that fulfills the conditions of being a normed commutative ring, a normed algebra over the complex numbers (`β`), a complete space, a star ring, a Cβ-ring, and a star module over the complex numbers, the Gelfand transform (represented here by `WeakDual.gelfandTransform β A`) is a bijective function. In other words, the Gelfand transform maps distinct elements of `A` to distinct elements in its codomain (injectivity) and every element in its codomain is an image of some element in `A` (surjectivity) when `A` is a Cβ-algebra over the complex numbers.
More concisely: The Gelfand transform of a complete, normed Cβ-algebra over the complex numbers is a bijective function.
|
WeakDual.CharacterSpace.compContinuousMap_id
theorem WeakDual.CharacterSpace.compContinuousMap_id :
β (A : Type u_1) {π : Type u_4} [inst : NontriviallyNormedField π] [inst_1 : NormedRing A]
[inst_2 : NormedAlgebra π A] [inst_3 : CompleteSpace A] [inst_4 : StarRing A],
WeakDual.CharacterSpace.compContinuousMap (StarAlgHom.id π A) = ContinuousMap.id β(WeakDual.characterSpace π A)
The theorem `WeakDual.CharacterSpace.compContinuousMap_id` states that for any type `A`, and given a nontrivially normed field `π`, a normed ring `A`, a normed algebra structure on `A` over `π`, a complete space structure on `A`, and a `StarRing` structure on `A`, the function `WeakDual.CharacterSpace.compContinuousMap` applied to the `StarAlgHom.id` (the identity function as a star algebra homomorphism) is equal to `ContinuousMap.id` (the identity function as a continuous map) on the weak dual character space of `π` and `A`. In other words, in this context, the identity function maintains its identity property when transformed by the `compContinuousMap` method of the weak dual character space.
More concisely: The identity function as a star algebra homomorphism is equal to the identity function as a continuous map when applied to the weak dual character space of a normed algebra over a nontrivially normed field.
|
WeakDual.CharacterSpace.exists_apply_eq_zero
theorem WeakDual.CharacterSpace.exists_apply_eq_zero :
β {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra β A] [inst_2 : CompleteSpace A] {a : A},
Β¬IsUnit a β β f, f a = 0
This theorem states that for any normed commutative ring `A` which is also a normed algebra over the complex numbers `β` and is a complete space, if an element `a` from `A` is not a unit (i.e., it does not have a two-sided inverse), then there exists a character `f` (a continuous group homomorphism from `A` to the complex numbers `β`) such that `f(a)` equals zero. This is equivalent to saying that the Gelfand transform of `a` attains the value zero for some character.
More concisely: For any completable, commutative normed `β`-algebra `A`, a non-unit `a` in `A` has a character `f` in its Gelfand spectrum such that `f(a) = 0`.
|
gelfandTransform_isometry
theorem gelfandTransform_isometry :
β (A : Type u_1) [inst : NormedCommRing A] [inst_1 : NormedAlgebra β A] [inst_2 : CompleteSpace A]
[inst_3 : StarRing A] [inst_4 : CstarRing A] [inst_5 : StarModule β A],
Isometry β(WeakDual.gelfandTransform β A)
The theorem `gelfandTransform_isometry` states that for any type `A` that is a normed commutative ring, a normed algebra over the complex numbers `β`, a complete space, a star ring, a C*-ring, and a star module over `β`, the Gelfand transform (which is a function that maps elements of this type `A` to their Gelfand representations) is an isometry. In other words, the Gelfand transform preserves the edistance, i.e., for any two elements `x1` and `x2` in `A`, the edistance between the images of `x1` and `x2` under the Gelfand transform is the same as the edistance between `x1` and `x2` themselves.
More concisely: For any normed commutative ring `A` that is a normed algebra over the complex numbers, complete, star ring, C*-ring, and star module over `β`, the Gelfand transform is an isometry, preserving the Euclidean distance between elements.
|
WeakDual.CharacterSpace.compContinuousMap_comp
theorem WeakDual.CharacterSpace.compContinuousMap_comp :
β {A : Type u_1} {B : Type u_2} {C : Type u_3} {π : Type u_4} [inst : NontriviallyNormedField π]
[inst_1 : NormedRing A] [inst_2 : NormedAlgebra π A] [inst_3 : CompleteSpace A] [inst_4 : StarRing A]
[inst_5 : NormedRing B] [inst_6 : NormedAlgebra π B] [inst_7 : CompleteSpace B] [inst_8 : StarRing B]
[inst_9 : NormedRing C] [inst_10 : NormedAlgebra π C] [inst_11 : CompleteSpace C] [inst_12 : StarRing C]
(Οβ : B βββ[π] C) (Οβ : A βββ[π] B),
WeakDual.CharacterSpace.compContinuousMap (Οβ.comp Οβ) =
(WeakDual.CharacterSpace.compContinuousMap Οβ).comp (WeakDual.CharacterSpace.compContinuousMap Οβ)
The theorem `WeakDual.CharacterSpace.compContinuousMap_comp` states that the composition of continuous maps in the space of characters (linear forms from a normed algebra to the base field) is functorial over normed π-algebras. More specifically, for any three types `A`, `B`, and `C` which are complete normed π-algebras with a conjugate-linear star operation, and any two continuous π-algebra homomorphisms `Οβ` from `A` to `B` and `Οβ` from `B` to `C`, the composition of `Οβ` and `Οβ` as mapped by the function `WeakDual.CharacterSpace.compContinuousMap` is equal to the composition of the results of separately mapping `Οβ` and `Οβ` by the same function.
More concisely: For any complete normed algebras A, B, and C with a conjugate-linear star operation, and continuous algebra homomorphisms Οβ from A to B and Οβ from B to C, the map WeakDual.CharacterSpace.compContinuousMap composes them consistently: (WeakDual.CharacterSpace.compContinuousMap Οβ β Οβ) = WeakDual.CharacterSpace.compContinuousMap Οβ β Οβ.
|