Structural properties of one shell-generated C*-algebra

MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint

theorem

Collects the proved properties of a single generated algebra, keeping the shell-family input separate from its consequences.

Statement

For every fixed shell family, form , and as below. Then is nonzero, norm closed and infinite-dimensional, is injective and unital, and is faithful and irreducible. Every nonzero irreducible complex star representation of , even if not initially required to preserve the unit, is unitarily equivalent to . The only norm-closed two-sided ideals of are and , and has no injective star representation whose range is precisely all compact operators on any complex Hilbert space.

Assumptions

Let be the completed CAR algebra with matrix stages embedded by . Write for the image of the first diagonal matrix unit, , and for the root state characterized by on each stage, where is its canonical embedding.

Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes , with root index and representative states .

A fixed shell family consists of complex-linear unital star automorphisms and elements satisfying , and .

At the root, is the identity and .

Let be the Hilbert direct sum of these GNS spaces, their representation of , and its embedded unit cyclic vector, where is the selected unit cyclic vector and is coordinate inclusion.

Choose once a family of unitary operators from the construction of the shell unitaries: , , and . Here denotes the bounded complex-linear operators on .

Put , the norm-closed unital star algebra generated by these operators. Let be with its codomain restricted to , and let be inclusion.

The comparison Hilbert space may be any complete complex Hilbert space in an arbitrary independent universe. No separability or dimension bound on is added. The chosen family, links and algebra do not depend on that comparison universe.

Conclusion

All conclusions concern this same concrete . In the capture assertion, unitary equivalence means there is a surjective complex-linear isometry with for all and . In the compact-operator assertion, the competing map need not be unital and the zero Hilbert space is also covered.

The separately linked Lean structure lists these properties; defining that proposition does not prove it. This theorem proves that proposition for every supplied family. The family hypothesis remains explicit. The structural theorem for the homogeneity-based algebra and its faithful representation on a separable Hilbert space specialize this fixed-family result.

Proof route

The construction of the shell unitaries gives a faithful source map and irreducible inclusion. The unital copy of the infinite-dimensional CAR algebra makes nonzero and infinite-dimensional. The universal capture theorem supplies unitary equivalence for unital irreducible representations; irreducibility forces any nonzero possibly nonunital representation to preserve the unit. Ideal-separating pure GNS representations then yield simplicity. Finally a unital infinite-dimensional algebra cannot be represented injectively onto all compact operators.

theorem shellFamilyEndpoint (family : RepresentativeShellFamily) :
    ShellFamilyEndpoint.{v} family

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)

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

Earlier published Card and PDF