Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/DensityCharacter.lean
Pinned GitHub source · Raw UTF-8 source
Back to CH and a Naimark counterexample of norm density aleph one · Back to A Naimark counterexample of continuum norm density
1import MathlibAnnex.Topology.DensityCharacter2import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.DensityLowerBound3import MathlibAnnex.Analysis.CStarAlgebra.Representation.OrdinarySingleton45/-!6# Exact density and the continuum-hypothesis obstruction78The reverse implication is for an arbitrary ordinary singleton model, not just9the fixed CAR construction and not just separably represented algebras.10The algebra and displayed Hilbert universes are independent. The singleton11quantifier uses the algebra universe, as in its existing provider API.12-/13set_option autoImplicit false14open scoped Cardinal ComplexOrder15namespace MathlibAnnex.Analysis.CStarAlgebra16open MathlibAnnex.Topology17universe u v1819/-- Translate the existing ordinary-competitor singleton predicate into the20genuinely nonunital-domain representation API without changing its quantifier. -/21theorem Representation.IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel_toNonUnitalStarAlgHom22 {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]23 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]24 {pi : Representation A H}25 (hpi : Representation.IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) :26 NonUnitalCStarRepresentation.IsSingletonIrreducibleModel.{u, v, u}27 pi.toNonUnitalStarAlgHom := by28 refine ⟨?_, ?_⟩29 · exact NonUnitalRepresentation.isIrreducible_toNonUnitalStarAlgHom pi hpi.130 · intro K _ _ _ rho hrho31 obtain ⟨U, hU⟩ := hpi.2 K rho hrho32 exact ⟨U, fun a x => hU a x⟩3334/-- Any possibly nonunital counterexample of exact norm density aleph one35forces the continuum hypothesis. No separable representation is assumed. -/36theorem NonUnitalCStarRepresentation.continuum_eq_aleph_one_of_singleton_of_not_isCompactOperatorModel_of_hasDensityCharacter37 {A : Type u} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]38 [Nontrivial A] {H : Type v} [NormedAddCommGroup H]39 [InnerProductSpace ℂ H] [CompleteSpace H]40 (pi : NonUnitalCStarRepresentation A H)41 (hpi : NonUnitalCStarRepresentation.IsSingletonIrreducibleModel.{u, v, u} pi)42 (hnot : ¬ IsCompactOperatorModel pi)43 (hd : HasDensityCharacter A (Cardinal.aleph 1)) :44 (Cardinal.continuum : Cardinal.{u}) = Cardinal.aleph 1 := by45 obtain ⟨s, hs, hsc⟩ := hd.146 have hle :=47 NonUnitalCStarRepresentation.continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_isCompactOperatorModel48 pi hpi hnot s hs49 exact le_antisymm (hsc ▸ hle) Cardinal.aleph_one_le_continuum5051/-- An ordinary Naimark counterexample with exact norm density κ.5253The source algebra need not have a unit; irreducibility includes nonzeroness.54The statement ranges over carriers and competitors in the indicated universe,55following the existing singleton API. It includes no separability hypothesis. -/56def ExistsNaimarkCounterexampleOfDensity (κ : Cardinal.{u}) : Prop :=57 ∃ (A : Type u) (iA : NonUnitalCStarAlgebra A),58 letI := iA59 ∃ (oA : PartialOrder A),60 letI := oA61 ∃ (sA : StarOrderedRing A) (nA : Nontrivial A),62 letI := sA63 letI := nA64 ∃ (H : Type u) (nH : NormedAddCommGroup H),65 letI := nH66 ∃ (iH : InnerProductSpace ℂ H),67 letI := iH68 ∃ (cH : CompleteSpace H),69 letI := cH70 ∃ pi : NonUnitalCStarRepresentation A H,71 NonUnitalCStarRepresentation.IsSingletonIrreducibleModel.{u, u, u} pi ∧72 (¬ IsCompactOperatorModel pi) ∧ HasDensityCharacter A κ7374/-- The density-aleph-one existence statement implies CH in any carrier universe. -/75theorem continuum_eq_aleph_one_of_existsNaimarkCounterexampleOfDensity76 (h : ExistsNaimarkCounterexampleOfDensity (Cardinal.aleph 1 : Cardinal.{u})) :77 (Cardinal.continuum : Cardinal.{u}) = Cardinal.aleph 1 := by78 obtain ⟨A, iA, oA, sA, nA, H, nH, iH, cH, pi, hpi, hnot, hd⟩ := h79 letI := iA80 letI := oA81 letI := sA82 letI := nA83 letI := nH84 letI := iH85 letI := cH86 exact NonUnitalCStarRepresentation.continuum_eq_aleph_one_of_singleton_of_not_isCompactOperatorModel_of_hasDensityCharacter87 pi hpi hnot hd8889end MathlibAnnex.Analysis.CStarAlgebra