Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.Analysis.CStarAlgebra.Representation.continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional
MathlibAnnex/Analysis/CStarAlgebra/Representation/DensityLowerBound.lean · lines 61–69
1import Mathlib.Tactic.FunProp 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.CompactModelDensity 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.OrdinarySingleton 4import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.DensityLowerBound 5 6/-! 7# Unital and ordinary-representation density endpoints 8 9These interfaces specialize the density argument to unital source algebras 10while retaining the original quantifier over ordinary nonzero irreducible 11representations. The unit need not be explicitly preserved by competitors. 12-/ 13 14set_option autoImplicit false 15 16open Set 17open scoped Cardinal ComplexOrder 18 19namespace MathlibAnnex.Analysis.CStarAlgebra 20 21universe u v 22 23variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 25 26namespace Representation 27 28/-- The density version of the ordinary-competitor Rosenberg conclusion. -/ 29theorem isCompactOperatorModel_of_singleton_amongNonUnital_of_dense 30 [Nontrivial A] (pi : Representation A H) 31 (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) 32 (s : Set H) (hs : Dense s) (hcard : #s < Cardinal.continuum) : 33 IsCompactOperatorModel pi.toNonUnitalStarAlgHom := 34 isCompactOperatorModel_of_singleton_of_dense pi hsingle.isSingletonIrreducibleModel s hs hcard 35 36/-- Dense subsets of an infinite-dimensional unital singleton model cannot 37have cardinality below the continuum. -/ 38theorem continuum_le_cardinalMk_dense_space_of_singleton_of_not_finiteDimensional 39 [Nontrivial A] (pi : Representation A H) 40 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) 41 (hA : ¬ FiniteDimensional ℂ A) (s : Set H) (hs : Dense s) : 42 Cardinal.continuum ≤ #s := by 43 by_contra h 44 exact hA (finiteDimensional_algebra_of_singleton_of_dense 45 pi hsingle s hs (lt_of_not_ge h)) 46 47/-- A small dense subset of a unital algebra gives a small dense subset of 48any nonzero irreducible model by continuity of one nonzero vector's orbit. -/ 49theorem exists_dense_cardinalMk_lt_continuum_of_isIrreducible 50 (pi : Representation A H) (hirr : pi.IsIrreducible) 51 (s : Set A) (hs : Dense s) (hcard : #s < Cardinal.continuum) : 52 ∃ t : Set H, Dense t ∧ #t < Cardinal.continuum := by 53 letI : Nontrivial H := nontrivial_of_isNonzero pi hirr.1 54 obtain ⟨x, hx⟩ : ∃ x : H, x ≠ 0 := exists_ne 0 55 have horbit := denseRange_orbitMap_of_isIrreducible pi hirr hx 56 have hcont : Continuous (fun a : A => pi a x) := by fun_prop 57 exact MathlibAnnex.Topology.exists_dense_cardinalMk_lt_continuum_of_continuous_denseRange 58 (fun a : A => pi a x) hcont horbit s hs hcard 59 60/-- The algebra's norm-density lower bound in the unital infinite-dimensional case. -/ 61theorem continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional 62 [Nontrivial A] (pi : Representation A H) 63 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) 64 (hA : ¬ FiniteDimensional ℂ A) (s : Set A) (hs : Dense s) : 65 Cardinal.continuum ≤ #s := by 66 by_contra h 67 obtain ⟨t, ht, htcard⟩ := exists_dense_cardinalMk_lt_continuum_of_isIrreducible 68 pi hsingle.1 s hs (lt_of_not_ge h) 69 exact hA (finiteDimensional_algebra_of_singleton_of_dense pi hsingle t ht htcard) 70 71/-- The same lower bound with all ordinary possibly nonunital competitors included. -/ 72theorem continuum_le_cardinalMk_dense_algebra_of_singleton_amongNonUnital_of_not_finiteDimensional 73 [Nontrivial A] (pi : Representation A H) 74 (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) 75 (hA : ¬ FiniteDimensional ℂ A) (s : Set A) (hs : Dense s) : 76 Cardinal.continuum ≤ #s := 77 continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional 78 pi hsingle.isSingletonIrreducibleModel hA s hs 79 80end Representation 81end MathlibAnnex.Analysis.CStarAlgebra