The atomic inclusion representation

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleRepresentation

def

Defines the representation on the atomic Hilbert space, keeping it distinct from the separable tracial model.

Statement

Define πₐₜ: A → B(Hₐₜ) to be the inclusion representation of the fixed CAR-based operator algebra A. Thus πₐₜ(a)x = a(x).

Definition

The map is literal subtype inclusion. Its injectivity follows from this construction; its irreducibility is a further theorem, recorded in the counterexample theorem for A, rather than part of the meaning of a representation. Hₐₜ is not the CAR trace-GNS space Hτ.

Assumptions

Let A ⊆ B(Hₐₜ) be the fixed unital C*-algebra obtained by adjoining the chosen shell-link unitaries to the atomic representation of the CAR algebra C, and then taking the norm-closed unital *-algebra they generate. Regard A as a closed unital *-subalgebra of B(Hₐₜ), with its inherited algebraic operations.

Conclusion

A specified unital complex *-algebra homomorphism πₐₜ: A → B(Hₐₜ), given by the underlying operator of each element of A.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion

  Exact source attribution.

Lean source declaration (exact)

/-- The fixed faithful irreducible displayed representation of `AtomicCounterexampleAlgebra`. -/
noncomputable def atomicCounterexampleRepresentation :
    Representation AtomicCounterexampleAlgebra
      (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=
  shellFamilyInclusion homogeneityShellFamily

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Approved Card JSON

Lean realization notes

Source kind: noncomputable def. Exact name: atomicCounterexampleRepresentation. Representation A H is the unital *-homomorphism API. This definition specializes shellFamilyInclusion to homogeneityShellFamily.