OAI/Analysis/FactorGeneration/RepresentedFreeness.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Full freeness in the faithful bounded-operator representation. The quotient image is not asserted to be complete or weak-operator closed.

  1. abbrev OAI.Generator.Tracial.QuotientOperators line 20
  2. def OAI.Generator.Tracial.quotientVectorState line 22
  3. theorem OAI.Generator.Tracial.quotientVectorState_representation line 26
  4. theorem OAI.Generator.Tracial.quotientVectorState_one line 30
  5. def OAI.Generator.Tracial.representedUnitary line 35
  6. theorem OAI.Generator.Tracial.representedUnitary_coe line 38
  7. theorem OAI.Generator.Tracial.representedUnitary_power line 41
  8. theorem OAI.Generator.Tracial.represented_nonzero_powers line 47
  9. theorem OAI.Generator.Tracial.represented_centered_subalgebra line 57
  10. theorem OAI.Generator.Tracial.represented_haar_free line 70

    Source documentation

    The exact endpoint formula proves freeness for the actual represented C*(v) and the norm closure of the represented base algebra.

    theorem represented_haar_free (v : unitary (Q τ ω)) (D : Subalgebra ℂ (Q τ ω))
    (hhaar : ∀ n : ℤ,n ≠ 0 → quotientTrace τ ω (↑(v^n) : Q τ ω)=0)
    (hpow : alternatingMomentsZero (quotientTrace τ ω) (nonzeroUnitaryPowers v)
      {d | d ∈ D ∧ quotientTrace τ ω d=0}) :
    freeSets (A := QuotientOperators τ ω) (quotientVectorState τ ω)
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.alternatingMomentsZero, OAI.Generator.nonzeroUnitaryPowers, OAI.Generator.freeSets, OAI.Generator.Tracial.QuotientOperators, OAI.Generator.Tracial.quotientVectorState

  11. def OAI.Generator.Tracial.representedFreeFrom line 103
  12. def OAI.Generator.Tracial.representedClosedFree line 107
  13. theorem OAI.Generator.Tracial.represented_haar_free_interface line 110
  14. theorem OAI.Generator.Tracial.exists_coordinate_haar_free line 138