Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Cardinality.lean
Pinned GitHub source · Raw UTF-8 source
Back to Exact norm density of the fixed atomic algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.SeparableFaithful2import MathlibAnnex.Analysis.CStarAlgebra.Representation.SeparableCardinality3import MathlibAnnex.Analysis.CStarAlgebra.Representation.DensityLowerBound4import MathlibAnnex.Analysis.CStarAlgebra.Representation.DensityCharacter56/-!7# Cardinality and norm density of the fixed atomic counterexample89The upper bound comes from the already constructed faithful separable model.10The lower bound applies to every norm-dense subset of this same algebra.11The whole-carrier cardinality and norm density are distinguished throughout.12-/13set_option autoImplicit false14open Set15open scoped Cardinal ComplexOrder16namespace MathlibAnnex.CStarAlgebra.CAR17open MathlibAnnex.Analysis.CStarAlgebra MathlibAnnex.Topology1819/-- The existing faithful separable representation bounds the fixed carrier. -/20theorem cardinalMk_atomicCounterexampleAlgebra_le_continuum :21 #AtomicCounterexampleAlgebra ≤ Cardinal.continuum := by22 letI : TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace :=23 separableSpace_separableCounterexampleHilbertSpace24 exact Representation.cardinalMk_le_continuum_of_injective25 separableCounterexampleRepresentation separableCounterexampleRepresentation_injective2627/-- No norm-dense subset of the fixed algebra is smaller than the continuum. -/28theorem continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra29 (s : Set AtomicCounterexampleAlgebra) (hs : Dense s) :30 Cardinal.continuum ≤ #s :=31 Representation.continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional32 (shellFamilyInclusion homogeneityShellFamily)33 (isUniqueIrreducibleModel_shellFamilyInclusion.{0} homogeneityShellFamily).234 (not_finiteDimensional_shellFamilyTarget homogeneityShellFamily) s hs3536/-- The cardinality of the underlying set of the fixed algebra is continuum. -/37theorem cardinalMk_atomicCounterexampleAlgebra :38 #AtomicCounterexampleAlgebra = Cardinal.continuum := by39 apply le_antisymm cardinalMk_atomicCounterexampleAlgebra_le_continuum40 simpa using continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra Set.univ dense_univ4142/-- The exact norm density of the same fixed algebra is continuum. -/43theorem hasDensityCharacter_atomicCounterexampleAlgebra :44 HasDensityCharacter AtomicCounterexampleAlgebra Cardinal.continuum :=45 HasDensityCharacter.of_cardinalMk_le_of_forall_dense46 cardinalMk_atomicCounterexampleAlgebra_le_continuum47 continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra4849/-- Under CH, the fixed algebra has exact norm density aleph one. CH is an50explicit premise, not an added axiom and not a conclusion asserted in ZFC. -/51theorem hasDensityCharacter_atomicCounterexampleAlgebra_of_continuum_eq_aleph_one52 (hCH : (Cardinal.continuum : Cardinal.{0}) = Cardinal.aleph 1) :53 HasDensityCharacter AtomicCounterexampleAlgebra (Cardinal.aleph 1) := by54 rw [← hCH]55 exact hasDensityCharacter_atomicCounterexampleAlgebra5657/-- Every dense subset of the fixed irreducible Hilbert model is at least58continuum-sized. This is norm density, not algebraic Hamel dimension. -/59theorem continuum_le_cardinalMk_dense_atomicCounterexampleHilbert60 (s : Set (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert61 completedRootPureState)) (hs : Dense s) : Cardinal.continuum ≤ #s :=62 Representation.continuum_le_cardinalMk_dense_space_of_singleton_of_not_finiteDimensional63 (shellFamilyInclusion homogeneityShellFamily)64 (isUniqueIrreducibleModel_shellFamilyInclusion.{0} homogeneityShellFamily).265 (not_finiteDimensional_shellFamilyTarget homogeneityShellFamily) s hs6667/-- The cyclic orbit bounds the exact norm density of the fixed irreducible68Hilbert model from above; the general Rosenberg bound gives the reverse. -/69theorem hasDensityCharacter_atomicCounterexampleHilbert :70 HasDensityCharacter71 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)72 Cardinal.continuum := by73 let H := MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState74 let pi : Representation AtomicCounterexampleAlgebra H :=75 shellFamilyInclusion homogeneityShellFamily76 have hirr : Representation.IsIrreducible pi :=77 isIrreducible_shellFamilyInclusion homogeneityShellFamily78 letI : Nontrivial H := Representation.nontrivial_of_isNonzero pi hirr.179 obtain ⟨x, hx⟩ : ∃ x : H, x ≠ 0 := exists_ne 080 let s : Set H := Set.range (fun a : AtomicCounterexampleAlgebra => pi a x)81 have hs : Dense s := Representation.denseRange_orbitMap_of_isIrreducible pi hirr hx82 have hupper' : Cardinal.lift.{0} (#s) ≤83 Cardinal.lift.{0} (#AtomicCounterexampleAlgebra) := Cardinal.mk_range_le_lift84 have hupper : #s ≤ Cardinal.continuum := by85 simpa [cardinalMk_atomicCounterexampleAlgebra] using hupper'86 refine ⟨⟨s, hs, le_antisymm hupper87 (continuum_le_cardinalMk_dense_atomicCounterexampleHilbert s hs)⟩,88 continuum_le_cardinalMk_dense_atomicCounterexampleHilbert⟩8990/-- The faithful separable model is infinite-dimensional: otherwise its91operator algebra, and hence the faithfully represented source, would be finite-dimensional. -/92theorem not_finiteDimensional_separableCounterexampleHilbertSpace :93 ¬ FiniteDimensional ℂ SeparableCounterexampleHilbertSpace := by94 intro hfinite95 letI : FiniteDimensional ℂ SeparableCounterexampleHilbertSpace := hfinite96 letI : FiniteDimensional ℂ97 (SeparableCounterexampleHilbertSpace →L[ℂ] SeparableCounterexampleHilbertSpace) :=98 ContinuousLinearMap.finiteDimensional99 exact (not_finiteDimensional_shellFamilyTarget homogeneityShellFamily)100 (FiniteDimensional.of_injective101 (LinearMapClass.linearMap separableCounterexampleRepresentation)102 separableCounterexampleRepresentation_injective)103104end MathlibAnnex.CStarAlgebra.CAR