Skip to content

Commit 7e1b73e

Browse files
gw90gw90
committed
feat(Analysis/CStarAlgebra): GNS construction (leanprover-community#33116)
We construct a Hilbert space and a StarAlgHom between a possibly non-unital CStarAlgebra and the algebra of bounded operators on that Hilbert space. Co-authored-by: Gregory Wickham <gwickham99@gmail.com>
1 parent bd33e8d commit 7e1b73e

6 files changed

Lines changed: 263 additions & 3 deletions

File tree

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1528,6 +1528,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
15281528
public import Mathlib.Analysis.CStarAlgebra.ContinuousMap
15291529
public import Mathlib.Analysis.CStarAlgebra.Exponential
15301530
public import Mathlib.Analysis.CStarAlgebra.GelfandDuality
1531+
public import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
15311532
public import Mathlib.Analysis.CStarAlgebra.Hom
15321533
public import Mathlib.Analysis.CStarAlgebra.Matrix
15331534
public import Mathlib.Analysis.CStarAlgebra.Module.Constructions
@@ -6876,6 +6877,7 @@ public import Mathlib.Topology.Algebra.IsUniformGroup.Constructions
68766877
public import Mathlib.Topology.Algebra.IsUniformGroup.Defs
68776878
public import Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
68786879
public import Mathlib.Topology.Algebra.IsUniformGroup.Order
6880+
public import Mathlib.Topology.Algebra.LinearMapCompletion
68796881
public import Mathlib.Topology.Algebra.LinearTopology
68806882
public import Mathlib.Topology.Algebra.Localization
68816883
public import Mathlib.Topology.Algebra.MetricSpace.Lipschitz

‎Mathlib/Analysis/CStarAlgebra/GelfandNaimarkSegal.lean‎

Lines changed: 198 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,198 @@
1+
/-
2+
Copyright (c) 2025 Gregory Wickham. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Gregory Wickham
5+
-/
6+
module
7+
8+
public import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
9+
public import Mathlib.Analysis.InnerProductSpace.Adjoint
10+
public import Mathlib.Analysis.InnerProductSpace.Completion
11+
public import Mathlib.Topology.Algebra.LinearMapCompletion
12+
13+
/-!
14+
# The GNS (Gelfand-Naimark-Segal) construction
15+
16+
This file contains the constructions and definitions that produce a ⋆-homomorphism from an arbitrary
17+
C⋆-algebra into the algebra of bounded linear operators on an appropriately constructed Hilbert
18+
space.
19+
20+
## Main results
21+
22+
- `f.PreGNS` : a type synonym of `A` that bundles in a fixed positive linear functional `f` so that
23+
we can construct an inner product and inner product-induced norm.
24+
- `f.GNS` : the Hilbert space completion of `f.preGNS`.
25+
- `f.gnsNonUnitalStarAlgHom` : The non-unital ⋆-homomorphism from a non-unital `A` into the bounded
26+
linear operators on `f.GNS`.
27+
- `f.gnsStarAlgHom` : The unital ⋆-homomorphism from a unital `A` into the bounded linear operators
28+
on `f.GNS`.
29+
30+
## TODO
31+
32+
- Explicitly construct a unit norm cyclic vector ζ such that
33+
a ↦ ⟨(f.gns(NonUnital)StarAlgHom a) \* ζ, ,ζ⟩ is a state on `A` for both unital and non-unital
34+
cases.
35+
36+
-/
37+
38+
@[expose] public section
39+
open scoped ComplexOrder InnerProductSpace
40+
open Complex ContinuousLinearMap UniformSpace Completion
41+
42+
variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ)
43+
44+
namespace PositiveLinearMap
45+
46+
set_option linter.unusedVariables false in
47+
/-- The Gelfand─Naimark─Segal (GNS) space constructed from a positive linear functional on a
48+
non-unital C⋆-algebra. This is a type synonym of `A`.
49+
50+
This space is only a pre-inner product space. Its Hilbert space completion is
51+
`PositiveLinearMap.GNS`. -/
52+
@[nolint unusedArguments]
53+
def PreGNS (f : A →ₚ[ℂ] ℂ) := A
54+
55+
instance : AddCommGroup f.PreGNS := inferInstanceAs (AddCommGroup A)
56+
instance : Module ℂ f.PreGNS := inferInstanceAs (Module ℂ A)
57+
58+
/-- The map from the C⋆-algebra to the GNS space, as a linear equivalence. -/
59+
def toPreGNS : A ≃ₗ[ℂ] f.PreGNS := LinearEquiv.refl ℂ _
60+
61+
/-- The map from the GNS space to the C⋆-algebra, as a linear equivalence. -/
62+
def ofPreGNS : f.PreGNS ≃ₗ[ℂ] A := f.toPreGNS.symm
63+
64+
@[simp]
65+
lemma toPreGNS_ofPreGNS (a : f.PreGNS) : f.toPreGNS (f.ofPreGNS a) = a := rfl
66+
67+
@[simp]
68+
lemma ofPreGNS_toPreGNS (a : A) : f.ofPreGNS (f.toPreGNS a) = a := rfl
69+
70+
variable [StarOrderedRing A]
71+
72+
/--
73+
The (semi-)inner product space whose elements are the elements of `A`, but which has an
74+
inner product-induced norm that is different from the norm on `A` and which is induced by `f`.
75+
-/
76+
abbrev preGNSpreInnerProdSpace : PreInnerProductSpace.Core ℂ f.PreGNS where
77+
inner a b := f (star (f.ofPreGNS a) * f.ofPreGNS b)
78+
conj_inner_symm := by simp [← Complex.star_def, ← map_star f]
79+
re_inner_nonneg _ := RCLike.nonneg_iff.mp (f.map_nonneg (star_mul_self_nonneg _)) |>.1
80+
add_left _ _ _ := by rw [map_add, star_add, add_mul, map_add]
81+
smul_left := by simp [smul_mul_assoc]
82+
83+
noncomputable instance : SeminormedAddCommGroup f.PreGNS :=
84+
InnerProductSpace.Core.toSeminormedAddCommGroup (c := f.preGNSpreInnerProdSpace)
85+
noncomputable instance : InnerProductSpace ℂ f.PreGNS :=
86+
InnerProductSpace.ofCore f.preGNSpreInnerProdSpace
87+
88+
lemma preGNS_inner_def (a b : f.PreGNS) :
89+
⟪a, b⟫_ℂ = f (star (f.ofPreGNS a) * f.ofPreGNS b) := rfl
90+
91+
lemma preGNS_norm_def (a : f.PreGNS) :
92+
‖a‖ = √(f (star (f.ofPreGNS a) * f.ofPreGNS a)).re := rfl
93+
94+
lemma preGNS_norm_sq (a : f.PreGNS) :
95+
‖a‖ ^ 2 = f (star (f.ofPreGNS a) * f.ofPreGNS a) := by
96+
have : 0 ≤ f (star (f.ofPreGNS a) * f.ofPreGNS a) := map_nonneg f <| star_mul_self_nonneg _
97+
rw [preGNS_norm_def, ← ofReal_pow, Real.sq_sqrt]
98+
· rw [conj_eq_iff_re.mp this.star_eq]
99+
· rwa [re_nonneg_iff_nonneg this.isSelfAdjoint]
100+
101+
/--
102+
The Hilbert space constructed from a positive linear functional on a C⋆-algebra.
103+
-/
104+
abbrev GNS := UniformSpace.Completion f.PreGNS
105+
106+
/--
107+
The continuous linear map from a C⋆-algebra `A` to the `PositiveLinearMap.preGNS` space induced by
108+
a positive linear functional `f : A →ₚ[ℂ] ℂ`. This map is given by left-multiplication by `a`:
109+
`x ↦ f.toPreGNS (a * f.ofPreGNS x)`.
110+
111+
This is the map that is lifted to the completion of `f.PreGNS` (i.e. `f.GNS`) in order to define
112+
`gnsNonUnitalStarAlgHom`.
113+
-/
114+
@[simps!]
115+
noncomputable def leftMulMapPreGNS (a : A) : f.PreGNS →L[ℂ] f.PreGNS :=
116+
f.toPreGNS.toLinearMap ∘ₗ mul ℂ A a ∘ₗ f.ofPreGNS.toLinearMap |>.mkContinuous ‖a‖ fun x ↦ by
117+
rw [← sq_le_sq₀ (by positivity) (by positivity), mul_pow, ← RCLike.ofReal_le_ofReal (K := ℂ),
118+
RCLike.ofReal_pow, RCLike.ofReal_eq_complex_ofReal, preGNS_norm_sq]
119+
have : star (f.ofPreGNS x) * star a * (a * f.ofPreGNS x) ≤
120+
‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x := by
121+
rw [← mul_assoc, mul_assoc _ (star a), sq, ← CStarRing.norm_star_mul_self (x := a),
122+
smul_mul_assoc]
123+
exact CStarAlgebra.star_left_conjugate_le_norm_smul
124+
calc
125+
_ ≤ f (‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x) := by
126+
simpa using OrderHomClass.mono f this
127+
_ = _ := by simp [← Complex.coe_smul, preGNS_norm_sq, smul_mul_assoc]
128+
129+
@[simp]
130+
lemma leftMulMapPreGNS_mul_eq_comp (a b : A) :
131+
f.leftMulMapPreGNS (a * b) = f.leftMulMapPreGNS a ∘L f.leftMulMapPreGNS b := by
132+
ext c; simp [mul_assoc]
133+
134+
/--
135+
The non-unital ⋆-homomorphism/⋆-representation of `A` into the algebra of bounded operators on
136+
a Hilbert space that is constructed from a positive linear functional `f` on a possibly non-unital
137+
C⋆-algebra.
138+
-/
139+
noncomputable def gnsNonUnitalStarAlgHom : A →⋆ₙₐ[ℂ] (f.GNS →L[ℂ] f.GNS) where
140+
toFun a := (f.leftMulMapPreGNS a).completion
141+
map_smul' r a := by
142+
ext x
143+
induction x using Completion.induction_on with
144+
| hp => apply isClosed_eq <;> fun_prop
145+
| ih x => simp [smul_mul_assoc]
146+
map_zero' := by
147+
ext b
148+
induction b using Completion.induction_on with
149+
| hp => apply isClosed_eq <;> fun_prop
150+
| ih b => simp [Completion.coe_zero]
151+
map_add' x y := by
152+
ext c
153+
induction c using Completion.induction_on with
154+
| hp => apply isClosed_eq <;> fun_prop
155+
| ih c => simp [add_mul, Completion.coe_add]
156+
map_mul' a b := by
157+
ext c
158+
induction c using Completion.induction_on with
159+
| hp => apply isClosed_eq <;> fun_prop
160+
| ih c => simp
161+
map_star' a := by
162+
refine (eq_adjoint_iff (f.leftMulMapPreGNS (star a)).completion
163+
(f.leftMulMapPreGNS a).completion).mpr ?_
164+
intro x y
165+
induction x, y using Completion.induction_on₂ with
166+
| hp => apply isClosed_eq <;> fun_prop
167+
| ih x y => simp [mul_assoc, preGNS_inner_def]
168+
169+
lemma gnsNonUnitalStarAlgHom_apply {a : A} :
170+
f.gnsNonUnitalStarAlgHom a = (f.leftMulMapPreGNS a).completion := rfl
171+
172+
@[simp]
173+
lemma gnsNonUnitalStarAlgHom_apply_coe {a : A} {b : f.PreGNS} :
174+
f.gnsNonUnitalStarAlgHom a b = f.leftMulMapPreGNS a b := by
175+
simp [gnsNonUnitalStarAlgHom_apply]
176+
177+
variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →ₚ[ℂ] ℂ)
178+
179+
@[simp]
180+
private lemma gnsNonUnitalStarAlgHom_map_one : f.gnsNonUnitalStarAlgHom 1 = 1 := by
181+
ext b
182+
induction b using Completion.induction_on with
183+
| hp => apply isClosed_eq <;> fun_prop
184+
| ih b => simp [gnsNonUnitalStarAlgHom]
185+
186+
/--
187+
The unital ⋆-homomorphism/⋆-representation of `A` into the algebra of bounded operators on a Hilbert
188+
space that is constructed from a positive linear functional `f` on a unital C⋆-algebra.
189+
190+
This is the unital version of `gnsNonUnitalStarAlgHom`.
191+
-/
192+
@[simps]
193+
noncomputable def gnsStarAlgHom : A →⋆ₐ[ℂ] (f.GNS →L[ℂ] f.GNS) where
194+
__ := f.gnsNonUnitalStarAlgHom
195+
map_one' := by simp
196+
commutes' r := by simp [Algebra.algebraMap_eq_smul_one]
197+
198+
end PositiveLinearMap

