UnitalizedExtension.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Extension by zero is a nonunital star homomorphism. Its unitization provides a genuine representation whose distinguished projection recovers the original Hilbert subspace.

def OAI.KadisonSimilarity.isometricExtensionHom line 18
theorem OAI.KadisonSimilarity.separable_unitization line 37
def OAI.KadisonSimilarity.unitalizedExtension line 44
Source documentation
A unital representation retaining the zero extension of every original algebra element. The added unit acts on the full ambient Hilbert space.
```
def unitalizedExtension : Unitization ℂ B →⋆ₐ[ℂ] (K →L[ℂ] K) :=
…
```
theorem OAI.KadisonSimilarity.unitalizedExtension_inr line 47
theorem OAI.KadisonSimilarity.unitalizedExtension_apply line 52
theorem OAI.KadisonSimilarity.unitalizedExtension_old_unit line 59
Source documentation
The old unit becomes the orthogonal range projection of the embedding.
```
theorem unitalizedExtension_old_unit :
    unitalizedExtension J σ (Unitization.inr (1 : B)) =
      J.toContinuousLinearMap.comp J.toContinuousLinearMap.adjoint := by
…
```
Mentions: OAI.KadisonSimilarity.unitalizedExtension
theorem OAI.KadisonSimilarity.unitalizedExtension_commutes line 65