UnitizationProjection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Recover a represented unital algebra from its unitization by restricting to the image of its old unit.

theorem OAI.KadisonSimilarity.unitization_old_unit_commutes line 15
def OAI.KadisonSimilarity.unitizationProjection line 21
theorem OAI.KadisonSimilarity.unitizationProjection_isStarProjection line 24
theorem OAI.KadisonSimilarity.unitizationProjection_commutes line 32
def OAI.KadisonSimilarity.unitizationRangeRepresentation line 39
Source documentation
The original algebra acts unitally on the range of its own unit, even though its inclusion into its unitization is nonunital.
```
def unitizationRangeRepresentation (ρ : Unitization ℂ B →⋆ₐ[ℂ] (K →L[ℂ] K)) :
    B →⋆ₐ[ℂ]
      (projectionFiber (unitizationProjection ρ) (unitizationProjection_isStarProjection ρ) →L[ℂ]
        projectionFiber (unitizationProjection ρ) (unitizationProjection_isStarProjection ρ)) where
…
```
Mentions: OAI.KadisonSimilarity.projectionFiber, OAI.KadisonSimilarity.unitizationProjection, OAI.KadisonSimilarity.unitizationProjection_isStarProjection
theorem OAI.KadisonSimilarity.unitizationRangeRepresentation_coe line 80