OAI/Analysis/KadisonKastler/InfiniteFactorProperInfiniteness.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

An infinite factor is properly infinite

A proper isometry supplies an infinite orthogonal sequence of equivalent wandering projections. A maximal orthogonal family of partial isometries with sources under the first wandering projection covers the identity by factoriality. Separability makes this family countable, so its ranges can be mapped into the even and odd wandering projections separately.

No trace, dimension function, or published projection comparison is used.

  1. def OAI.KadisonKastler.projectionComplement line 30
  2. theorem OAI.KadisonKastler.le_projectionComplement line 33
  3. theorem OAI.KadisonKastler.mul_eq_zero_of_le_complement line 38
  4. theorem OAI.KadisonKastler.projection_fixed_vectors_orthogonal line 44
  5. theorem OAI.KadisonKastler.projection_unit_vector line 62

    Source documentation

    A nonzero projection has a unit vector in its range.

    private theorem projection_unit_vector (p : AlgebraProjection M) (hp : p.val ≠ 0) :
    ∃ x : H, ‖x‖ = 1 ∧ (p.val : H →L[ℂ] H) x = x := by
…
  6. theorem OAI.KadisonKastler.countable_of_orthogonal_nonzero_projections line 85

    Source documentation

    Pairwise orthogonal nonzero projections in a separably acting algebra form a countable family.

    theorem countable_of_orthogonal_nonzero_projections [TopologicalSpace.SeparableSpace H]
    {ι : Type*} (p : ι → AlgebraProjection M)
    (hp : ∀ i, (p i).val ≠ 0)
    (ho : Pairwise (fun i j => (p i).val * (p j).val = 0)) : Countable ι := by
…
  7. def OAI.KadisonKastler.sourceFamily line 105
  8. theorem OAI.KadisonKastler.exists_maximal_sourceFamily line 110
  9. theorem OAI.KadisonKastler.target_ne_zero_of_support_ne_zero line 126
  10. theorem OAI.KadisonKastler.exists_countable_source_partition_of_projection_countability line 138

    Source documentation

    Every nonzero projection in a countably decomposable factor supplies a countable partition of the identity by ranges of partial isometries whose initial projections lie under the supplied projection.

    theorem exists_countable_source_partition_of_projection_countability
    (hFamilies : HasCountableProjectionFamilies M)
    (hfactor : ∀ c : Algebra M, (∀ a : Algebra M, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra M))
    (p : AlgebraProjection M) (hp : p.val ≠ 0) :
    ∃ a : ℕ → PartialIsometry M,
      (∀ n, (a n).support ≤ p) ∧
      Pairwise (fun i j => (a i).target.val * (a j).target.val = 0) ∧
      (∀ q : AlgebraProjection M, (∀ n, (a n).target ≤ q) →
        (1 : Algebra M) = q.val) := by
…

    Mentions: OAI.KadisonKastler.HasCountableProjectionFamilies, OAI.KadisonKastler.Algebra

  11. theorem OAI.KadisonKastler.exists_countable_source_partition line 225

    Source documentation

    The original separably acting specialization.

    theorem exists_countable_source_partition [TopologicalSpace.SeparableSpace H]
    (hfactor : ∀ c : Algebra M, (∀ a : Algebra M, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra M))
    (p : AlgebraProjection M) (hp : p.val ≠ 0) :
    ∃ a : ℕ → PartialIsometry M,
      (∀ n, (a n).support ≤ p) ∧
      Pairwise (fun i j => (a i).target.val * (a j).target.val = 0) ∧
      (∀ q : AlgebraProjection M, (∀ n, (a n).target ≤ q) →
        (1 : Algebra M) = q.val) :=
…

    Mentions: OAI.KadisonKastler.Algebra

  12. theorem OAI.KadisonKastler.star_pow_mul_pow line 238

    Also declared: OAI/Analysis/KadisonKastler/TypeIIIMatrixCorner.lean:38 (same declaration text).

  13. def OAI.KadisonKastler.wanderingProjection line 249

    Also declared: OAI/Analysis/KadisonKastler/TypeIIIMatrixCorner.lean:49 (same declaration text).

  14. theorem OAI.KadisonKastler.wanderingProjection_mul line 257

    Also declared: OAI/Analysis/KadisonKastler/TypeIIIMatrixCorner.lean:57 (same declaration text).

  15. theorem OAI.KadisonKastler.wanderingProjection_mul_pow line 262

    Also declared: OAI/Analysis/KadisonKastler/TypeIIIMatrixCorner.lean:62 (same declaration text).

  16. def OAI.KadisonKastler.wanderingPartialIsometry line 267

    Also declared: OAI/Analysis/KadisonKastler/TypeIIIMatrixCorner.lean:67 (same declaration text).

  17. theorem OAI.KadisonKastler.wandering_cross line 282

    Also declared: OAI/Analysis/KadisonKastler/TypeIIIMatrixCorner.lean:82 (same declaration text).

  18. theorem OAI.KadisonKastler.wandering_targets_orthogonal line 298

    Also declared: OAI/Analysis/KadisonKastler/TypeIIIMatrixCorner.lean:98 (same declaration text).

  19. theorem OAI.KadisonKastler.orthogonal_targets_of_sums line 319
  20. theorem OAI.KadisonKastler.properlyInfiniteIdentity_of_proper_isometry line 335

    Source documentation

    A proper isometry in a separably acting factor yields two isometries with orthogonal ranges.

    theorem properlyInfiniteIdentity_of_proper_isometry [Nontrivial H]
    [TopologicalSpace.SeparableSpace H] (hM : ScalarCenter M)
    (w : Algebra M) (hw : star w * w = 1) (hproper : w * star w ≠ 1) :
    ProperlyInfiniteIdentity M := by
…

    Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ProperlyInfiniteIdentity

  21. theorem OAI.KadisonKastler.publishedInfiniteFactorProperlyInfinite line 390

    Source documentation

    The formerly published infinite-factor projection input follows from concrete partial-isometry comparison and separability.

    theorem publishedInfiniteFactorProperlyInfinite :
    PublishedInfiniteFactorProperlyInfinite.{u} := by
…