OAI/Analysis/KadisonSimilarity/Tracial/TracialMatrixCenter.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Density of full matrix stages forces the center of the original faithful tracial algebra to be scalar.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.central_stage_pairing line 22
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.central_eq_trace_smul_one line 43

    Source documentation

    No nonscalar central element survives density of the full matrix stages.

    theorem central_eq_trace_smul_one (hf : Function.Injective G.vector)
    (c : P) (hc : ∀ a : P, a * c = c * a) : c = G.trace c • (1 : P) := by
…
  3. theorem OAI.KadisonSimilarity.TracialCornerGeometry.scalar_center_of_matrix_tower line 60