Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/AtomicShell.lean, lines 35–133.
Back to An irreducible operator algebra constructed from projection shells · Back to The atomic-shell construction on selected pure-GNS fibers
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.AtomicCommutant 3import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.Concrete 4 5/-! 6# A source-parametric atomic model from projection shells 7 8This theorem consumes only representation-local source data: pairwise 9inequivalent irreducible fibers, selected unit vectors, decreasing normalized 10flags, and shell partial isometries with their exact initial/final supports. 11It constructs the off-diagonal rank-one completions, proves their termwise 12shell relations, and proves irreducibility of the displayed concrete target. 13No target capture, target simplicity, or final Naimark conclusion is a field 14or hypothesis. 15-/ 16 17set_option autoImplicit false 18 19open Filter Topology 20open scoped ENNReal lp InnerProduct 21 22namespace MathlibAnnex.CStarAlgebra.AtomicConstruction 23 24universe u v w 25 26variable {A : Type u} [CStarAlgebra A] 27variable {I : Type v} {H : I → Type w} 28variable [DecidableEq I] 29variable [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)] 30variable [∀ i, CompleteSpace (H i)] [∀ i, Nontrivial (H i)] 31 32open MathlibAnnex.Analysis.CStarAlgebra 33open MathlibAnnex.Analysis.InnerProductSpace 34 35/-- Natural shell data on an arbitrary family of pairwise inequivalent 36irreducible fibers produces actual inter-block unitary generators and an 37irreducible concrete generated representation. -/ 38theorem exists_irreducible_atomicShellModel 39 (pi : ∀ i, Representation A (H i)) 40 (hirr : ∀ i, StarAlgHom.IsIrreducible (pi i)) 41 (hno : ∀ ⦃i j : I⦄, i ≠ j → ∀ e : H i ≃ₗᵢ[ℂ] H j, 42 ¬ StarAlgHom.Intertwines (pi i) (pi j) (e : H i →L[ℂ] H j)) 43 (o : I) (xi : ∀ i, H i) (hxi : ∀ i, ‖xi i‖ = 1) 44 (W : I → ℕ → HilbertSum H →L[ℂ] HilbertSum H) 45 (U V : I → ℕ → Submodule ℂ (HilbertSum H)) 46 [∀ i n, (U i n).HasOrthogonalProjection] 47 [∀ i n, (V i n).HasOrthogonalProjection] 48 [∀ i, (⨅ n, U i n).HasOrthogonalProjection] 49 [∀ i, (⨅ n, V i n).HasOrthogonalProjection] 50 (hU : ∀ i, Antitone (U i)) (hV : ∀ i, Antitone (V i)) 51 (hU0 : ∀ i, U i 0 = ⊤) (hV0 : ∀ i, V i 0 = ⊤) 52 (hInitial : ∀ i n, ((W i n)†).comp (W i n) = 53 Submodule.projectionShell (U i) n) 54 (hFinal : ∀ i n, (W i n).comp ((W i n)†) = 55 Submodule.projectionShell (V i) n) 56 (hUinf : ∀ i, (⨅ n, U i n).starProjection = 57 InnerProductSpace.rankOne ℂ (coordinateEmbedding i (xi i)) 58 (coordinateEmbedding i (xi i))) 59 (hVinf : ∀ i, (⨅ n, V i n).starProjection = 60 InnerProductSpace.rankOne ℂ (coordinateEmbedding o (xi o)) 61 (coordinateEmbedding o (xi o))) : 62 ∃ L : I → HilbertSum H →L[ℂ] HilbertSum H, 63 (∀ i, L i ∈ unitary (HilbertSum H →L[ℂ] HilbertSum H)) ∧ 64 (∀ i, L i (coordinateEmbedding i (xi i)) = 65 coordinateEmbedding o (xi o)) ∧ 66 (∀ i n, (L i).comp (Submodule.projectionShell (U i) n) = W i n) ∧ 67 Representation.IsIrreducible 68 (ambientInclusion (atomicRepresentation pi) L) := by 69 have hexists (i : I) : ∃ S : HilbertSum H →L[ℂ] HilbertSum H, 70 ContinuousLinearMap.StronglyConverges 71 (ContinuousLinearMap.partialSum (W i)) atTop S ∧ 72 (S + InnerProductSpace.rankOne ℂ 73 (coordinateEmbedding o (xi o)) (coordinateEmbedding i (xi i))) ∈ 74 unitary (HilbertSum H →L[ℂ] HilbertSum H) ∧ 75 (S + InnerProductSpace.rankOne ℂ 76 (coordinateEmbedding o (xi o)) (coordinateEmbedding i (xi i))) 77 (coordinateEmbedding i (xi i)) = coordinateEmbedding o (xi o) ∧ 78 ∀ n, (S + InnerProductSpace.rankOne ℂ 79 (coordinateEmbedding o (xi o)) (coordinateEmbedding i (xi i))).comp 80 (Submodule.projectionShell (U i) n) = W i n := by 81 apply ContinuousLinearMap.exists_rankOneCompletion_of_projectionShells 82 (W i) (U i) (V i) (hU i) (hV i) (hU0 i) (hV0 i) 83 (hInitial i) (hFinal i) 84 (coordinateEmbedding o (xi o)) (coordinateEmbedding i (xi i)) 85 · simpa [norm_coordinateEmbedding] using hxi o 86 · simpa [norm_coordinateEmbedding] using hxi i 87 · exact hUinf i 88 · exact hVinf i 89 choose S hS hunit hmap hterm using hexists 90 let L : I → HilbertSum H →L[ℂ] HilbertSum H := fun i ↦ 91 S i + InnerProductSpace.rankOne ℂ 92 (coordinateEmbedding o (xi o)) (coordinateEmbedding i (xi i)) 93 have hLunit : ∀ i, L i ∈ unitary (HilbertSum H →L[ℂ] HilbertSum H) := by 94 intro i 95 exact hunit i 96 have hLmap : ∀ i, L i (coordinateEmbedding i (xi i)) = 97 coordinateEmbedding o (xi o) := by 98 intro i 99 exact hmap i 100 have hLterm : ∀ i n, (L i).comp 101 (Submodule.projectionShell (U i) n) = W i n := by 102 intro i n 103 exact hterm i n 104 have hrootne : coordinateEmbedding o (xi o) ≠ 0 := by 105 intro hzero 106 have := congrArg norm hzero 107 simpa [norm_coordinateEmbedding, hxi o] using this 108 letI : Nontrivial (HilbertSum H) := nontrivial_of_ne 109 (coordinateEmbedding o (xi o)) 0 hrootne 110 have hmodelStar : StarAlgHom.IsIrreducible 111 (ambientInclusion (atomicRepresentation pi) L) := by 112 apply StarAlgHom.isIrreducible_of_commutant_eq_algebraMap 113 intro T hT 114 apply eq_algebraMap_of_atomic_of_links pi hirr hno o xi hxi L hLmap T 115 · intro a 116 have h := hT (sourceHom (atomicRepresentation pi) L a) 117 change Commute T 118 (((sourceHom (atomicRepresentation pi) L a : 119 concreteTarget (atomicRepresentation pi) L) : 120 HilbertSum H →L[ℂ] HilbertSum H)) at h 121 rw [sourceHom_coe] at h 122 exact h 123 · intro i 124 have h := hT (generator (atomicRepresentation pi) L i) 125 change Commute T 126 (((generator (atomicRepresentation pi) L i : 127 concreteTarget (atomicRepresentation pi) L) : 128 HilbertSum H →L[ℂ] HilbertSum H)) at h 129 rw [generator_coe] at h 130 exact h 131 exact ⟨L, hLunit, hLmap, hLterm, 132 (Representation.isIrreducible_iff_starAlgHom 133 (ambientInclusion (atomicRepresentation pi) L)).2 hmodelStar⟩ 134 135end MathlibAnnex.CStarAlgebra.AtomicConstruction