IntertwinerPolar.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The polar isometry of an injective bounded intertwiner. This form allows different source and target Hilbert spaces, as needed for closed cyclic graphs in the normal representation argument.

theorem OAI.KadisonSimilarity.isometry_of_injective_intertwiner line 19

Source documentation

An injective bounded intertwiner has an isometric polar part, even when its range is not closed.

theorem isometry_of_injective_intertwiner
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (L : H →L[ℂ] K) (hLi : Function.Injective L)
    (hL : ∀ a, L.comp (σ a) = (ρ a).comp L) :
    ∃ J : H →ₗᵢ[ℂ] K,
      (∀ a, J.toContinuousLinearMap.comp (σ a) = (ρ a).comp J.toContinuousLinearMap) ∧
      Set.range L ⊆ Set.range J := by
…

theorem OAI.KadisonSimilarity.isometry_of_injective_dense_correspondence line 79

Source documentation

A closed correspondence with injective first coordinate and dense second coordinate gives an isometric embedding of its second representation into its first. This is the operator step for a closable cyclic graph.

theorem isometry_of_injective_dense_correspondence
    {Q : Type*} [NormedAddCommGroup Q] [InnerProductSpace ℂ Q] [CompleteSpace Q]
    (ν : A →⋆ₐ[ℂ] (Q →L[ℂ] Q))
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (X : Q →L[ℂ] H) (Y : Q →L[ℂ] K)
    (hX : Function.Injective X) (hY : DenseRange Y)
    (hXν : ∀ a, X.comp (ν a) = (σ a).comp X)
    (hYν : ∀ a, Y.comp (ν a) = (ρ a).comp Y) :
    ∃ J : K →ₗᵢ[ℂ] H, ∀ a,
      J.toContinuousLinearMap.comp (ρ a) = (σ a).comp J.toContinuousLinearMap := by
…