IntertwinerExtension.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Extension by zero along an isometric Hilbert-space embedding. These identities transport the central commutant to the common scalar L² model.

def OAI.KadisonSimilarity.isometricExtension line 18
Source documentation
The actual operator equal to T on the range of J and zero on its orthogonal complement.
```
def isometricExtension (T : H →L[ℂ] H) : K →L[ℂ] K :=
…
```
theorem OAI.KadisonSimilarity.isometricExtension_on_range line 21
theorem OAI.KadisonSimilarity.isometricExtension_sub line 28
theorem OAI.KadisonSimilarity.isometricExtension_add line 35
theorem OAI.KadisonSimilarity.isometricExtension_mul line 42
theorem OAI.KadisonSimilarity.isometricExtension_star line 50
theorem OAI.KadisonSimilarity.isometricExtension_injective line 56
theorem OAI.KadisonSimilarity.isometricExtension_norm line 63

theorem OAI.KadisonSimilarity.isometricExtension_compression line 90

Source documentation

Compressing an operator supported on the isometric range and extending it back recovers the original operator.

theorem isometricExtension_compression
    (Q : K →L[ℂ] K)
    (hleft : isometricExtension J 1 * Q = Q)
    (hright : Q * isometricExtension J 1 = Q) :
    isometricExtension J
      ((J.toContinuousLinearMap.adjoint.comp Q).comp J.toContinuousLinearMap) = Q := by
…

Mentions: OAI.KadisonSimilarity.isometricExtension

theorem OAI.KadisonSimilarity.isometricExtension_commutes line 107

Source documentation

Star-compatible intertwining transports commutation to the extension.

theorem isometricExtension_commutes
    (S : H →L[ℂ] H) (R : K →L[ℂ] K)
    (hJ : J.toContinuousLinearMap.comp S = R.comp J.toContinuousLinearMap)
    (hJstar : J.toContinuousLinearMap.comp (star S) = (star R).comp J.toContinuousLinearMap)
    (T : H →L[ℂ] H) (hT : T * S = S * T) :
    isometricExtension J T * R = R * isometricExtension J T := by
…

Mentions: OAI.KadisonSimilarity.isometricExtension

theorem OAI.KadisonSimilarity.isometricExtension_commutes_representations line 131

Source documentation

A star intertwiner transports the whole represented commutant.

theorem isometricExtension_commutes_representations
    {A : Type*} [CStarAlgebra A]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (hJ : ∀ a, J.toContinuousLinearMap.comp (σ a) = (ρ a).comp J.toContinuousLinearMap)
    (T : H →L[ℂ] H) (hT : ∀ a, T * σ a = σ a * T) (a : A) :
    isometricExtension J T * ρ a = ρ a * isometricExtension J T := by
…

Mentions: OAI.KadisonSimilarity.isometricExtension

theorem OAI.KadisonSimilarity.isometricExtension_commutes_representations_of_apply line 142

Source documentation

Pointwise intertwining is sufficient; form the equality of bounded operators before specializing to a concrete L² model.

theorem isometricExtension_commutes_representations_of_apply
    {A : Type*} [CStarAlgebra A]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (hJ : ∀ a x, J (σ a x) = ρ a (J x))
    (T : H →L[ℂ] H) (hT : ∀ a, T * σ a = σ a * T) (a : A) :
    isometricExtension J T * ρ a = ρ a * isometricExtension J T :=
…

Mentions: OAI.KadisonSimilarity.isometricExtension

theorem OAI.KadisonSimilarity.isometricCompression_commutes_representations_of_apply line 153

Source documentation

Compression through a star intertwiner preserves commutation with the represented algebra. No support hypothesis is required.

theorem isometricCompression_commutes_representations_of_apply
    {A : Type*} [CStarAlgebra A]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (hJ : ∀ a x, J (σ a x) = ρ a (J x))
    (Q : K →L[ℂ] K) (hQ : ∀ a, Q * ρ a = ρ a * Q) (a : A) :
    ((J.toContinuousLinearMap.adjoint.comp Q).comp J.toContinuousLinearMap) * σ a =
      σ a * ((J.toContinuousLinearMap.adjoint.comp Q).comp J.toContinuousLinearMap) := by
…