Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint
MathlibAnnex/Analysis/CStarAlgebra/CAR/AtomicCounterexample.lean · lines 95–98
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.GlobalTransport 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicEndpoint 3 4/-! 5# Ordinary Naimark endpoint from the proved CAR homogeneity theorem 6 7The shell family and concrete target in this file are chosen once. The 8generic `MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty` is not changed or assumed: the closed CAR theorem 9supplies exactly the representative-to-root automorphisms needed by the 10family-parametric atomic construction. 11-/ 12 13set_option autoImplicit false 14 15noncomputable section 16 17namespace MathlibAnnex.CStarAlgebra.CAR 18 19open MathlibAnnex.Analysis.CStarAlgebra 20 21universe v 22 23/-- Canonical identity shell data at the distinguished root class. -/ 24private noncomputable def rootRepresentativeShellData : 25 RepresentativeShellData completedRootPureState.classOf where 26 alpha := StarAlgEquiv.refl ℂ Limit 27 state_eq := rootShell_identity_family.1 28 link := rootShell 29 initial_support := fun n ↦ (rootShell_identity_family.2 n).1 30 final_support := fun n ↦ (rootShell_identity_family.2 n).2 31 32/-- For one selected pure-state class, closed CAR homogeneity supplies a 33single automorphism. Generic approximate-inner shell matching then supplies 34all exact shell links for that same automorphism. The root branch is fixed 35canonically instead of invoking homogeneity. -/ 36noncomputable def representativeShellDataOfHomogeneity 37 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : RepresentativeShellData j := by 38 classical 39 by_cases hj : j = completedRootPureState.classOf 40 · subst j 41 exact rootRepresentativeShellData 42 · let hex := homogeneity 43 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 44 completedRootPureState.1 45 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).2 46 completedRootPureState.2 47 let alpha := Classical.choose hex 48 have halpha := Classical.choose_spec hex 49 let hwex := MathlibAnnex.CStarAlgebra.exists_shell_family_of_approximately_inner 50 Limit alpha halpha.2 rootShell isStarProjection_rootShell 51 let w := Classical.choose hwex 52 have hw := Classical.choose_spec hwex 53 exact 54 { alpha := alpha 55 state_eq := halpha.1 56 link := w 57 initial_support := fun n ↦ (hw n).1 58 final_support := fun n ↦ (hw n).2 } 59 60@[simp] 61theorem representativeShellDataOfHomogeneity_root_alpha : 62 (representativeShellDataOfHomogeneity 63 completedRootPureState.classOf).alpha = StarAlgEquiv.refl ℂ Limit := by 64 simp [representativeShellDataOfHomogeneity, rootRepresentativeShellData] 65 66@[simp] 67theorem representativeShellDataOfHomogeneity_root_link (n : ℕ) : 68 (representativeShellDataOfHomogeneity 69 completedRootPureState.classOf).link n = rootShell n := by 70 simp [representativeShellDataOfHomogeneity, rootRepresentativeShellData] 71 72/-- The one representative shell family used by the ordinary CAR endpoint. -/ 73noncomputable def homogeneityShellFamily : RepresentativeShellFamily where 74 data := representativeShellDataOfHomogeneity 75 root_alpha := representativeShellDataOfHomogeneity_root_alpha 76 root_link := representativeShellDataOfHomogeneity_root_link 77 78/-- The single concrete C-star algebra used by every field of `AtomicCounterexampleEndpoint`. -/ 79abbrev AtomicCounterexampleAlgebra := ShellFamilyTarget homogeneityShellFamily 80 81/-- The actual completed CAR source map into the fixed main target. -/ 82noncomputable def atomicCounterexampleSourceHom : Limit →⋆ₐ[ℂ] AtomicCounterexampleAlgebra := 83 shellFamilySourceHom homogeneityShellFamily 84 85/-- The fixed faithful irreducible displayed representation of `AtomicCounterexampleAlgebra`. -/ 86noncomputable def atomicCounterexampleRepresentation : 87 Representation AtomicCounterexampleAlgebra 88 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 89 shellFamilyInclusion homogeneityShellFamily 90 91/-- Fully expanded ordinary endpoint for the single target chosen above. -/ 92abbrev AtomicCounterexampleEndpoint : Prop := 93 ShellFamilyEndpoint.{v} homogeneityShellFamily 94 95/-- Closed ordinary Naimark main for the actual CAR construction. It has no 96generic KOS, shell-data, rank-one, capture, simplicity, or compactness premise. -/ 97theorem atomicCounterexampleEndpoint : AtomicCounterexampleEndpoint.{v} := 98 shellFamilyEndpoint homogeneityShellFamily 99 100end MathlibAnnex.CStarAlgebra.CAR