Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CompletedSource.lean, lines 16–18.
Back to The atomic common range is one embedded GNS line · Back to The matching GNS fiber retains exactly its cyclic line · Back to Every irreducible representation is unitarily equivalent to the inclusion · Back to Realizing a shell family by a faithful irreducible operator algebra · Back to An inequivalent GNS fiber has no residual common range · Back to An irreducible target representation has a surviving fixed space · Back to Reconstructing a represented unitary from its shells and residual corner · Back to Unitary equivalence without an initial unitality assumption · Back to The cyclic sum fills every irreducible target representation · Back to A common root vector realizes every selected state through the generators · Back to Assembling selected GNS cyclic subspaces into an isometric source representation
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Simplicity 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.ShellMatching 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.PureStateRepresentatives 4 5/-! 6# Source data on the completed CAR algebra 7 8The root product state and its common decreasing projection flag are constructed on 9the actual completion. KOS remains an explicit theorem argument. 10-/ 11 12set_option autoImplicit false 13 14namespace MathlibAnnex.CStarAlgebra.CAR 15 16/-- The completed root state bundled with its directly proved purity. -/ 17noncomputable def completedRootPureState : MathlibAnnex.CStarAlgebra.PureState Limit := 18 ⟨rootState, isPureState_rootState⟩ 19 20@[simp] 21theorem representative_completedRootPureState : 22 MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState completedRootPureState.classOf = 23 completedRootPureState := 24 MathlibAnnex.CStarAlgebra.PureState.representative_root _ 25 26/-- For a selected pure-state GNS class, one KOS automorphism transports its state 27to the root state and supports every member of the common root flag. -/ 28theorem exists_representative_rootFlag_shell_family_of_kishimotoOzawaSakai 29 (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) 30 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 31 ∃ alpha : Limit ≃⋆ₐ[ℂ] Limit, 32 (∀ a : Limit, 33 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 (alpha a) = 34 completedRootPureState.1 a) ∧ 35 ∃ w : ℕ → Limit, ∀ n, 36 star (w n) * w n = alpha (rootFlag n) ∧ 37 w n * star (w n) = rootFlag n := by 38 exact MathlibAnnex.CStarAlgebra.exists_shell_family_of_kishimotoOzawaSakai hKOS Limit isSimpleCStarAlgebra_limit 39 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 40 completedRootPureState.1 41 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).2 42 completedRootPureState.2 rootFlag isStarProjection_rootFlag 43 44/-- A compiled two-shell use of the family theorem; both links use the same KOS 45automorphism, not separately selected automorphisms. -/ 46theorem exists_two_representative_rootFlag_links_of_kishimotoOzawaSakai 47 (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 48 ∃ alpha : Limit ≃⋆ₐ[ℂ] Limit, 49 (∀ a : Limit, 50 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 (alpha a) = 51 completedRootPureState.1 a) ∧ 52 ∃ w₀ w₁ : Limit, 53 (star w₀ * w₀ = alpha (rootFlag 0) ∧ w₀ * star w₀ = rootFlag 0) ∧ 54 (star w₁ * w₁ = alpha (rootFlag 1) ∧ w₁ * star w₁ = rootFlag 1) := by 55 obtain ⟨alpha, hstate, w, hw⟩ := 56 exists_representative_rootFlag_shell_family_of_kishimotoOzawaSakai hKOS j 57 exact ⟨alpha, hstate, w 0, w 1, hw 0, hw 1⟩ 58 59end MathlibAnnex.CStarAlgebra.CAR