‎Mathlib/Topology/Algebra/GroupCompletion.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,6 @@ Authors: Patrick Massot, Johannes Hölzl
66
module
77

88
public import Mathlib.Topology.Algebra.UniformMulAction
9-
public import Mathlib.Topology.UniformSpace.Completion
10-
public import Mathlib.Topology.Algebra.Group.Pointwise
119

1210
/-!
1311
# Completion of topological groups:
@@ -260,6 +258,7 @@ theorem AddMonoidHom.continuous_completion (f : α →+ β) (hf : Continuous f)
260258
Continuous (AddMonoidHom.completion f hf : Completion α → Completion β) :=
261259
continuous_map
262260

261+
@[simp]
263262
theorem AddMonoidHom.completion_coe (f : α →+ β) (hf : Continuous f) (a : α) :
264263
AddMonoidHom.completion f hf a = f a :=
265264
map_coe (uniformContinuous_addMonoidHom_of_continuous hf) a

‎Mathlib/Topology/Algebra/LinearMapCompletion.lean‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
/-
2+
Copyright (c) 2025 Gregory Wickham. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Gregory Wickham
5+
-/
6+
module
7+
8+
public import Mathlib.Topology.Algebra.GroupCompletion
9+
public import Mathlib.Topology.Algebra.Module.LinearMap
10+
11+
/-!
12+
# Completion of continuous (semi-)linear maps:
13+
14+
This file has a declaration that enables a continuous (semi-)linear map between modules to be
15+
lifted to a continuous semilinear map between the completions of those modules.
16+
17+
## Main declarations:
18+
19+
* `ContinuousLinearMap.completion`: promotes a continuous semilinear map
20+
from `G` to `H` to a continuous semilinear map from `Completion G` to `Completion H`.
21+
-/
22+
23+
@[expose] public section
24+
25+
namespace ContinuousLinearMap
26+
27+
open UniformSpace UniformSpace.Completion
28+
29+
variable {α β : Type*} {R₁ R₂ : Type*} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α]
30+
[Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β]
31+
[AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β]
32+
{σ : R₁ →+* R₂}
33+
34+
/--
35+
Lift a continuous semilinear map to a continuous semilinear map between the
36+
`UniformSpace.Completion`s of the spaces. This is `UniformSpace.Completion.map` bundled as a
37+
continuous linear map when the input is itself a continuous linear map.
38+
-/
39+
noncomputable def completion (f : α →SL[σ] β) : Completion α →SL[σ] Completion β where
40+
__ := f.toAddMonoidHom.completion f.continuous
41+
map_smul' r x := by
42+
induction x using Completion.induction_on with
43+
| hp =>
44+
exact isClosed_eq (continuous_map.comp <| continuous_const_smul r)
45+
(continuous_map.const_smul _)
46+
| ih x => simp [← Completion.coe_smul]
47+
cont := continuous_map
48+
49+
@[simp]
50+
lemma toAddMonoidHom_completion (f : α →SL[σ] β) :
51+
f.completion.toAddMonoidHom = f.toAddMonoidHom.completion f.continuous := rfl
52+
53+
lemma coe_completion (f : α →SL[σ] β) :
54+
f.completion = Completion.map f := rfl
55+
56+
@[simp]
57+
theorem completion_apply_coe (f : α →SL[σ] β) (a : α) :
58+
f.completion a = f a := by simp [coe_completion, map_coe]
59+
60+
end ContinuousLinearMap

‎Mathlib/Topology/Algebra/Module/LinearMap.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ theorem coe_mk' (f : M₁ →ₛₗ[σ₁₂] M₂) (h) : (mk f h : M₁ → M
117117
protected theorem continuous (f : M₁ →SL[σ₁₂] M₂) : Continuous f :=
118118
f.2
119119

120+
@[simp]
120121
protected theorem uniformContinuous {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂]
121122
[AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁]
122123
[IsUniformAddGroup E₂] (f : E₁ →SL[σ₁₂] E₂) : UniformContinuous f :=

‎Mathlib/Topology/UniformSpace/Completion.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -481,7 +481,7 @@ protected def map (f : α → β) : Completion α → Completion β :=
481481
theorem uniformContinuous_map : UniformContinuous (Completion.map f) :=
482482
cPkg.uniformContinuous_map cPkg f
483483

484-
@[continuity]
484+
@[continuity, fun_prop]
485485
theorem continuous_map : Continuous (Completion.map f) :=
486486
cPkg.continuous_map cPkg f
487487

0 commit comments

Comments
 (0)