Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/AtomicCounterexample.lean
Pinned GitHub source · Raw UTF-8 source
Back to Choosing the CAR shell family from proved homogeneity
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.GlobalTransport2import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicEndpoint34/-!5# Ordinary Naimark endpoint from the proved CAR homogeneity theorem67The shell family and concrete target in this file are chosen once. The8generic `MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty` is not changed or assumed: the closed CAR theorem9supplies exactly the representative-to-root automorphisms needed by the10family-parametric atomic construction.11-/1213set_option autoImplicit false1415noncomputable section1617namespace MathlibAnnex.CStarAlgebra.CAR1819open MathlibAnnex.Analysis.CStarAlgebra2021universe v2223/-- Canonical identity shell data at the distinguished root class. -/24private noncomputable def rootRepresentativeShellData :25 RepresentativeShellData completedRootPureState.classOf where26 alpha := StarAlgEquiv.refl ℂ Limit27 state_eq := rootShell_identity_family.128 link := rootShell29 initial_support := fun n ↦ (rootShell_identity_family.2 n).130 final_support := fun n ↦ (rootShell_identity_family.2 n).23132/-- For one selected pure-state class, closed CAR homogeneity supplies a33single automorphism. Generic approximate-inner shell matching then supplies34all exact shell links for that same automorphism. The root branch is fixed35canonically instead of invoking homogeneity. -/36noncomputable def representativeShellDataOfHomogeneity37 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : RepresentativeShellData j := by38 classical39 by_cases hj : j = completedRootPureState.classOf40 · subst j41 exact rootRepresentativeShellData42 · let hex := homogeneity43 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).144 completedRootPureState.145 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).246 completedRootPureState.247 let alpha := Classical.choose hex48 have halpha := Classical.choose_spec hex49 let hwex := MathlibAnnex.CStarAlgebra.exists_shell_family_of_approximately_inner50 Limit alpha halpha.2 rootShell isStarProjection_rootShell51 let w := Classical.choose hwex52 have hw := Classical.choose_spec hwex53 exact54 { alpha := alpha55 state_eq := halpha.156 link := w57 initial_support := fun n ↦ (hw n).158 final_support := fun n ↦ (hw n).2 }5960@[simp]61theorem representativeShellDataOfHomogeneity_root_alpha :62 (representativeShellDataOfHomogeneity63 completedRootPureState.classOf).alpha = StarAlgEquiv.refl ℂ Limit := by64 simp [representativeShellDataOfHomogeneity, rootRepresentativeShellData]6566@[simp]67theorem representativeShellDataOfHomogeneity_root_link (n : ℕ) :68 (representativeShellDataOfHomogeneity69 completedRootPureState.classOf).link n = rootShell n := by70 simp [representativeShellDataOfHomogeneity, rootRepresentativeShellData]7172/-- The one representative shell family used by the ordinary CAR endpoint. -/73noncomputable def homogeneityShellFamily : RepresentativeShellFamily where74 data := representativeShellDataOfHomogeneity75 root_alpha := representativeShellDataOfHomogeneity_root_alpha76 root_link := representativeShellDataOfHomogeneity_root_link7778/-- The single concrete C-star algebra used by every field of `AtomicCounterexampleEndpoint`. -/79abbrev AtomicCounterexampleAlgebra := ShellFamilyTarget homogeneityShellFamily8081/-- The actual completed CAR source map into the fixed main target. -/82noncomputable def atomicCounterexampleSourceHom : Limit →⋆ₐ[ℂ] AtomicCounterexampleAlgebra :=83 shellFamilySourceHom homogeneityShellFamily8485/-- The fixed faithful irreducible displayed representation of `AtomicCounterexampleAlgebra`. -/86noncomputable def atomicCounterexampleRepresentation :87 Representation AtomicCounterexampleAlgebra88 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=89 shellFamilyInclusion homogeneityShellFamily9091/-- Fully expanded ordinary endpoint for the single target chosen above. -/92abbrev AtomicCounterexampleEndpoint : Prop :=93 ShellFamilyEndpoint.{v} homogeneityShellFamily9495/-- Closed ordinary Naimark main for the actual CAR construction. It has no96generic KOS, shell-data, rank-one, capture, simplicity, or compactness premise. -/97theorem atomicCounterexampleEndpoint : AtomicCounterexampleEndpoint.{v} :=98 shellFamilyEndpoint homogeneityShellFamily99100end MathlibAnnex.CStarAlgebra.CAR