ProperInfiniteProjectionCopies.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Countable copies of a full projection

A maximal orthogonal family with sources under a full projection gives a countable partition of the identity. Two orthogonal isometries provide room for countably many copies of the full projection. The partition embeds into their sum, and concrete projection Schroeder--Bernstein moves that sum onto the identity.

theorem OAI.KadisonKastler.exists_link_of_full line 27
def OAI.KadisonKastler.fullSourceFamily line 43
theorem OAI.KadisonKastler.exists_maximal_fullSourceFamily line 48
theorem OAI.KadisonKastler.nonzero_target line 64

theorem OAI.KadisonKastler.exists_countable_source_partition_of_full line 75

Source documentation

A full projection is the source bound for a countable orthogonal partition of the identity, even when the algebra is not a factor.

theorem exists_countable_source_partition_of_full [TopologicalSpace.SeparableSpace H]
    (p : AlgebraProjection M) (hp : (centralSupport p).val = 1) :
    ∃ 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.Algebra

def OAI.KadisonKastler.finiteProjectionSum line 155

theorem OAI.KadisonKastler.exists_orthogonal_projection_sum line 161

Source documentation

Orthogonal projection sums are strong sums in the original representation.

theorem exists_orthogonal_projection_sum (p : ℕ → AlgebraProjection M)
    (ho : Pairwise (fun i j => (p i).val * (p j).val = 0)) :
    ∃ q : AlgebraProjection M, (∀ i, p i ≤ q) ∧
      (∀ r : AlgebraProjection M, (∀ i, p i ≤ r) → q ≤ r) ∧
      ∀ x : H, HasSum (fun i => ((p i).val : H →L[ℂ] H) x)
        ((q.val : H →L[ℂ] H) x) := by
…

theorem OAI.KadisonKastler.isometry_power line 210
def OAI.KadisonKastler.copySlot line 220
theorem OAI.KadisonKastler.copySlot_cross line 235
theorem OAI.KadisonKastler.copySlot_orthogonal line 255
theorem OAI.KadisonKastler.exists_countable_projection_copies line 275
Source documentation
Countably many copies of a full projection fill a properly infinite, separably acting algebra. All the witnesses lie in the original algebra.
```
theorem exists_countable_projection_copies [TopologicalSpace.SeparableSpace H]
    (hM : ProperlyInfiniteIdentity M) (p : AlgebraProjection M)
    (hp : (centralSupport p).val = 1) : Nonempty (CountableProjectionCopies M p) := by
…
```
Mentions: OAI.KadisonKastler.ProperlyInfiniteIdentity, OAI.KadisonKastler.CountableProjectionCopies
theorem OAI.KadisonKastler.publishedProperInfiniteProjectionCopies line 341
Source documentation
Blackadar's countable full-projection copying assertion, proved from partial-isometry sums and projection Schroeder--Bernstein.
```
theorem publishedProperInfiniteProjectionCopies :
    PublishedProperInfiniteProjectionCopies.{u} := by
…
```