TracialMatrixRealization.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Matrix stages inside an actual tracial Hilbert representation

A trace-preserving matrix embedding supplies the normalized Hilbert--Schmidt geometry, the corner left action, and the centered projection used by the invariant-intertwiner argument. No invariant-theory conclusion is an input.

abbrev OAI.KadisonSimilarity.centeredSubspace line 22
Source documentation
The centered subspace is the orthogonal complement of the trace vector.
```
abbrev centeredSubspace (Ω : E) : Submodule ℂ E := (ℂ ∙ Ω)ᗮ
```
def OAI.KadisonSimilarity.tracialCenter line 25
Source documentation
Center a represented algebra vector by its actual orthogonal projection.
```
def tracialCenter (V : R →ₗ[ℂ] E) : R →ₗ[ℂ] centeredSubspace (V 1) :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.tracialCenter_apply line 29
theorem OAI.KadisonSimilarity.norm_tracialCenter_le line 34
Source documentation
Centering is contractive in the represented Hilbert norm.
```
theorem norm_tracialCenter_le (V : R →ₗ[ℂ] E) (a : R) :
    ‖tracialCenter V a‖ ≤ ‖V a‖ :=
…
```
Mentions: OAI.KadisonSimilarity.tracialCenter
theorem OAI.KadisonSimilarity.tracialCenter_one line 39
theorem OAI.KadisonSimilarity.denseRange_tracialCenter line 44
Source documentation
Density of the represented algebra passes to its centered projection.
```
theorem denseRange_tracialCenter (V : R →ₗ[ℂ] E) (hdense : DenseRange V) :
    DenseRange (tracialCenter V) := by
…
```
Mentions: OAI.KadisonSimilarity.tracialCenter
theorem OAI.KadisonSimilarity.tracialCenter_sub_trace line 55
Source documentation
Subtracting the trace creates an algebraic trace-zero vector and does not change its centered projection.
```
theorem tracialCenter_sub_trace (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E) (a : R) :
    tracialCenter V (a - τ a • 1) = tracialCenter V a := by
…
```
Mentions: OAI.KadisonSimilarity.tracialCenter
theorem OAI.KadisonSimilarity.trace_sub_trace line 60

theorem OAI.KadisonSimilarity.tracial_vector_mem_centered line 66

Source documentation

Trace-zero algebra vectors already lie in the centered subspace.

theorem tracial_vector_mem_centered (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E)
    (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b))
    (a : R) (ha : τ a = 0) : V a ∈ centeredSubspace (V 1) := by
…

Mentions: OAI.KadisonSimilarity.centeredSubspace

theorem OAI.KadisonSimilarity.coe_tracialCenter_of_trace_zero line 75
Source documentation
Inserting a centered trace-zero vector back into the full Hilbert space recovers the original vector exactly.
```
theorem coe_tracialCenter_of_trace_zero (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E)
    (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b))
    (a : R) (ha : τ a = 0) : (tracialCenter V a : E) = V a := by
