TypeICyclicRepresentation.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The irreducible cyclic representation afforded by a minimal projection

A nonzero vector in a minimal projection determines a faithful irreducible cyclic representation of a factor. The construction uses the actual closed orbit in the given Hilbert space; no classification theorem is invoked.

abbrev OAI.KadisonKastler.typeICyclicSpace line 27
def OAI.KadisonKastler.typeICyclicVector line 30
def OAI.KadisonKastler.typeICyclicOperator line 33
theorem OAI.KadisonKastler.typeICyclicOperator_apply line 37
theorem OAI.KadisonKastler.typeICyclicOperator_star line 40
def OAI.KadisonKastler.typeICyclicHom line 52
theorem OAI.KadisonKastler.typeICyclicHom_apply line 62
theorem OAI.KadisonKastler.typeICyclicHom_cyclic line 65
theorem OAI.KadisonKastler.exists_nonzero_fixed_vector line 73
theorem OAI.KadisonKastler.minimal_corner_scalar line 84
theorem OAI.KadisonKastler.minimal_right_ideal_separating line 93
Source documentation
Evaluation at a nonzero vector in a minimal projection is faithful on the right ideal supported by that projection.
```
theorem minimal_right_ideal_separating (p : AlgebraProjection M)
    (hp : IsMinimalProjectionIn M p) (ξ : H) (hξ : ξ ≠ 0)
    (hpξ : p.val.val ξ = ξ) (a : Algebra M) (hap : a * p.val = a)
    (haξ : a.val ξ = 0) : a = 0 := by
…
```
Mentions: OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.typeICyclicHom_injective line 111
Source documentation
The cyclic restriction of a factor at a minimal projection is faithful.
```
theorem typeICyclicHom_injective (hM : ScalarCenter M) (p : AlgebraProjection M)
    (hp : IsMinimalProjectionIn M p) (ξ : H) (hξ : ξ ≠ 0)
    (hpξ : p.val.val ξ = ξ) : Function.Injective (typeICyclicHom (M := M) ξ) := by
…
```
Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.typeICyclicHom
theorem OAI.KadisonKastler.typeICyclicHom_norm line 145
theorem OAI.KadisonKastler.typeICyclicProjection_range line 154
Source documentation
The minimal projection restricts to a rank-one projection.
```
theorem typeICyclicProjection_range (p : AlgebraProjection M)
    (hp : IsMinimalProjectionIn M p) (ξ : H) (hpξ : p.val.val ξ = ξ)
    (y : typeICyclicSpace M ξ) :
    ∃ z : ℂ, typeICyclicHom ξ p.val y = z • typeICyclicVector M ξ := by
…
```
Mentions: OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.typeICyclicSpace, OAI.KadisonKastler.typeICyclicHom, OAI.KadisonKastler.typeICyclicVector

theorem OAI.KadisonKastler.typeICyclicHom_commutant line 177

Source documentation

Every operator commuting with this cyclic representation is scalar.

theorem typeICyclicHom_commutant (p : AlgebraProjection M)
    (hp : IsMinimalProjectionIn M p) (ξ : H) (hpξ : p.val.val ξ = ξ)
    (T : typeICyclicSpace M ξ →L[ℂ] typeICyclicSpace M ξ)
    (hT : ∀ a : Algebra M, typeICyclicHom ξ a * T = T * typeICyclicHom ξ a) :
    ∃ z : ℂ, T = z • 1 := by
…

Mentions: OAI.KadisonKastler.IsMinimalProjectionIn, OAI.KadisonKastler.typeICyclicSpace, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.typeICyclicHom