FreeProductMatrixExtension.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The precise two-factor matrix-automorphism extension input.

def OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugateLetter line 19
Source documentation
Algebraic conjugation of a letter in the other factor.
```
def matrixConjugateLetter (c : D) : D :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugateLetter_one line 22
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugateLetter_mul line 26
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugateLetter_inv line 31
theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_matrixConjugateLetter line 35
def OAI.KadisonSimilarity.TracialCornerGeometry.MatrixConjugationExtensionInput line 54
Source documentation
The two-factor specialization of Blanchard--Dykema, Embeddings of reduced free products of operator algebras, Pacific J. Math. 199 (2001), 1--19, Theorem 3.7 (arXiv:math/9911012, p. 13). Applied to a tracial reduced free product, the identity embedding on the base factor and matrix conjugation on the other factor extend to a trace-preserving normal star homomorphism.
Only the algebraic extension and trace preservation are recorded here; no unitary implementation, completed-word covariance, or operator estimate is included. Normality is not needed for the L² construction.
```
def MatrixConjugationExtensionInput (A : StarSubalgebra ℂ P) : Prop :=
…
```