Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/Atomic.lean, lines 30–30.
Back to The atomic direct sum of the selected CAR representations
1import Mathlib.Analysis.CStarAlgebra.Spectrum 2import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.Basic 4import MathlibAnnex.Analysis.InnerProductSpace.HilbertSum 5 6/-! 7# Atomic representations on dependent Hilbert sums 8 9An arbitrary set-indexed family of Hilbert-space representations acts 10coordinatewise on Mathlib's dependent Hilbert sum. No separability, 11countability, finite-index, or common-fiber hypothesis is used. 12-/ 13 14set_option autoImplicit false 15 16open scoped CStarAlgebra ENNReal lp 17 18namespace MathlibAnnex.Analysis.CStarAlgebra 19 20universe u v w 21 22variable {A : Type u} [CStarAlgebra A] 23variable {I : Type v} {H : I → Type w} 24variable [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)] 25variable [∀ i, CompleteSpace (H i)] 26 27open MathlibAnnex.Analysis.InnerProductSpace 28 29/-- The bounded coordinatewise action of one algebra element. -/ 30noncomputable def atomicAction 31 (pi : ∀ i, Representation A (H i)) (a : A) : 32 HilbertSum H →L[ℂ] HilbertSum H := 33 diagonal (fun i ↦ pi i a) ‖a‖ (norm_nonneg a) 34 (fun i ↦ NonUnitalStarAlgHom.norm_apply_le (pi i) a) 35 36@[simp] 37theorem atomicAction_apply 38 (pi : ∀ i, Representation A (H i)) (a : A) 39 (x : HilbertSum H) (i : I) : 40 atomicAction pi a x i = pi i a (x i) := 41 rfl 42 43/-- The genuine arbitrary-index atomic direct-sum representation. -/ 44noncomputable def atomicRepresentation 45 (pi : ∀ i, Representation A (H i)) : 46 Representation A (HilbertSum H) where 47 toFun := atomicAction pi 48 map_one' := by 49 apply ContinuousLinearMap.ext 50 intro x 51 apply lp.ext 52 funext i 53 simp 54 map_mul' a b := by 55 apply ContinuousLinearMap.ext 56 intro x 57 apply lp.ext 58 funext i 59 simp [ContinuousLinearMap.mul_apply] 60 map_zero' := by 61 apply ContinuousLinearMap.ext 62 intro x 63 apply lp.ext 64 funext i 65 simp 66 map_add' a b := by 67 apply ContinuousLinearMap.ext 68 intro x 69 apply lp.ext 70 funext i 71 simp 72 commutes' c := by 73 apply ContinuousLinearMap.ext 74 intro x 75 apply lp.ext 76 funext i 77 change pi i (algebraMap ℂ A c) (x i) = c • x i 78 rw [← ContinuousLinearMap.algebraMap_apply (R := ℂ) (S := ℂ) 79 (M := H i)] 80 exact congrArg (fun T : H i →L[ℂ] H i ↦ T (x i)) ((pi i).commutes c) 81 map_star' a := by 82 rw [ContinuousLinearMap.star_eq_adjoint] 83 apply ContinuousLinearMap.ext 84 intro x 85 apply ext_inner_right ℂ 86 intro y 87 rw [lp.inner_eq_tsum, ContinuousLinearMap.adjoint_inner_left, 88 lp.inner_eq_tsum] 89 apply tsum_congr 90 intro i 91 simp only [atomicAction_apply] 92 rw [map_star, ContinuousLinearMap.star_eq_adjoint] 93 exact ContinuousLinearMap.adjoint_inner_left (pi i a) (y i) (x i) 94 95@[simp] 96theorem atomicRepresentation_apply 97 (pi : ∀ i, Representation A (H i)) (a : A) 98 (x : HilbertSum H) (i : I) : 99 atomicRepresentation pi a x i = pi i a (x i) := 100 rfl 101 102@[simp] 103theorem atomicRepresentation_single 104 [DecidableEq I] (pi : ∀ i, Representation A (H i)) 105 (a : A) (i : I) (x : H i) : 106 atomicRepresentation pi a (lp.single 2 i x) = 107 lp.single 2 i (pi i a x) := by 108 classical 109 apply lp.ext 110 funext j 111 simp only [atomicRepresentation_apply, lp.coeFn_single] 112 by_cases hji : j = i 113 · subst j 114 simp 115 · simp [Pi.single_apply, hji] 116 117/-- One faithful summand makes the whole atomic representation faithful. -/ 118theorem atomicRepresentation_injective_of_component 119 (pi : ∀ i, Representation A (H i)) (i : I) 120 (hi : Function.Injective (pi i)) : 121 Function.Injective (atomicRepresentation pi) := by 122 classical 123 intro a b hab 124 apply hi 125 apply ContinuousLinearMap.ext 126 intro x 127 have h := congrArg 128 (fun T : HilbertSum H →L[ℂ] HilbertSum H ↦ T (lp.single 2 i x)) hab 129 have hc := congrArg (fun y : HilbertSum H ↦ y i) h 130 simpa using hc 131 132/-- Fiberwise unitary intertwiners assemble into a unitary intertwiner of the 133arbitrary dependent atomic sums. -/ 134theorem atomicRepresentation_unitaryEquivalent 135 {K : I → Type*} 136 [∀ i, NormedAddCommGroup (K i)] [∀ i, InnerProductSpace ℂ (K i)] 137 [∀ i, CompleteSpace (K i)] 138 (pi : ∀ i, Representation A (H i)) 139 (rho : ∀ i, Representation A (K i)) 140 (U : ∀ i, H i ≃ₗᵢ[ℂ] K i) 141 (hU : ∀ i a x, U i (pi i a x) = rho i a (U i x)) : 142 (atomicRepresentation pi).UnitaryEquivalent (atomicRepresentation rho) := by 143 refine ⟨diagonalLinearIsometryEquiv U, ?_⟩ 144 intro a x 145 apply lp.ext 146 funext i 147 simpa using hU i a (x i) 148 149end MathlibAnnex.Analysis.CStarAlgebra