FactorizationSpace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The reducing space generated by a homomorphism factorization

Only the vectors generated by the right factor are needed. Multiplicativity makes the left factor an intertwiner on this closed span. Its kernel is then a reducing subspace, which is the geometric input to invertible similarity.

def OAI.KadisonSimilarity.factorizationSpace line 22
Source documentation
The closed cyclic span of the range of the right factor.
```
def factorizationSpace (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (W : H →L[ℂ] K) :
    ClosedSubmodule ℂ K :=
…
```
theorem OAI.KadisonSimilarity.right_mem_factorizationSpace line 26

theorem OAI.KadisonSimilarity.factorizationSpace_invariant line 33

Source documentation

The generating space is invariant under the whole star representation.

theorem factorizationSpace_invariant (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (W : H →L[ℂ] K) (a : A) (x : K) (hx : x ∈ factorizationSpace σ W) :
    σ a x ∈ factorizationSpace σ W := by
…

Mentions: OAI.KadisonSimilarity.factorizationSpace

theorem OAI.KadisonSimilarity.left_intertwines_factorizationSpace line 47
Source documentation
The left factor intertwines on the closed cyclic span, by continuity from the algebraic generators and multiplicativity of the homomorphism.
```
theorem left_intertwines_factorizationSpace (π : BoundedUnitalHom A H)
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (W : H →L[ℂ] K) (L : K →L[ℂ] H)
    (hf : ∀ a, L.comp ((σ a).comp W) = π.1 a)
    (a : A) (x : K) (hx : x ∈ factorizationSpace σ W) :
    L (σ a x) = π.1 a (L x) := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.factorizationSpace