OAI/Analysis/KadisonSimilarity/Tracial/FiniteFactorPresentation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The finite diffuse branch has a constructed normal trace and an actual irreducible matrix source. Its sole remaining local input is Popa freeness.

  1. def OAI.KadisonSimilarity.normalGNSRepresentation line 23
  2. def OAI.KadisonSimilarity.normalGNSEquivalence line 28
  3. theorem OAI.KadisonSimilarity.normalGNSRepresentation_trace line 33
  4. structure OAI.KadisonSimilarity.NormalFiniteTrace line 50

    Source documentation

    The constructed normalized faithful normal trace.

    structure NormalFiniteTrace where
…
  5. structure OAI.KadisonSimilarity.IrreducibleMatrixSource line 58

    Source documentation

    The actual increasing irreducible matrix source in a fixed normal representation.

    structure IrreducibleMatrixSource {K : Type u} [NormedAddCommGroup K]
    [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) where
…
  6. structure OAI.KadisonSimilarity.FiniteFactorPresentation line 69

    Source documentation

    All finite-factor presentation data except the local free position. The represented Hilbert space is bundled to keep the GNS implementation opaque.

    structure FiniteFactorPresentation where
…
  7. theorem OAI.KadisonSimilarity.exists_finiteFactorPresentation line 84
  8. theorem OAI.KadisonSimilarity.factor_structural_cases line 109

    Source documentation

    The structural factor split is proved before invoking any free-position input.

    theorem factor_structural_cases [Nontrivial H]
    (hfactor : ∀ a : P.toStarSubalgebra, (∀ b, a * b = b * a) →
      ∃ c : ℂ, a = algebraMap ℂ P.toStarSubalgebra c) :
    IsII1Factor P.toStarSubalgebra ∨ HasInternalIsometryRows P ∨
      Nonempty (FiniteMatrixFactorModel P) := by
…

    Mentions: OAI.KadisonSimilarity.HasInternalIsometryRows, OAI.KadisonSimilarity.FiniteMatrixFactorModel

  9. theorem OAI.KadisonSimilarity.FiniteFactorPresentation.normal line 134
  10. def OAI.KadisonSimilarity.FiniteFactorPresentation.inclusion line 137
  11. theorem OAI.KadisonSimilarity.FiniteFactorPresentation.trace_inclusion line 140
  12. def OAI.KadisonSimilarity.FiniteFactorPresentation.FreePosition line 145
  13. def OAI.KadisonSimilarity.FiniteFactorPresentation.model line 151
  14. theorem OAI.KadisonSimilarity.publishedFactorCases_of_free_position line 168

    Source documentation

    Factor classification and the normal matrix presentation reduce the finite diffuse case to prescribed-source free position.

    theorem publishedFactorCases_of_free_position [Nontrivial H] [TopologicalSpace.SeparableSpace H]
    (hfactor : ∀ a : P.toStarSubalgebra, (∀ b, a * b = b * a) →
      ∃ c : ℂ, a = algebraMap ℂ P.toStarSubalgebra c)
    (hfree : ∀ F : FiniteFactorPresentation P,
      ∃ (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ) ≤ Filter.cofinite), F.FreePosition ω hω) :
    PublishedFactorCasesInput P := by
…

    Mentions: OAI.KadisonSimilarity.FiniteFactorPresentation, OAI.KadisonSimilarity.PublishedFactorCasesInput