Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceUnique.lean, lines 82–91.
Back to The fixed shell target has a unique tracial state · Back to Constructing the normalized trace on the completed CAR algebra · Back to Normalization and the trace identity determine the CAR trace
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Trace 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteAverage 3 4/-! 5# Uniqueness of the normalized CAR trace 6 7The matrix-unit calculations are separated from the density argument. 8Positivity is not an additional hypothesis: normalization and the trace 9identity already determine any continuous linear functional on CAR. 10-/ 11 12set_option autoImplicit false 13 14namespace MathlibAnnex.CStarAlgebra.CAR 15 16private theorem apply_limitMatrixUnit_diag_eq_of_mul_comm 17 (f : Limit →L[ℂ] ℂ) (hf : ∀ a b, f (a * b) = f (b * a)) 18 (n : ℕ) (i : Fin (2 ^ n)) : 19 f (limitMatrixUnit n i i) = f (limitMatrixUnit n 0 0) := by 20 simpa only [limitMatrixUnit_mul, ↓reduceIte] using 21 hf (limitMatrixUnit n i 0) (limitMatrixUnit n 0 i) 22 23private theorem apply_limitMatrixUnit_eq_zero_of_ne_of_mul_comm 24 (f : Limit →L[ℂ] ℂ) (hf : ∀ a b, f (a * b) = f (b * a)) 25 (n : ℕ) (i j : Fin (2 ^ n)) (hij : i ≠ j) : 26 f (limitMatrixUnit n i j) = 0 := by 27 simpa only [limitMatrixUnit_mul, ↓reduceIte, hij, Ne.symm hij, if_false, map_zero] using 28 hf (limitMatrixUnit n i i) (limitMatrixUnit n i j) 29 30private theorem apply_limitMatrixUnit_zero_zero_of_apply_one_of_mul_comm 31 (f : Limit →L[ℂ] ℂ) (hf1 : f 1 = 1) 32 (hf : ∀ a b, f (a * b) = f (b * a)) (n : ℕ) : 33 f (limitMatrixUnit n 0 0) = (2 ^ n : ℂ)⁻¹ := by 34 have hmul : (2 ^ n : ℂ) * f (limitMatrixUnit n 0 0) = 1 := by 35 calc 36 (2 ^ n : ℂ) * f (limitMatrixUnit n 0 0) = 37 ∑ _i : Fin (2 ^ n), f (limitMatrixUnit n 0 0) := by simp 38 _ = ∑ i : Fin (2 ^ n), f (limitMatrixUnit n i i) := by 39 apply Finset.sum_congr rfl 40 intro i _ 41 exact (apply_limitMatrixUnit_diag_eq_of_mul_comm f hf n i).symm 42 _ = f (∑ i : Fin (2 ^ n), limitMatrixUnit n i i) := by rw [map_sum] 43 _ = 1 := by rw [sum_limitMatrixUnit_diag, hf1] 44 have hn : (2 ^ n : ℂ) ≠ 0 := pow_ne_zero _ (by norm_num) 45 calc 46 f (limitMatrixUnit n 0 0) = 47 ((2 ^ n : ℂ)⁻¹ * (2 ^ n : ℂ)) * f (limitMatrixUnit n 0 0) := by 48 rw [inv_mul_cancel₀ hn, one_mul] 49 _ = (2 ^ n : ℂ)⁻¹ * ((2 ^ n : ℂ) * f (limitMatrixUnit n 0 0)) := 50 mul_assoc _ _ _ 51 _ = (2 ^ n : ℂ)⁻¹ := by rw [hmul, mul_one] 52 53/-- A normalized continuous trace agrees with the constructed trace on 54all matrix units, including off-diagonal ones. -/ 55theorem apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm 56 (f : Limit →L[ℂ] ℂ) (hf1 : f 1 = 1) 57 (hf : ∀ a b, f (a * b) = f (b * a)) 58 (n : ℕ) (i j : Fin (2 ^ n)) : 59 f (limitMatrixUnit n i j) = trace (limitMatrixUnit n i j) := by 60 by_cases hij : i = j 61 · subst j 62 rw [apply_limitMatrixUnit_diag_eq_of_mul_comm f hf n i, 63 apply_limitMatrixUnit_diag_eq_of_mul_comm trace trace_mul_comm n i, 64 apply_limitMatrixUnit_zero_zero_of_apply_one_of_mul_comm f hf1 hf n, 65 apply_limitMatrixUnit_zero_zero_of_apply_one_of_mul_comm trace trace_one trace_mul_comm n] 66 · rw [apply_limitMatrixUnit_eq_zero_of_ne_of_mul_comm f hf n i j hij, 67 apply_limitMatrixUnit_eq_zero_of_ne_of_mul_comm trace trace_mul_comm n i j hij] 68 69/-- Agreement on matrix units extends linearly to each complete finite stage. -/ 70theorem apply_ofStage_eq_trace_of_apply_one_of_mul_comm 71 (f : Limit →L[ℂ] ℂ) (hf1 : f 1 = 1) 72 (hf : ∀ a b, f (a * b) = f (b * a)) (n : ℕ) (a : Stage n) : 73 f (ofStage n a) = trace (ofStage n a) := by 74 rw [ofStage_eq_sum_smul_limitMatrixUnit] 75 simp only [map_sum, map_smul] 76 apply Finset.sum_congr rfl 77 intro i _ 78 apply Finset.sum_congr rfl 79 intro j _ 80 rw [apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm f hf1 hf n i j] 81 82/-- The normalized trace is unique among continuous linear functionals 83satisfying the trace identity. -/ 84theorem eq_trace_of_apply_one_of_mul_comm 85 (f : Limit →L[ℂ] ℂ) (hf1 : f 1 = 1) 86 (hf : ∀ a b, f (a * b) = f (b * a)) : f = trace := by 87 apply ContinuousLinearMap.coeFn_injective 88 apply f.continuous.ext_on dense_stageRange trace.continuous 89 intro x hx 90 obtain ⟨n, a, rfl⟩ := Set.mem_iUnion.mp hx 91 exact apply_ofStage_eq_trace_of_apply_one_of_mul_comm f hf1 hf n a 92 93end MathlibAnnex.CStarAlgebra.CAR