CornerFactorStructure.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Factor and finite-isometry structure of represented corners

Countable full matrix units identify the original algebra with the actual amplification of its first corner. A central corner operator therefore inflates to a central ambient operator. Finiteness of the first projection also passes directly to the represented corner by extension by zero. No trace or semifinite decomposition is assumed in these arguments.

theorem OAI.KadisonKastler.FullMatrixCorner.amplified_representedCorner_eq line 27
Source documentation
Common full matrix units recover an algebra from its actual first corner.
```
theorem amplified_representedCorner_eq (M : VonNeumannAlgebra H)
    (hF : ∀ i j, F.entry i j ∈ M) :
    F.amplifiedAlgebra (representedCorner E M (F.zero_zero ▸ hF 0 0)) = M := by
…
```
Mentions: OAI.KadisonKastler.representedCorner
theorem OAI.KadisonKastler.FullMatrixCorner.inflateHom_injective line 40
theorem OAI.KadisonKastler.FullMatrixCorner.scalarCenter_representedCorner line 49
Source documentation
Scalar center descends through the concrete matrix-corner decomposition.
```
theorem scalarCenter_representedCorner (M : VonNeumannAlgebra H)
    (hF : ∀ i j, F.entry i j ∈ M) (hM : ScalarCenter M) :
    ScalarCenter (representedCorner E M (F.zero_zero ▸ hF 0 0)) := by
…
```
Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.representedCorner
theorem OAI.KadisonKastler.cornerExtension_injective line 75
Source documentation
Extension by zero is faithful, even when the original representation is not the standard tracial representation.
```
theorem cornerExtension_injective : Function.Injective (cornerExtension E) := by
…
```
Mentions: OAI.KadisonKastler.cornerExtension
theorem OAI.KadisonKastler.finite_representedCorner_of_finite_projection line 81
Source documentation
A finite ambient projection makes the represented corner a finite algebra.
```
theorem finite_representedCorner_of_finite_projection (M : VonNeumannAlgebra H)
    (hE : E.starProjection ∈ M)
    (hfinite : FiniteProjectionIn M ⟨E.starProjection, hE⟩) :
    ∀ v : Algebra (representedCorner E M hE),
      star v * v = 1 → v * star v = 1 := by
…
```
Mentions: OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.representedCorner
theorem OAI.KadisonKastler.representedCorner_nonzero_of_projection_ne_zero line 108
Source documentation
A nonzero corner projection gives a nonzero represented identity.
```
theorem representedCorner_nonzero_of_projection_ne_zero
    (hE : E.starProjection ≠ (0 : H →L[ℂ] H)) : (0 : E →L[ℂ] E) ≠ 1 := by
…
```

theorem OAI.KadisonKastler.diffuse_representedCorner line 116

Source documentation

Proper projection splittings remain proper after compression to a larger projection. Thus diffuseness passes to every represented corner.

theorem diffuse_representedCorner (M : VonNeumannAlgebra H)
    (hE : E.starProjection ∈ M)
    (hdiff : ∀ p : Algebra M, IsStarProjection p → p ≠ 0 →
      ∃ q : Algebra M, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q) :
    ∀ p : Algebra (representedCorner E M hE), IsStarProjection p → p ≠ 0 →
      ∃ q : Algebra (representedCorner E M hE), IsStarProjection q ∧ q ≠ 0 ∧
        q ≠ p ∧ p * q = q ∧ q * p = q := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.representedCorner

theorem OAI.KadisonKastler.FullMatrixCorner.representedCorner_isII1 line 205

Source documentation

The finite nonzero first corner of a diffuse scalar-center algebra is an actual II₁ factor. All projection and finiteness hypotheses are geometric.

theorem FullMatrixCorner.representedCorner_isII1 (F : FullMatrixCorner E)
    (M : VonNeumannAlgebra H) (hF : ∀ i j, F.entry i j ∈ M)
    (hM : ScalarCenter M) (hE0 : E.starProjection ≠ (0 : H →L[ℂ] H))
    (hfinite : FiniteProjectionIn M ⟨E.starProjection, F.zero_zero ▸ hF 0 0⟩)
    (hdiff : ∀ p : Algebra M, IsStarProjection p → p ≠ 0 →
      ∃ q : Algebra M, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q) :
    Generator.IsII1Factor
      (representedCorner E M (F.zero_zero ▸ hF 0 0)).toStarSubalgebra := by
…

Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.Algebra, OAI.Generator.IsII1Factor, OAI.KadisonKastler.representedCorner