Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/AtomicShell.lean
Pinned GitHub source · Raw UTF-8 source
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.Adapters2import MathlibAnnex.Analysis.CStarAlgebra.Representation.AtomicCommutant3import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.Concrete45/-!6# A source-parametric atomic model from projection shells78This theorem consumes only representation-local source data: pairwise9inequivalent irreducible fibers, selected unit vectors, decreasing normalized10flags, and shell partial isometries with their exact initial/final supports.11It constructs the off-diagonal rank-one completions, proves their termwise12shell relations, and proves irreducibility of the displayed concrete target.13No target capture, target simplicity, or final Naimark conclusion is a field14or hypothesis.15-/1617set_option autoImplicit false1819open Filter Topology20open scoped ENNReal lp InnerProduct2122namespace MathlibAnnex.CStarAlgebra.AtomicConstruction2324universe u v w2526variable {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)]3132open MathlibAnnex.Analysis.CStarAlgebra33open MathlibAnnex.Analysis.InnerProductSpace3435/-- Natural shell data on an arbitrary family of pairwise inequivalent36irreducible fibers produces actual inter-block unitary generators and an37irreducible concrete generated representation. -/38theorem exists_irreducible_atomicShellModel39 (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.IsIrreducible68 (ambientInclusion (atomicRepresentation pi) L) := by69 have hexists (i : I) : ∃ S : HilbertSum H →L[ℂ] HilbertSum H,70 ContinuousLinearMap.StronglyConverges71 (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))).comp80 (Submodule.projectionShell (U i) n) = W i n := by81 apply ContinuousLinearMap.exists_rankOneCompletion_of_projectionShells82 (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 o86 · simpa [norm_coordinateEmbedding] using hxi i87 · exact hUinf i88 · exact hVinf i89 choose S hS hunit hmap hterm using hexists90 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) := by94 intro i95 exact hunit i96 have hLmap : ∀ i, L i (coordinateEmbedding i (xi i)) =97 coordinateEmbedding o (xi o) := by98 intro i99 exact hmap i100 have hLterm : ∀ i n, (L i).comp101 (Submodule.projectionShell (U i) n) = W i n := by102 intro i n103 exact hterm i n104 have hrootne : coordinateEmbedding o (xi o) ≠ 0 := by105 intro hzero106 have := congrArg norm hzero107 simpa [norm_coordinateEmbedding, hxi o] using this108 letI : Nontrivial (HilbertSum H) := nontrivial_of_ne109 (coordinateEmbedding o (xi o)) 0 hrootne110 have hmodelStar : StarAlgHom.IsIrreducible111 (ambientInclusion (atomicRepresentation pi) L) := by112 apply StarAlgHom.isIrreducible_of_commutant_eq_algebraMap113 intro T hT114 apply eq_algebraMap_of_atomic_of_links pi hirr hno o xi hxi L hLmap T115 · intro a116 have h := hT (sourceHom (atomicRepresentation pi) L a)117 change Commute T118 (((sourceHom (atomicRepresentation pi) L a :119 concreteTarget (atomicRepresentation pi) L) :120 HilbertSum H →L[ℂ] HilbertSum H)) at h121 rw [sourceHom_coe] at h122 exact h123 · intro i124 have h := hT (generator (atomicRepresentation pi) L i)125 change Commute T126 (((generator (atomicRepresentation pi) L i :127 concreteTarget (atomicRepresentation pi) L) :128 HilbertSum H →L[ℂ] HilbertSum H)) at h129 rw [generator_coe] at h130 exact h131 exact ⟨L, hLunit, hLmap, hLterm,132 (Representation.isIrreducible_iff_starAlgHom133 (ambientInclusion (atomicRepresentation pi) L)).2 hmodelStar⟩134135end MathlibAnnex.CStarAlgebra.AtomicConstruction