MATHLIBANNEX / CANONICAL DECLARATION CARD

A separably represented C*-algebra with no separable irreducible representation

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation

theorem

The same algebra has a faithful representation on a separable Hilbert space, but no nonzero irreducible representation on any separable Hilbert space.

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 normalized trace of . The algebra retains all the properties in the cited representation-classification theorem: it is nonzero, norm closed, unital, infinite dimensional and simple; is injective and unital; the inclusion is faithful and irreducible; every nonzero irreducible -representation of is unitarily equivalent to ; and is not isomorphic to the full algebra of compact operators on any Hilbert space. In addition, is nonzero and separable, and there exists a faithful unital representation . No separable complex Hilbert space carries a nonzero irreducible -representation of , even without assuming preservation of the identity.

Assumptions

All assertions concern the same generated algebra and the same fixed shell unitaries. The absence of irreducible representations is quantified over arbitrary separable complex Hilbert spaces. Norm separability of is neither required nor asserted.

Conclusion

has both the faithful representation on the separable space and the faithful irreducible representation on . The representation is reducible, whereas cannot be separable.

The faithful representation in the existential assertion is the already chosen . No different algebra or unrelated representation is chosen to establish the two separability assertions.

Proof route

Combine the classification and simplicity results for with the normalized CAR trace vector, the dense CAR orbit, faithfulness of , and the theorem excluding nonzero irreducible representations on separable Hilbert spaces.

Proof steps

  1. Let be the GNS representation and cyclic vector of . One has , so . The continuous map has dense range. Since is separable, is separable.

  2. Take the GNS representation of the chosen extension of to , and the unitary from the cited trace construction. Then is the established faithful representation on . The cited theorem excluding nonzero irreducible representations on separable Hilbert spaces applies to every -representation with separable. These statements are conjoined with the classification and structural properties of the same .

Main citations

Supporting route explanation

Lean source signature (exact)

theorem atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation :
    AtomicCounterexampleEndpoint.{v} ∧
    Nontrivial SeparableCounterexampleHilbertSpace ∧
    TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace ∧
    (∃ ρ : Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace,
      Function.Injective ρ) ∧
    (∀ (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
        [CompleteSpace H] [TopologicalSpace.SeparableSpace H],
      ∀ ρ : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H),
        ¬ ρ.IsIrreducible)
In the source Mathematical meaning
AtomicCounterexampleEndpoint.{v} First output: all ten structural properties of the same fixed target , source , and inclusion . The separate exact abbreviation, structure and field table below make this component explicit within this Card.
Nontrivial SeparableCounterexampleHilbertSpace Second output: the CAR trace GNS space is nonzero.
TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace Third output: this same has a countable norm-dense subset.
∃ ρ : Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace, Function.Injective ρ Fourth output: there exists an injective unital star representation , supplied by the fixed . It is faithful but is not asserted irreducible.
∀ (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [TopologicalSpace.SeparableSpace H] For the fifth output, now quantify any separable complete complex Hilbert space in universe v; it is not restricted to the previously fixed .
∀ ρ : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H), ¬ ρ.IsIrreducible For every possibly nonunital star representation on that , nonzero irreducibility fails. This universal is different in quantifier role from the fourth output’s existential representation. None of these outputs asserts norm separability of .

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: The long conjunction in the exact signature keeps AtomicCounterexampleEndpoint, Nontrivial and SeparableSpace of , an existential injective representation, and the universal exclusion statement separate. SeparableCounterexampleHilbertSpace is and NonUnitalRepresentation does not initially require . The proof chooses separableCounterexampleRepresentation, the same .

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_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation

Accepted content SHA-256: df641d48577ed178651ff18b5cdc2c3fb4e0d88c8cf4fd6d01b96628ed25d648

Accepted source guide SHA-256: 16f450a005ba142d889b4ec3737f5ca01b0d44a0d907db676530e2f74356bbf2

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