Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/Atomic.lean
Pinned GitHub source · Raw UTF-8 source
Back to The atomic direct sum of the selected CAR representations
1import Mathlib.Analysis.CStarAlgebra.Spectrum2import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap3import MathlibAnnex.Analysis.CStarAlgebra.Representation.Basic4import MathlibAnnex.Analysis.InnerProductSpace.HilbertSum56/-!7# Atomic representations on dependent Hilbert sums89An arbitrary set-indexed family of Hilbert-space representations acts10coordinatewise on Mathlib's dependent Hilbert sum. No separability,11countability, finite-index, or common-fiber hypothesis is used.12-/1314set_option autoImplicit false1516open scoped CStarAlgebra ENNReal lp1718namespace MathlibAnnex.Analysis.CStarAlgebra1920universe u v w2122variable {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)]2627open MathlibAnnex.Analysis.InnerProductSpace2829/-- The bounded coordinatewise action of one algebra element. -/30noncomputable def atomicAction31 (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)3536@[simp]37theorem atomicAction_apply38 (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 rfl4243/-- The genuine arbitrary-index atomic direct-sum representation. -/44noncomputable def atomicRepresentation45 (pi : ∀ i, Representation A (H i)) :46 Representation A (HilbertSum H) where47 toFun := atomicAction pi48 map_one' := by49 apply ContinuousLinearMap.ext50 intro x51 apply lp.ext52 funext i53 simp54 map_mul' a b := by55 apply ContinuousLinearMap.ext56 intro x57 apply lp.ext58 funext i59 simp [ContinuousLinearMap.mul_apply]60 map_zero' := by61 apply ContinuousLinearMap.ext62 intro x63 apply lp.ext64 funext i65 simp66 map_add' a b := by67 apply ContinuousLinearMap.ext68 intro x69 apply lp.ext70 funext i71 simp72 commutes' c := by73 apply ContinuousLinearMap.ext74 intro x75 apply lp.ext76 funext i77 change pi i (algebraMap ℂ A c) (x i) = c • x i78 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 := by82 rw [ContinuousLinearMap.star_eq_adjoint]83 apply ContinuousLinearMap.ext84 intro x85 apply ext_inner_right ℂ86 intro y87 rw [lp.inner_eq_tsum, ContinuousLinearMap.adjoint_inner_left,88 lp.inner_eq_tsum]89 apply tsum_congr90 intro i91 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)9495@[simp]96theorem atomicRepresentation_apply97 (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 rfl101102@[simp]103theorem atomicRepresentation_single104 [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) := by108 classical109 apply lp.ext110 funext j111 simp only [atomicRepresentation_apply, lp.coeFn_single]112 by_cases hji : j = i113 · subst j114 simp115 · simp [Pi.single_apply, hji]116117/-- One faithful summand makes the whole atomic representation faithful. -/118theorem atomicRepresentation_injective_of_component119 (pi : ∀ i, Representation A (H i)) (i : I)120 (hi : Function.Injective (pi i)) :121 Function.Injective (atomicRepresentation pi) := by122 classical123 intro a b hab124 apply hi125 apply ContinuousLinearMap.ext126 intro x127 have h := congrArg128 (fun T : HilbertSum H →L[ℂ] HilbertSum H ↦ T (lp.single 2 i x)) hab129 have hc := congrArg (fun y : HilbertSum H ↦ y i) h130 simpa using hc131132/-- Fiberwise unitary intertwiners assemble into a unitary intertwiner of the133arbitrary dependent atomic sums. -/134theorem atomicRepresentation_unitaryEquivalent135 {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) := by143 refine ⟨diagonalLinearIsometryEquiv U, ?_⟩144 intro a x145 apply lp.ext146 funext i147 simpa using hU i a (x i)148149end MathlibAnnex.Analysis.CStarAlgebra