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.

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 .

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 .

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

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

Earlier published Card and PDF