FreeProductAutomorphisms.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Algebraic extensions become actual automorphisms by tracial L² density. The only extension input is the two-factor published embedding specialization.

def OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra line 18
Source documentation
The bounded factor algebra, before taking its tracial L² closure.
```
def factorAlgebra (A D : StarSubalgebra ℂ P) : StarSubalgebra ℂ P :=
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.FactorsTraciallyGenerate line 23
Source documentation
Ordinary tracial generation by the two factors. This is geometric density of algebra vectors, independent of any operator intertwining statement.
```
def FactorsTraciallyGenerate (A D : StarSubalgebra ℂ P) : Prop :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.hom_vector_norm line 28
Source documentation
A trace-preserving homomorphism is isometric on the tracial algebra vectors.
```
theorem hom_vector_norm (Φ : P →⋆ₐ[ℂ] P)
    (hΦ : ∀ a, G.trace (Φ a) = G.trace a) (a : P) :
    ‖G.vector (Φ a)‖ = ‖G.vector a‖ := by
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.homIsometry line 36
Source documentation
The actual L² isometry of a trace-preserving ambient homomorphism.
```
def homIsometry (Φ : P →⋆ₐ[ℂ] P) (hΦ : ∀ a, G.trace (Φ a) = G.trace a) :
    H →ₗᵢ[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.homIsometry_vector line 41

theorem OAI.KadisonSimilarity.TracialCornerGeometry.hom_eq_of_factor_eq line 48

Source documentation

Trace preservation turns tracial generation into uniqueness of ambient extensions of the two factor maps.

theorem hom_eq_of_factor_eq (A D : StarSubalgebra ℂ P)
    (hgen : G.FactorsTraciallyGenerate A D) (hfaithful : Function.Injective G.vector)
    (Φ Ψ : P →⋆ₐ[ℂ] P)
    (hΦ : ∀ a, G.trace (Φ a) = G.trace a)
    (hΨ : ∀ a, G.trace (Ψ a) = G.trace a)
    (hA : ∀ a : A, Φ (a : P) = Ψ (a : P))
    (hD : ∀ d : D, Φ (d : P) = Ψ (d : P)) : Φ = Ψ := by
…

def OAI.KadisonSimilarity.TracialCornerGeometry.chosenMatrixExtension line 82
Source documentation
A choice of the published algebraic extension, with no unitary or tensor conclusion included in that input.
```
def chosenMatrixExtension (u : Matrix.unitaryGroup α ℂ) : P →⋆ₐ[ℂ] P :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.chosenMatrixExtension_trace line 85
theorem OAI.KadisonSimilarity.TracialCornerGeometry.chosenMatrixExtension_base line 89
theorem OAI.KadisonSimilarity.TracialCornerGeometry.chosenMatrixExtension_other line 93
theorem OAI.KadisonSimilarity.TracialCornerGeometry.chosenMatrixExtension_inv_comp line 101
Source documentation
The inverse factor conjugations give inverse ambient homomorphisms by tracial generation; no ambient automorphism existence is assumed.
```
theorem chosenMatrixExtension_inv_comp (u : Matrix.unitaryGroup α ℂ) :
    (G.chosenMatrixExtension A D ι hext u⁻¹).comp
      (G.chosenMatrixExtension A D ι hext u) = StarAlgHom.id ℂ P := by
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionAutomorphism line 118
Source documentation
The actual ambient automorphism is derived from the two inverse published factor embeddings.
```
def matrixExtensionAutomorphism (u : Matrix.unitaryGroup α ℂ) : P ≃⋆ₐ[ℂ] P :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionAutomorphism_apply line 126
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionAutomorphism_trace line 130
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionAutomorphism_base line 134
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionAutomorphism_other line 138
theorem OAI.KadisonSimilarity.TracialCornerGeometry.chosenMatrixExtension_one line 144
theorem OAI.KadisonSimilarity.TracialCornerGeometry.chosenMatrixExtension_mul line 156
def OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionAction line 173
Source documentation
The ambient extensions form a genuine group action, by uniqueness on the tracially dense generated algebra.
```
def matrixExtensionAction : Matrix.unitaryGroup α ℂ →* (P ≃⋆ₐ[ℂ] P) where
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionUnitaryRepresentation line 191
Source documentation
The actual Hilbert-space unitary representation induced by the derived free-product automorphisms.
```
def matrixExtensionUnitaryRepresentation :
    Matrix.unitaryGroup α ℂ →* unitary (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionUnitaryRepresentation_vector line 196
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionUnitaryRepresentation_base line 207
Source documentation
The constructed matrix action fixes the whole completed base space, by the algebraic fixation of its dense bounded vectors.
```
theorem matrixExtensionUnitaryRepresentation_base
    (u : Matrix.unitaryGroup α ℂ) (x : G.baseSpace A) :
    (G.matrixExtensionUnitaryRepresentation A D ι hgen hfaithful hext u : H →L[ℂ] H)
      (x : H) = (x : H) := by
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixExtensionUnitaryRepresentation_left line 218

Source documentation

The represented ambient left action transforms under the actual matrix-conjugation automorphism on all Hilbert vectors.

theorem matrixExtensionUnitaryRepresentation_left
    (u : Matrix.unitaryGroup α ℂ) (a : P) (x : H) :
    (G.matrixExtensionUnitaryRepresentation A D ι hgen hfaithful hext u : H →L[ℂ] H)
      (G.left a x) =
    G.left (G.chosenMatrixExtension A D ι hext u a)
      ((G.matrixExtensionUnitaryRepresentation A D ι hgen hfaithful hext u : H →L[ℂ] H) x) := by
…