…
```
Mentions: OAI.KadisonSimilarity.tracialCenter

theorem OAI.KadisonSimilarity.coe_tracialCenter line 83

Source documentation

Orthogonal centering is precisely subtraction of the trace component.

theorem coe_tracialCenter (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E)
    (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b)) (hτ : τ 1 = 1)
    (a : R) : (tracialCenter V a : E) = V a - τ a • V 1 := by
…

Mentions: OAI.KadisonSimilarity.tracialCenter

theorem OAI.KadisonSimilarity.norm_tracialTraceVector line 93

Source documentation

A normalized trace gives the required unit trace vector.

theorem norm_tracialTraceVector (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E)
    (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b)) (hτ : τ 1 = 1) :
    ‖V 1‖ = 1 := by
…

def OAI.KadisonSimilarity.tracialMatrixStage line 103

Source documentation

The concrete normalized matrix stage associated to a trace-preserving matrix star homomorphism and the left tracial representation.

def tracialMatrixStage
    (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E) (L : R →⋆ₐ[ℂ] (E →L[ℂ] E))
    (ι : Matrix α α ℂ →⋆ₐ[ℂ] R)
    (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b))
    (hleft : ∀ a b, L a (V b) = V (a * b))
    (htrace : ∀ a, τ (ι a) = (Fintype.card α : ℂ)⁻¹ * Matrix.trace a) :
    MatrixHilbertStage (E := E) (F := centeredSubspace (V 1)) (α := α) where
…

Mentions: OAI.KadisonSimilarity.MatrixHilbertStage, OAI.KadisonSimilarity.centeredSubspace

theorem OAI.KadisonSimilarity.tracialMatrixStage_full line 124
theorem OAI.KadisonSimilarity.tracialMatrixStage_unit line 131

theorem OAI.KadisonSimilarity.coe_tracialMatrixStage_center_of_trace_zero line 141

Source documentation

The stage centering acts as the identity on trace-zero matrices after including its value in the full Hilbert space.

theorem coe_tracialMatrixStage_center_of_trace_zero
    (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E) (L : R →⋆ₐ[ℂ] (E →L[ℂ] E))
    (ι : Matrix α α ℂ →⋆ₐ[ℂ] R) (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b))
    (hleft : ∀ a b, L a (V b) = V (a * b))
    (htrace : ∀ a, τ (ι a) = (Fintype.card α : ℂ)⁻¹ * Matrix.trace a)
    (a : Matrix α α ℂ) (ha : Matrix.trace a = 0) :
    ((tracialMatrixStage τ V L ι hinner hleft htrace).center a : E) = V (ι a) := by
…

Mentions: OAI.KadisonSimilarity.tracialMatrixStage

theorem OAI.KadisonSimilarity.inner_tracialMatrixStage_center line 154

Source documentation

Thus the centered trace-zero matrix vectors have the actual normalized Hilbert--Schmidt inner product.

theorem inner_tracialMatrixStage_center
    (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E) (L : R →⋆ₐ[ℂ] (E →L[ℂ] E))
    (ι : Matrix α α ℂ →⋆ₐ[ℂ] R) (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b))
    (hleft : ∀ a b, L a (V b) = V (a * b))
    (htrace : ∀ a, τ (ι a) = (Fintype.card α : ℂ)⁻¹ * Matrix.trace a)
    (a b : Matrix α α ℂ) (ha : Matrix.trace a = 0) (hb : Matrix.trace b = 0) :
    inner ℂ ((tracialMatrixStage τ V L ι hinner hleft htrace).center a)
      ((tracialMatrixStage τ V L ι hinner hleft htrace).center b) =
      (Fintype.card α : ℂ)⁻¹ * Matrix.trace (star a * b) := by
…

Mentions: OAI.KadisonSimilarity.tracialMatrixStage

theorem OAI.KadisonSimilarity.norm_tracial_star line 182
Source documentation
The tracial identity makes algebraic involution isometric in the represented Hilbert norm, even before a norm on the algebra has been specified.
```
theorem norm_tracial_star (a : R) : ‖V (star a)‖ = ‖V a‖ := by
…
```
def OAI.KadisonSimilarity.tracialConjugation line 190
Source documentation
The actual tracial conjugation is obtained by extending algebraic involution from the dense represented algebra.
```
def tracialConjugation : E →ₗᵢ⋆[ℂ] E :=
…
```
theorem OAI.KadisonSimilarity.tracialConjugation_apply_vector line 194
theorem OAI.KadisonSimilarity.tracialConjugation_traceVector line 199
theorem OAI.KadisonSimilarity.tracialConjugation_involutive line 204
Source documentation
The dense extension remains an involution.
```
theorem tracialConjugation_involutive :
    Function.Involutive (tracialConjugation τ V hinner htrace hdense) := by
…
```
Mentions: OAI.KadisonSimilarity.tracialConjugation

theorem OAI.KadisonSimilarity.inner_tracialConjugation line 212

Source documentation

Tracial conjugation reverses the Hilbert inner product.

theorem inner_tracialConjugation (x y : E) :
    inner ℂ (tracialConjugation τ V hinner htrace hdense x)
      (tracialConjugation τ V hinner htrace hdense y) = inner ℂ y x := by
…

Mentions: OAI.KadisonSimilarity.tracialConjugation

theorem OAI.KadisonSimilarity.tracialConjugation_mem_centered line 222
Source documentation
The trace-vector orthogonal complement is stable under actual tracial conjugation.
```
theorem tracialConjugation_mem_centered (x : centeredSubspace (V 1)) :
    tracialConjugation τ V hinner htrace hdense x ∈ centeredSubspace (V 1) := by
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.tracialConjugation
def OAI.KadisonSimilarity.centeredTracialConjugation line 233
Source documentation
Tracial conjugation restricted to the centered Hilbert space.
```
def centeredTracialConjugation :
    centeredSubspace (V 1) →ₗᵢ⋆[ℂ] centeredSubspace (V 1) where
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.coe_centeredTracialConjugation line 245
theorem OAI.KadisonSimilarity.centeredTracialConjugation_involutive line 249
def OAI.KadisonSimilarity.centeredTracialPairing line 257
Source documentation
The continuous bilinear pairing used for matrix trace contractions is built from the actual centered tracial conjugation.
```
def centeredTracialPairing :
    centeredSubspace (V 1) →L[ℂ] centeredSubspace (V 1) →L[ℂ] ℂ :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.centeredTracialPairing_conjugation line 262

theorem OAI.KadisonSimilarity.centeredTracialPairing_matrix line 269

Source documentation

On centered matrix vectors the pairing is exactly the normalized matrix trace, without an assumed pairing formula.

theorem centeredTracialPairing_matrix
    (L : R →⋆ₐ[ℂ] (E →L[ℂ] E)) (ι : Matrix α α ℂ →⋆ₐ[ℂ] R)
    (hleft : ∀ a b, L a (V b) = V (a * b))
    (hι : ∀ a, τ (ι a) = (Fintype.card α : ℂ)⁻¹ * Matrix.trace a)
    (a b : Matrix α α ℂ) (ha : Matrix.trace a = 0) (hb : Matrix.trace b = 0) :
    centeredTracialPairing τ V hinner htrace hdense
      ((tracialMatrixStage τ V L ι hinner hleft hι).center a)
      ((tracialMatrixStage τ V L ι hinner hleft hι).center b) =
      (Fintype.card α : ℂ)⁻¹ * Matrix.trace (a * b) := by
…

Mentions: OAI.KadisonSimilarity.centeredTracialPairing, OAI.KadisonSimilarity.tracialMatrixStage