OperatorTypeI.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Type I structure of full operator algebras

Every nonzero operator projection dominates a nonzero abelian rank-one projection. This verifies the type-I condition used in the classical vanishing input. In particular a full operator algebra has no type II₁ central summand. No trace or cohomological vanishing is assumed.

lemma OAI.BoundedHochschild.KadisonRingrose.exists_apply_ne_zero line 27
Source documentation
A nonzero operator has a vector on which it is nonzero.
```
lemma exists_apply_ne_zero {T : H →L[ℂ] H} (hT : T ≠ 0) : ∃ x : H, T x ≠ 0 := by
…
```

lemma OAI.BoundedHochschild.KadisonRingrose.projection_fixes_unit_vector line 35

Source documentation

A nonzero projection fixes a unit vector.

lemma projection_fixes_unit_vector {p : H →L[ℂ] H} (hp : IsStarProjection p)
    (hp0 : p ≠ 0) : ∃ x : H, ‖x‖ = 1 ∧ p x = x := by
…

lemma OAI.BoundedHochschild.KadisonRingrose.rankOne_abelian line 43
Source documentation
A rank-one orthogonal projection has an abelian corner.
```
lemma rankOne_abelian (x : H) (hx : ‖x‖ = 1) :
    ∃ hq : IsStarProjection (InnerProductSpace.rankOne ℂ x x),
      PopaTypeII.AbelianProjection hq := by
…
```
Mentions: OAI.PopaTypeII.AbelianProjection

theorem OAI.BoundedHochschild.KadisonRingrose.operator_projection_has_abelian_subprojection line 73

Source documentation

Every nonzero operator projection contains a rank-one abelian projection.

theorem operator_projection_has_abelian_subprojection {p : H →L[ℂ] H}
    (hp : IsStarProjection p) (hp0 : p ≠ 0) :
    ∃ q : H →L[ℂ] H, ∃ hq : IsStarProjection q,
      q ≤ p ∧ q ≠ 0 ∧ PopaTypeII.AbelianProjection hq := by
…

Mentions: OAI.PopaTypeII.AbelianProjection

lemma OAI.BoundedHochschild.KadisonRingrose.map_starProjection line 97
lemma OAI.BoundedHochschild.KadisonRingrose.abelianProjection_of_map line 105
theorem OAI.BoundedHochschild.KadisonRingrose.typeICorner_one_of_operator_equiv line 125
Source documentation
An actual full-operator-algebra presentation satisfies the type I condition.
```
theorem typeICorner_one_of_operator_equiv (φ : N ≃⋆ₐ[ℂ] (H →L[ℂ] H)) :
    PopaTypeII.TypeICorner (IsStarProjection.one N) := by
…
```
Mentions: OAI.PopaTypeII.TypeICorner

theorem OAI.BoundedHochschild.KadisonRingrose.central_operator_projection_eq_one line 162

Source documentation

A central operator projection is either zero or the identity.

theorem central_operator_projection_eq_one {z : H →L[ℂ] H} (hz : IsStarProjection z)
    (hc : ∀ T : H →L[ℂ] H, z * T = T * z) (hz0 : z ≠ 0) : z = 1 := by
…

theorem OAI.BoundedHochschild.KadisonRingrose.operators_noTypeII1Summand line 173
Source documentation
Full operator algebras have no type II₁ central summand.
```
theorem operators_noTypeII1Summand : NoTypeII1Summand (H →L[ℂ] H) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NoTypeII1Summand