MATHLIBANNEX / CANONICAL DECLARATION CARD

A simple C*-algebra with a unique irreducible representation class

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint

theorem

Establishes the properties that make the fixed algebra a counterexample to Naimark’s problem.

Statement

Let be the completed CAR algebra. Let be the direct sum of one chosen GNS representation from each pure-state GNS equivalence class, and let be the unitaries obtained from the fixed CAR homogeneity and shell construction. Put , and write for the embedding into . Let be the inclusion representation. Then is a nonzero, norm-closed, infinite-dimensional unital C*-algebra, is injective and unital, and is faithful and nonzero irreducible. Every nonzero irreducible -representation on a complex Hilbert space is unitarily equivalent to , even if is not assumed: there is a unitary with The algebra is simple: every norm-closed two-sided ideal is or . Moreover, for no complex Hilbert space is there an injective -representation with .

Assumptions

The automorphisms and shell unitaries are obtained from CAR homogeneity and fixed once. No simplicity or uniqueness-of-representation assumption is supplied to the theorem. The Hilbert space in the representation and compact-operator assertions is arbitrary; separability and preservation of the identity by the given representation are not assumed.

Conclusion

Thus has exactly one unitary-equivalence class of nonzero irreducible -representations, but is not isomorphic to the full algebra of compact operators on any Hilbert space. The nonzero, norm-closed algebra , its injective unital embedding and its faithful irreducible inclusion are the same throughout these assertions.

In the displayed inclusion representation, one also has . This follows from the stated properties: the intersection is a closed two-sided ideal of ; if it were nonzero, simplicity would give . Then would be compact, so , and hence , would be finite dimensional, a contradiction. This is a consequence of the theorem, not an extra field of its Lean statement.

Proof route

Apply the cited theorem for a fixed shell family to the family supplied by CAR homogeneity. The construction and the representation-classification theorem give the embedding and unitary equivalences; their cited consequences give simplicity and the exclusion of an algebra of compact operators.

Proof steps

  1. Let denote the class of the distinguished pure state, let be the decreasing root projections, and write for their shells. At choose and . In each other class, CAR homogeneity supplies one automorphism , and exact shell matching supplies all for that same . These choices are made once for the entire construction.

  2. The shell construction supplies an injective unital embedding and an irreducible inclusion . Since embeds the infinite-dimensional algebra , the algebra is infinite dimensional. Its norm closure is part of its construction, and its nonzeroness follows from injectivity of .

  3. The representation-classification theorem for this fixed family gives unitary equivalence with for every unital nonzero irreducible representation. The cited unitality lemma gives for every nonzero irreducible -representation of , so the same conclusion applies without initially assuming that preserves the identity.

  4. The cited simplicity theorem applies because is faithful and all nonzero irreducible representations are unitarily equivalent to it. The cited compact-operator exclusion applies because is unital and infinite dimensional. The Lean theorem collects these proved properties for the same algebra.

Main citations

Supporting route explanation

Lean source signature (exact)

theorem atomicCounterexampleEndpoint : AtomicCounterexampleEndpoint.{v}
In the source Mathematical meaning
theorem atomicCounterexampleEndpoint This theorem has no shell-family or simplicity premise. It proves the stated properties for the fixed homogeneity construction.
AtomicCounterexampleEndpoint.{v} The result abbreviation is ShellFamilyEndpoint.{v} homogeneityShellFamily. The two separate complete exact declarations and ten independent field rows below resolve the short result type locally.
homogeneityShellFamily The once-fixed automorphisms and shell links supplied by proved CAR homogeneity. They determine the same target , source and inclusion across every field, before any comparison Hilbert space is quantified.

These are two separate exact related declarations: the result abbreviation (AtomicCounterexample.lean, lines 92–93), then its ten-field proposition (AtomicEndpoint.lean, lines 194–229). Neither is a replacement or extension of the theorem signature above. Here the family is the fixed homogeneityShellFamily, so have exactly the meaning given in this Card.

abbrev AtomicCounterexampleEndpoint : Prop :=
  ShellFamilyEndpoint.{v} homogeneityShellFamily
structure ShellFamilyEndpoint (family : RepresentativeShellFamily) : Prop where
  nontrivial_target : Nontrivial (ShellFamilyTarget family)
  isClosed_target :
    IsClosed
      (ShellFamilyTarget family : Set
        (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
          MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))
  source_injective : Function.Injective (shellFamilySourceHom family)
  source_unital : shellFamilySourceHom family 1 = 1
  not_finiteDimensional_target :
    ¬ FiniteDimensional ℂ (ShellFamilyTarget family)
  ambient_injective : Function.Injective (shellFamilyInclusion family)
  isIrreducible_ambient :
    Representation.IsIrreducible (shellFamilyInclusion family)
  captures_nonunital :
    ∀ (K : Type v) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
      [CompleteSpace K]
      (rho : NonUnitalRepresentation
        (A := ShellFamilyTarget family) (H := K)),
      rho.IsIrreducible →
        ∃ U :
            MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K,
          ∀ (a : ShellFamilyTarget family)
            (x : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState),
            U (shellFamilyInclusion family a x) = rho a (U x)
  closedIdeal_dichotomy :
    ∀ I : TwoSidedIdeal (ShellFamilyTarget family),
      IsClosed (I : Set (ShellFamilyTarget family)) → I = ⊥ ∨ I = ⊤
  not_compactOperatorModel :
    ∀ (K : Type v) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
      [CompleteSpace K]
      (e : ShellFamilyTarget family →⋆ₙₐ[ℂ] (K →L[ℂ] K)),
      ¬ (Function.Injective e ∧
        (∀ a : ShellFamilyTarget family, IsCompactOperator (e a)) ∧
        ∀ T : K →L[ℂ] K, IsCompactOperator T →
          ∃ a : ShellFamilyTarget family, e a = T)
In the source Mathematical meaning
nontrivial_target The fixed algebra is nonzero.
isClosed_target The set is closed for the operator norm.
source_injective The fixed source map , , is injective.
source_unital The same map sends to .
not_finiteDimensional_target is not finite-dimensional over .
ambient_injective The literal inclusion is injective.
isIrreducible_ambient This same is nonzero irreducible: it has no proper nonzero closed reducing subspace.
captures_nonunital After the family and have been fixed, for every complete complex Hilbert space in universe v and every nonzero irreducible possibly nonunital , there is a surjective complex-linear isometry with for every , .
closedIdeal_dichotomy For every two-sided ideal in , if its underlying set is norm closed, then or .
not_compactOperatorModel For every complete complex Hilbert space and every possibly nonunital star homomorphism , it is impossible that is injective, all are compact, and every compact operator on equals some . The zero space is included.

Further source notes: AtomicCounterexampleEndpoint abbreviates ShellFamilyEndpoint homogeneityShellFamily; the separate abbreviation and the full structure are linked. In those fields, atomicCounterexampleRepresentation is , atomicCounterexampleSourceHom is , and captures_nonunital is the unitary-equivalence assertion for an arbitrary nonzero irreducible representation, without an initial unit-preservation assumption. These names occur in the linked structure and proof, not as extra arguments in this short signature.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint

Accepted content SHA-256: 4f19d4781905308f229b4ea228939a26a179391596c6514aafe076ff333edff0

Accepted source guide SHA-256: 32760d0a20eb09e1d7ef851c419a26f9d192ee9cd26cab6fbb946e8f3ec39017

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