OAI/Analysis/KadisonKastler/FiniteFactorAutomorphismProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Automorphisms preserve projection equivalence in a finite diffuse factor

The normalized trace and the constructed projection dimension identify a projection with its image under any star-algebra automorphism. This will compare a core window projection with its dual-character image.

  1. theorem OAI.KadisonKastler.equivalent_automorphism_projection line 28