TracialCornerTransport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Corner unitaries and completed half projections are transported along the actual trace-preserving factor embedding. This retains their concrete support projections inside the conjugated free copy.

def OAI.KadisonSimilarity.cornerStarAlgHom line 18
Source documentation
A unital star homomorphism restricts to a unital homomorphism between the actual corners of corresponding projections.
```
def cornerStarAlgHom (e : A) (he : IsStarProjection e) :
    CStarCorner e he →⋆ₐ[ℂ] CStarCorner (φ e) (he.map φ) where
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.cornerStarAlgHom_coe line 38
def OAI.KadisonSimilarity.transportedCornerUnitary line 41
theorem OAI.KadisonSimilarity.haarCornerPower_transport line 45
theorem OAI.KadisonSimilarity.HaarCornerMoments.transport line 53
def OAI.KadisonSimilarity.HalfTraceProjectionData.transport line 64
Source documentation
Half-trace completion and both support identities survive the factor embedding, as does the subsequently constructed centered reflection.
```
def HalfTraceProjectionData.transport
    {τA : A →ₗ[ℂ] ℂ} {τB : B →ₗ[ℂ] ℂ} (hφ : ∀ x, τB (φ x) = τA x)
    {e : A} (Q : HalfTraceProjectionData τA e) : HalfTraceProjectionData τB (φ e) where
…
```
Mentions: OAI.KadisonSimilarity.HalfTraceProjectionData