Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CompletedSource.lean
Pinned GitHub source · Raw UTF-8 source
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 irreducible target representation has a surviving fixed space · Back to Assembling selected GNS cyclic subspaces into an isometric source representation · 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 Reconstructing a represented unitary from its shells and residual corner · Back to The atomic common range is one embedded GNS line · Back to The matching GNS fiber retains exactly its cyclic line · Back to An inequivalent GNS fiber has no residual common range · Back to Unitary equivalence without an initial unitality assumption
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Simplicity2import MathlibAnnex.Analysis.CStarAlgebra.CAR.ShellMatching3import MathlibAnnex.Analysis.CStarAlgebra.Representation.PureStateRepresentatives45/-!6# Source data on the completed CAR algebra78The root product state and its common decreasing projection flag are constructed on9the actual completion. KOS remains an explicit theorem argument.10-/1112set_option autoImplicit false1314namespace MathlibAnnex.CStarAlgebra.CAR1516/-- The completed root state bundled with its directly proved purity. -/17noncomputable def completedRootPureState : MathlibAnnex.CStarAlgebra.PureState Limit :=18 ⟨rootState, isPureState_rootState⟩1920@[simp]21theorem representative_completedRootPureState :22 MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState completedRootPureState.classOf =23 completedRootPureState :=24 MathlibAnnex.CStarAlgebra.PureState.representative_root _2526/-- For a selected pure-state GNS class, one KOS automorphism transports its state27to the root state and supports every member of the common root flag. -/28theorem exists_representative_rootFlag_shell_family_of_kishimotoOzawaSakai29 (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 := by38 exact MathlibAnnex.CStarAlgebra.exists_shell_family_of_kishimotoOzawaSakai hKOS Limit isSimpleCStarAlgebra_limit39 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).140 completedRootPureState.141 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).242 completedRootPureState.2 rootFlag isStarProjection_rootFlag4344/-- A compiled two-shell use of the family theorem; both links use the same KOS45automorphism, not separately selected automorphisms. -/46theorem exists_two_representative_rootFlag_links_of_kishimotoOzawaSakai47 (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) := by55 obtain ⟨alpha, hstate, w, hw⟩ :=56 exists_representative_rootFlag_shell_family_of_kishimotoOzawaSakai hKOS j57 exact ⟨alpha, hstate, w 0, w 1, hw 0, hw 1⟩5859end MathlibAnnex.CStarAlgebra.CAR