Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.Analysis.CStarAlgebra.Representation.IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel_toNonUnitalStarAlgHom
MathlibAnnex/Analysis/CStarAlgebra/Representation/DensityCharacter.lean · lines 21–32
1import MathlibAnnex.Topology.DensityCharacter 2import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.DensityLowerBound 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.OrdinarySingleton 4 5/-! 6# Exact density and the continuum-hypothesis obstruction 7 8The reverse implication is for an arbitrary ordinary singleton model, not just 9the fixed CAR construction and not just separably represented algebras. 10The algebra and displayed Hilbert universes are independent. The singleton 11quantifier uses the algebra universe, as in its existing provider API. 12-/ 13set_option autoImplicit false 14open scoped Cardinal ComplexOrder 15namespace MathlibAnnex.Analysis.CStarAlgebra 16open MathlibAnnex.Topology 17universe u v 18 19/-- Translate the existing ordinary-competitor singleton predicate into the 20genuinely nonunital-domain representation API without changing its quantifier. -/ 21theorem Representation.IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel_toNonUnitalStarAlgHom 22 {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 := by 28 refine ⟨?_, ?_⟩ 29 · exact NonUnitalRepresentation.isIrreducible_toNonUnitalStarAlgHom pi hpi.1 30 · intro K _ _ _ rho hrho 31 obtain ⟨U, hU⟩ := hpi.2 K rho hrho 32 exact ⟨U, fun a x => hU a x⟩ 33 34/-- Any possibly nonunital counterexample of exact norm density aleph one 35forces the continuum hypothesis. No separable representation is assumed. -/ 36theorem NonUnitalCStarRepresentation.continuum_eq_aleph_one_of_singleton_of_not_isCompactOperatorModel_of_hasDensityCharacter 37 {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 := by 45 obtain ⟨s, hs, hsc⟩ := hd.1 46 have hle := 47 NonUnitalCStarRepresentation.continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_isCompactOperatorModel 48 pi hpi hnot s hs 49 exact le_antisymm (hsc ▸ hle) Cardinal.aleph_one_le_continuum 50 51/-- An ordinary Naimark counterexample with exact norm density κ. 52 53The 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 := iA 59 ∃ (oA : PartialOrder A), 60 letI := oA 61 ∃ (sA : StarOrderedRing A) (nA : Nontrivial A), 62 letI := sA 63 letI := nA 64 ∃ (H : Type u) (nH : NormedAddCommGroup H), 65 letI := nH 66 ∃ (iH : InnerProductSpace ℂ H), 67 letI := iH 68 ∃ (cH : CompleteSpace H), 69 letI := cH 70 ∃ pi : NonUnitalCStarRepresentation A H, 71 NonUnitalCStarRepresentation.IsSingletonIrreducibleModel.{u, u, u} pi ∧ 72 (¬ IsCompactOperatorModel pi) ∧ HasDensityCharacter A κ 73 74/-- The density-aleph-one existence statement implies CH in any carrier universe. -/ 75theorem continuum_eq_aleph_one_of_existsNaimarkCounterexampleOfDensity 76 (h : ExistsNaimarkCounterexampleOfDensity (Cardinal.aleph 1 : Cardinal.{u})) : 77 (Cardinal.continuum : Cardinal.{u}) = Cardinal.aleph 1 := by 78 obtain ⟨A, iA, oA, sA, nA, H, nH, iH, cH, pi, hpi, hnot, hd⟩ := h 79 letI := iA 80 letI := oA 81 letI := sA 82 letI := nA 83 letI := nH 84 letI := iH 85 letI := cH 86 exact NonUnitalCStarRepresentation.continuum_eq_aleph_one_of_singleton_of_not_isCompactOperatorModel_of_hasDensityCharacter 87 pi hpi hnot hd 88 89end MathlibAnnex.Analysis.CStarAlgebra