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 .

Main citations

Lean source signature (exact)

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

Here completedRootPureState is the root state bundled with its purity proof. data j contains and the equations of RepresentativeShellData j. root_alpha and root_link fix the component at completedRootPureState.classOf, namely . rootShell n is , whereas rootFlag n is . The separate exact excerpt below shows the component's full fields.

Related definition — separate exact excerpt

/-- Natural source data for one selected pure-state class.  Its fields are
only the automorphism and exact algebraic shell links obtained from KOS. -/
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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:3e800cc2482d039e0c10ab2af30dfa967a720a6eaf1fd7a550ad235a099cef66

Card revision: 1 · SHA-256: 1c532d64db83192c067a4e726afa6d4c4cd941d770a97dbf2687faf8544821f7

Exposition revision: 2 · SHA-256: ab4382383328c50b9b99ff1d004e2458b9c7fe0f4829510848d1999feb971733

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: d2bff7ed9ea98d6f53b55a4ac0b96a8f5507f8f1903e93f2cd488b7a91dbbad1