Choosing the CAR shell family from proved homogeneity

MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily

def

CAR homogeneity and exact shell matching supply one family whose distinguished component is fixed by an explicit identity choice.

Statement

Let be the completed CAR algebra, the norm completion of the matrix stages under , with the fixed coordinate reindexing. Write for the canonical inclusion, for the root state, for its decreasing root projections, and for the difference shells. Each is a self-adjoint projection. Let be the set of unitary-equivalence classes of pure-state Gelfand–Naimark–Segal (GNS) representations of . Choose a representative pure state for each , with the distinguished class represented by . Fix the following representative shell family. At , choose and . At every other , choose an automorphism from CAR homogeneity for the pair , and then choose shell links for that same automorphism. Thus , , and . This fixed choice is the homogeneity shell family.

Definition

The component supplier branches on . On the root branch, the root-state representative is exactly and , so identity and the shells themselves satisfy all component equations. On a non-root branch, homogeneity gives one with and approximate innerness. Apply the arbitrary-family shell-matching theorem to this and , and choose its link sequence. The two root lemmas certify the explicit branch, and the displayed definition assembles these data into one family.

Assumptions

The selected states are pure, including the root state. CAR homogeneity is a proved result, and the difference shells are projections. No external KOS proposition or pre-existing shell family is an input to this definition.

Conclusion

The definition supplies a value of the representative-family structure, including both root equations. The same selected value can be carried into later constructions without making a fresh choice at each use.

This is a fixed choice, not a uniqueness theorem for all possible families. In particular, the non-root links need not be unique. The subsequent structural theorem uses this very family. The present definition does not itself prove uniqueness of the irreducible representation class, the rank-one identities, simplicity, or the exclusion of compact-operator algebras.

Supporting route explanation

noncomputable def homogeneityShellFamily : RepresentativeShellFamily where
  data := representativeShellDataOfHomogeneity
  root_alpha := representativeShellDataOfHomogeneity_root_alpha
  root_link := representativeShellDataOfHomogeneity_root_link

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

Earlier published Card and PDF