SimilarityUniverseTransfer.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Universe transfer for the similarity theorem

Raising the source algebra and the represented Hilbert space to a common universe changes neither the bounded homomorphism nor its similarity problem. The proof transports the actual invertible implementing operator through the induced star algebra equivalence of operator algebras.

instance OAI.KadisonSimilarity.SimilarityUniverseTransfer.uliftStarRing line 21
instance OAI.KadisonSimilarity.SimilarityUniverseTransfer.uliftStarModule line 28
instance OAI.KadisonSimilarity.SimilarityUniverseTransfer.uliftCStarAlgebra line 32
instance OAI.KadisonSimilarity.SimilarityUniverseTransfer.uliftInnerProductSpace line 38
def OAI.KadisonSimilarity.SimilarityUniverseTransfer.uliftStarAlgEquiv line 47
def OAI.KadisonSimilarity.SimilarityUniverseTransfer.transportBoundedHom line 58
Source documentation
Transport a bounded homomorphism through an algebra equivalence and an isometric Hilbert-space equivalence.
```
def transportBoundedHom (π : BoundedUnitalHom A H)
    (eA : B ≃⋆ₐ[ℂ] A) (heA : Continuous eA) (eH : H ≃ₗᵢ[ℂ] K) :
    BoundedUnitalHom B K :=
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom
theorem OAI.KadisonSimilarity.SimilarityUniverseTransfer.similarToStar_of_transport line 67
Source documentation
The invertible similarity operator transports back along the concrete operator star algebra equivalence.
```
theorem similarToStar_of_transport (π : BoundedUnitalHom A H)
    (eA : B ≃⋆ₐ[ℂ] A) (heA : Continuous eA) (eH : H ≃ₗᵢ[ℂ] K)
    (h : SimilarToStar B K (transportBoundedHom π eA heA eH)) :
    SimilarToStar A H π := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.SimilarToStar, OAI.KadisonSimilarity.SimilarityUniverseTransfer.transportBoundedHom
theorem OAI.KadisonSimilarity.SimilarityUniverseTransfer.similarityTheorem_of_commonUniverse line 87
Source documentation
A proof in a common larger universe gives the unrestricted two-universe similarity theorem. No representation or analytic hypothesis is added.
```
theorem similarityTheorem_of_commonUniverse
    (h : SimilarityTheorem.{max u v, max u v}) : SimilarityTheorem.{u,v} := by
…
```