A fixed representative family of CAR shell data

MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily

structure

One family records a transporting automorphism and exact shell links for each selected pure-state class, with an explicitly fixed root component.

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 . A representative shell family assigns to each an automorphism and links with for every , , and for every . At the distinguished class it further requires and .

Definition

The component structure stores , the equation , the sequence , and its initial and final supports. The family structure chooses a component for every class and adds the root equations. They normalize a distinguished component of this chosen family; they do not impose equality between arbitrary choices made in unrelated existence statements.

Assumptions

The CAR system, root state, and selected representatives are fixed. A family is supplied as data of this structure. There is no restriction that be countable, and this structure declaration does not itself prove the existence of such a family.

Conclusion

The fields are the component data for every class and the two root equations. Each component contains one automorphism, its state-transport equation, its link sequence, and both support equations. The root shell is distinguished from the nested flag projection .

No rank-one, capture, simplicity, compactness, or approximate-innerness conclusion is stored in this structure. A later constructor can use approximate innerness to build the links, but that construction property is not an extra field required of every supplied family.

Supporting route explanation

structure RepresentativeShellFamily where
  data : ∀ j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit, RepresentativeShellData j
  root_alpha : (data completedRootPureState.classOf).alpha =
    StarAlgEquiv.refl ℂ Limit
  root_link : ∀ n, (data completedRootPureState.classOf).link n = rootShell n

structure RepresentativeShellData (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) where
  alpha : Limit ≃⋆ₐ[ℂ] Limit
  state_eq : ∀ a : Limit,
    (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 (alpha a) =
      completedRootPureState.1 a
  link : ℕ → Limit
  initial_support : ∀ n,
    star (link n) * link n = alpha (rootShell n)
  final_support : ∀ n,
    link n * star (link n) = rootShell n

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

Earlier published Card and PDF