MathlibAnnex.CStarAlgebra.CAR.stageTrace_embed

Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Trace.lean, lines 19–28.
Back to Constructing the normalized trace on the completed CAR algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Completion
2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteTrace
3import MathlibAnnex.Analysis.CStarAlgebra.State.Basic
4
5/-!
6# The normalized trace on the completed CAR algebra
7
8The compatible finite traces are first defined on the actual algebraic
9inductive limit, transported to the metric union, and continuously extended
10to its completion. Positivity, traciality and normalization are all proved.
11-/
12
13set_option autoImplicit false
14
15open scoped ComplexOrder
16
17namespace MathlibAnnex.CStarAlgebra.CAR
18
19@[simp]
20theorem stageTrace_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (a : Stage n),
21    stageTrace m (embed n m h a) = stageTrace n a := by
22  apply Nat.le_induction
23  · intro a
24    rw [embed_refl]
25    rfl
26  · intro m h ih a
27    rw [embed_succ, StarAlgHom.comp_apply, stageTrace_step, ih]
28    exact h
29
30/-- The trace on the algebraic inductive limit. -/
31noncomputable def algTraceLinear : AlgCAR →ₗ[ℂ] ℂ :=
32  DirectLimit.Module.lift ℂ ℕ Stage (fun _ _ h ↦ embed _ _ h)
33    (fun n ↦ (stageTrace n).toLinearMap)
34    (fun i j hij a ↦ stageTrace_embed i j hij a)
35
36@[simp]
37theorem algTraceLinear_algStageHom (n : ℕ) (a : Stage n) :
38    algTraceLinear (algStageHom n a) = stageTrace n a := rfl
39
40/-- The trace on the normed, not yet completed, union. -/
41noncomputable def preTraceLinear : PreCAR →ₗ[ℂ] ℂ :=
42  algTraceLinear.comp preStarAlgEquiv.toAlgEquiv.toLinearEquiv.toLinearMap
43
44@[simp]
45theorem preTraceLinear_stageHom (n : ℕ) (a : Stage n) :
46    preTraceLinear (stageHom n a) = stageTrace n a := rfl
47
48theorem norm_preTraceLinear_le (x : PreCAR) : ‖preTraceLinear x‖ ≤ ‖x‖ := by
49  obtain ⟨n, a, _, ha, _⟩ := exists_common_stage x x
50  rw [← ha, preTraceLinear_stageHom, norm_stageHom]
51  exact norm_stageTrace_le n a
52
53/-- The continuous trace on the metric union. -/
54noncomputable def preTrace : PreCAR →L[ℂ] ℂ :=
55  preTraceLinear.mkContinuous 1 fun x ↦ by
56    simpa only [one_mul] using norm_preTraceLinear_le x
57
58@[simp]
59theorem preTrace_stageHom (n : ℕ) (a : Stage n) :
60    preTrace (stageHom n a) = stageTrace n a := rfl
61
62/-- The normalized trace of the completed CAR algebra. -/
63noncomputable def trace : Limit →L[ℂ] ℂ :=
64  preTrace.extend (UniformSpace.Completion.toComplL : PreCAR →L[ℂ] Limit)
65
66@[simp]
67theorem trace_coe (x : PreCAR) : trace (x : Limit) = preTrace x :=
68  ContinuousLinearMap.extend_eq preTrace UniformSpace.Completion.denseRange_coe
69    (UniformSpace.Completion.isUniformInducing_coe PreCAR) x
70
71@[simp]
72theorem trace_ofStage (n : ℕ) (a : Stage n) : trace (ofStage n a) = stageTrace n a := by
73  rw [ofStage_apply, trace_coe, preTrace_stageHom]
74
75theorem norm_trace_le (x : Limit) : ‖trace x‖ ≤ ‖x‖ := by
76  refine UniformSpace.Completion.induction_on (α := PreCAR)
77    (p := fun x ↦ ‖trace x‖ ≤ ‖x‖) x ?_ ?_
78  · exact isClosed_le trace.continuous.norm continuous_norm
79  · intro a
80    rw [trace_coe, UniformSpace.Completion.norm_coe]
81    change ‖preTraceLinear a‖ ≤ ‖a‖
82    exact norm_preTraceLinear_le a
83
84@[simp]
85theorem trace_one : trace 1 = 1 := by
86  calc
87    trace 1 = trace (ofStage 0 (1 : Stage 0)) :=
88      congrArg trace ((ofStage 0).map_one).symm
89    _ = stageTrace 0 1 := trace_ofStage 0 1
90    _ = 1 := stageTrace_one 0
91
92private theorem preTrace_star_mul_self_nonneg (x : PreCAR) :
93    0 ≤ preTrace (star x * x) := by
94  obtain ⟨n, a, _, ha, _⟩ := exists_common_stage x x
95  rw [← ha, ← map_star, ← map_mul, preTrace_stageHom]
96  exact stageTrace_star_mul_self_nonneg n a
97
98theorem trace_star_mul_self_nonneg (x : Limit) : 0 ≤ trace (star x * x) := by
99  refine UniformSpace.Completion.induction_on (α := PreCAR)
100    (p := fun x ↦ 0 ≤ trace (star x * x)) x ?_ ?_
101  · exact isClosed_le continuous_const
102      (trace.continuous.comp (continuous_limit_star.mul continuous_id))
103  · intro a
104    simpa only [← UniformSpace.Completion.coe_mul, star_coe, trace_coe] using
105      preTrace_star_mul_self_nonneg a
106
107theorem trace_nonneg (x : Limit) (hx : 0 ≤ x) : 0 ≤ trace x := by
108  obtain ⟨y, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx
109  exact trace_star_mul_self_nonneg y
110
111theorem trace_mem_stateSpace :
112    trace ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace Limit :=
113  ⟨trace_nonneg, trace_one⟩
114
115private theorem preTrace_mul_comm (x y : PreCAR) : preTrace (x * y) = preTrace (y * x) := by
116  obtain ⟨n, a, b, ha, hb⟩ := exists_common_stage x y
117  rw [← ha, ← hb, ← map_mul, ← map_mul, preTrace_stageHom, preTrace_stageHom]
118  exact stageTrace_mul_comm n a b
119
120theorem trace_mul_comm (x y : Limit) : trace (x * y) = trace (y * x) := by
121  refine UniformSpace.Completion.induction_on₂ (α := PreCAR) (β := PreCAR)
122    (p := fun x y ↦ trace (x * y) = trace (y * x)) x y ?_ ?_
123  · apply isClosed_eq <;> fun_prop
124  · intro a b
125    simpa only [← UniformSpace.Completion.coe_mul, trace_coe] using preTrace_mul_comm a b
126
127@[simp]
128theorem trace_rootFlag (n : ℕ) : trace (rootFlag n) = (2 ^ n : ℂ)⁻¹ := by
129  rw [rootFlag, trace_ofStage, stageTrace_rootProjection]
130
131/-- The same trace as a positive linear map, for GNS calculations. -/
132noncomputable def tracePositive : Limit →ₚ[ℂ] ℂ :=
133  PositiveLinearMap.mk₀ trace.toLinearMap trace_nonneg
134
135@[simp]
136theorem tracePositive_apply (x : Limit) : tracePositive x = trace x := rfl
137
138@[simp]
139theorem tracePositive_one : tracePositive 1 = 1 := trace_one
140
141end MathlibAnnex.CStarAlgebra.CAR