FactorizationGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing the kernel of a star intertwiner

A surjective intertwiner with a bounded right inverse restricts to an isomorphism on the orthogonal complement of its kernel. Orthogonal projection does not increase the right-inverse norm, which retains the sharp bound needed for quantitative similarity.

def OAI.KadisonSimilarity.restrictStarRepresentation line 22

Source documentation

Restriction of a star representation to a closed invariant subspace.

def restrictStarRepresentation (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (M : ClosedSubmodule ℂ K)
    (hM : ∀ a x, x ∈ M → σ a x ∈ M) : A →⋆ₐ[ℂ] (M →L[ℂ] M) where
…

theorem OAI.KadisonSimilarity.quantitative_similarity_of_surjective_intertwiner line 44

Source documentation

A bounded right inverse of a surjective star intertwiner gives similarity with no increase in the product of its two norms.

theorem quantitative_similarity_of_surjective_intertwiner
    (π : BoundedUnitalHom A H) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (W : H →L[ℂ] K) (L : K →L[ℂ] H) (hLW : L.comp W = 1)
    (hL : ∀ a, L.comp (σ a) = (π.1 a).comp L) :
    ∃ S : (H →L[ℂ] H)ˣ,
      ‖(S : H →L[ℂ] H)‖ * ‖(↑S⁻¹ : H →L[ℂ] H)‖ ≤ ‖W‖ * ‖L‖ ∧
      ∀ a, (S : H →L[ℂ] H) * π.1 (star a) * (↑S⁻¹ : H →L[ℂ] H) =
        star ((S : H →L[ℂ] H) * π.1 a * (↑S⁻¹ : H →L[ℂ] H)) := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom

theorem OAI.KadisonSimilarity.quantitative_similarity_of_factorization line 121

Source documentation

Multiplicativity upgrades a bounded star-representation factorization to a similarity, with the original product bound.

theorem quantitative_similarity_of_factorization
    (π : BoundedUnitalHom A H) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (W : H →L[ℂ] K) (L : K →L[ℂ] H)
    (hf : ∀ a, L.comp ((σ a).comp W) = π.1 a) :
    ∃ S : (H →L[ℂ] H)ˣ,
      ‖(S : H →L[ℂ] H)‖ * ‖(↑S⁻¹ : H →L[ℂ] H)‖ ≤ ‖W‖ * ‖L‖ ∧
      ∀ a, (S : H →L[ℂ] H) * π.1 (star a) * (↑S⁻¹ : H →L[ℂ] H) =
        star ((S : H →L[ℂ] H) * π.1 a * (↑S⁻¹ : H →L[ℂ] H)) := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom