The decreasing root projections in the CAR completion

MathlibAnnex.CStarAlgebra.CAR.rootFlag

def

The distinguished stage corners give a nested sequence of projections supporting the root state.

Statement

Let be the completed CAR algebra: the norm completion of the increasing union of under the unital embeddings (with the fixed coordinate reindexing). Write for the canonical isometric inclusion and for its matrix units. Let be the product-vector state determined by . Define . This sequence is the root flag.

Definition

At stage , the matrix has a single nonzero entry, equal to at the distinguished diagonal position. Send it into by . At the next stage, the new distinguished projection lies under the image of the preceding one, giving the decreasing relation. The finite matrix identity , together with the coordinate-preserving embeddings, explains the compression formula at later stages.

Assumptions

The zero coordinate is the same distinguished coordinate used by the standard stage inclusions. The index ranges over all natural numbers.

Conclusion

Each is a self-adjoint projection, , , and . For an element from stage , compression by at any later stage is exactly scalar: . The cited results establish these properties of the defined sequence.

The term rank one refers to inside the finite matrix algebra. It does not assert that the image of has one-dimensional range in a representation of the completed algebra. No norm or strong limit of the flag is part of this definition.

noncomputable def rootFlag (n : ℕ) : Limit :=
  ofStage n (rootProjection n)

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

Earlier published Card and PDF