MATHLIBANNEX / CANONICAL DECLARATION CARD

A finite-row average centralizes its matrix stage

MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_rowAverage

theorem

Turns an arbitrary element of the completed CAR algebra into one commuting with a prescribed finite matrix stage.

Statement

Let be the completed CAR algebra obtained from under , and write for the stage embedding. Set and , where are the standard matrix units, indexed from to . Define . Then for every and every .

Assumptions

The integer is arbitrary. Both and are arbitrary elements of the indicated algebras; neither positivity nor self-adjointness is assumed. The matrix units belong to one fixed stage and satisfy , , and .

Conclusion

The range of lies in the relative commutant of inside , namely the set of elements commuting with every member of that stage. The same finite-row formula works for every once is fixed.

Proof route

First test commutation against a matrix unit . Multiplying the defining sum on the left leaves only its term with index , while multiplying on the right leaves only its term with index . Both products are . Every matrix is the finite linear combination , so bilinearity gives the assertion for .

Proof steps

  1. Use the matrix-unit relations to compute .

  2. The same relations give . Thus every matrix unit commutes with .

  3. Expand and distribute multiplication through the finite sums and scalar multiples.

Main citations

Lean source signature (exact)

theorem ofStage_commute_rowAverage (n : ℕ) (c : Stage n) (b : Limit) :
    ofStage n c * rowAverageLinear n b = rowAverageLinear n b * ofStage n c

Here Limit is , Stage n is , ofStage n c is , and rowAverageLinear n b is . The source equality is precisely the commutation identity in the Statement.

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

Lean realization notes

The formula is a corner-based finite-row average, not an average over a unitary group. Separate cited results show , positivity, and the dimension-independent bound . The present theorem establishes exact commutation with this stage; it does not assert that lies in the center of all of .

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:6fbe44dcc304a80eafd8327b9ab6680b8df6ab9e4189faf651c71fdb0a348d05

Card revision: 1 · SHA-256: 0d68686d00c3d337c678c712c0b5b674b45f46ab6533112b36df34e5c43a9893

Exposition revision: 1 · SHA-256: 8b60ab2d1eb40cfeda293b0754bbe38f4ae60badb4750a9d46b7d803296d0db1

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 5ddb12441cea78b452dfbffa3285e7e76e0dbee44fd9821cb0a348947de859db

Back to top ↑