Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceUnique.lean
Pinned GitHub source · Raw UTF-8 source
Back to Normalization and the trace identity determine the CAR trace · Back to The fixed shell target has a unique tracial state · Back to Constructing the normalized trace on the completed CAR algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Trace2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteAverage34/-!5# Uniqueness of the normalized CAR trace67The matrix-unit calculations are separated from the density argument.8Positivity is not an additional hypothesis: normalization and the trace9identity already determine any continuous linear functional on CAR.10-/1112set_option autoImplicit false1314namespace MathlibAnnex.CStarAlgebra.CAR1516private theorem apply_limitMatrixUnit_diag_eq_of_mul_comm17 (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) := by20 simpa only [limitMatrixUnit_mul, ↓reduceIte] using21 hf (limitMatrixUnit n i 0) (limitMatrixUnit n 0 i)2223private theorem apply_limitMatrixUnit_eq_zero_of_ne_of_mul_comm24 (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 := by27 simpa only [limitMatrixUnit_mul, ↓reduceIte, hij, Ne.symm hij, if_false, map_zero] using28 hf (limitMatrixUnit n i i) (limitMatrixUnit n i j)2930private theorem apply_limitMatrixUnit_zero_zero_of_apply_one_of_mul_comm31 (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 : ℂ)⁻¹ := by34 have hmul : (2 ^ n : ℂ) * f (limitMatrixUnit n 0 0) = 1 := by35 calc36 (2 ^ n : ℂ) * f (limitMatrixUnit n 0 0) =37 ∑ _i : Fin (2 ^ n), f (limitMatrixUnit n 0 0) := by simp38 _ = ∑ i : Fin (2 ^ n), f (limitMatrixUnit n i i) := by39 apply Finset.sum_congr rfl40 intro i _41 exact (apply_limitMatrixUnit_diag_eq_of_mul_comm f hf n i).symm42 _ = 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 calc46 f (limitMatrixUnit n 0 0) =47 ((2 ^ n : ℂ)⁻¹ * (2 ^ n : ℂ)) * f (limitMatrixUnit n 0 0) := by48 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]5253/-- A normalized continuous trace agrees with the constructed trace on54all matrix units, including off-diagonal ones. -/55theorem apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm56 (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) := by60 by_cases hij : i = j61 · subst j62 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]6869/-- Agreement on matrix units extends linearly to each complete finite stage. -/70theorem apply_ofStage_eq_trace_of_apply_one_of_mul_comm71 (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) := by74 rw [ofStage_eq_sum_smul_limitMatrixUnit]75 simp only [map_sum, map_smul]76 apply Finset.sum_congr rfl77 intro i _78 apply Finset.sum_congr rfl79 intro j _80 rw [apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm f hf1 hf n i j]8182/-- The normalized trace is unique among continuous linear functionals83satisfying the trace identity. -/84theorem eq_trace_of_apply_one_of_mul_comm85 (f : Limit →L[ℂ] ℂ) (hf1 : f 1 = 1)86 (hf : ∀ a b, f (a * b) = f (b * a)) : f = trace := by87 apply ContinuousLinearMap.coeFn_injective88 apply f.continuous.ext_on dense_stageRange trace.continuous89 intro x hx90 obtain ⟨n, a, rfl⟩ := Set.mem_iUnion.mp hx91 exact apply_ofStage_eq_trace_of_apply_one_of_mul_comm f hf1 hf n a9293end MathlibAnnex.CStarAlgebra.CAR