MatrixUnitFamilies.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Finite partial-isometry frames constructed from an actual unital matrix star homomorphism. No frame-existence assumption is used.

def OAI.KadisonSimilarity.embeddedMatrixUnit line 17
Source documentation
The image of an ordinary matrix unit in the ambient C-star algebra.
```
def embeddedMatrixUnit (ι : Matrix α α ℂ →⋆ₐ[ℂ] P) (i j : α) : P :=
…
```
theorem OAI.KadisonSimilarity.embeddedMatrixUnit_star line 20
theorem OAI.KadisonSimilarity.embeddedMatrixUnit_mul line 25
theorem OAI.KadisonSimilarity.embeddedMatrixUnit_isStarProjection line 37
Source documentation
Diagonal matrix units are actual star projections.
```
theorem embeddedMatrixUnit_isStarProjection (ι : Matrix α α ℂ →⋆ₐ[ℂ] P) (i : α) :
    IsStarProjection (embeddedMatrixUnit ι i i) := by
…
```
Mentions: OAI.KadisonSimilarity.embeddedMatrixUnit
theorem OAI.KadisonSimilarity.sum_embeddedMatrixUnit_diagonal line 45
Source documentation
The diagonal images resolve the unit because the embedding is unital.
```
theorem sum_embeddedMatrixUnit_diagonal (ι : Matrix α α ℂ →⋆ₐ[ℂ] P) :
    ∑ i : α, embeddedMatrixUnit ι i i = 1 := by
…
```
Mentions: OAI.KadisonSimilarity.embeddedMatrixUnit
structure OAI.KadisonSimilarity.MatrixUnitColumnFamily line 51
Source documentation
The precise finite-frame data consumed by full-column coordinates.
```
structure MatrixUnitColumnFamily (P α : Type*) [CStarAlgebra P]
    [Fintype α] [DecidableEq α] where
…
```
def OAI.KadisonSimilarity.matrixUnitColumnFamilyOfEmbedding line 62
Source documentation
Taking a single column of embedded matrix units supplies the full frame.
```
def matrixUnitColumnFamilyOfEmbedding (ι : Matrix α α ℂ →⋆ₐ[ℂ] P) (i₀ : α) :
    MatrixUnitColumnFamily P α where
…
```
Mentions: OAI.KadisonSimilarity.MatrixUnitColumnFamily
theorem OAI.KadisonSimilarity.matrixUnitColumnFamilyOfEmbedding_corner line 75
theorem OAI.KadisonSimilarity.matrixUnitColumnFamilyOfEmbedding_column line 79

theorem OAI.KadisonSimilarity.trace_embeddedMatrixUnit_diagonal line 85

Source documentation

Normalized trace preservation gives the reciprocal-dimension trace of all the diagonal projections, and hence of the chosen initial corner.

theorem trace_embeddedMatrixUnit_diagonal
    (τ : P →ₗ[ℂ] ℂ) (ι : Matrix α α ℂ →⋆ₐ[ℂ] P)
    (htrace : ∀ a, τ (ι a) = (Fintype.card α : ℂ)⁻¹ * Matrix.trace a) (i : α) :
    τ (embeddedMatrixUnit ι i i) = 1 / (Fintype.card α : ℂ) := by
…

Mentions: OAI.KadisonSimilarity.embeddedMatrixUnit

structure OAI.KadisonSimilarity.TracialMatrixUnitColumnFamily line 92
Source documentation
The frame together with the corner trace used in small-corner estimates.
```
structure TracialMatrixUnitColumnFamily (τ : P →ₗ[ℂ] ℂ) (α : Type*)
    [Fintype α] [DecidableEq α] extends MatrixUnitColumnFamily P α where
…
```
Mentions: OAI.KadisonSimilarity.MatrixUnitColumnFamily

def OAI.KadisonSimilarity.tracialMatrixUnitColumnFamilyOfEmbedding line 97

Source documentation

A trace-preserving unital matrix embedding supplies both frame and trace.

def tracialMatrixUnitColumnFamilyOfEmbedding
    (τ : P →ₗ[ℂ] ℂ) (ι : Matrix α α ℂ →⋆ₐ[ℂ] P)
    (htrace : ∀ a, τ (ι a) = (Fintype.card α : ℂ)⁻¹ * Matrix.trace a) (i₀ : α) :
    TracialMatrixUnitColumnFamily τ α where
…

Mentions: OAI.KadisonSimilarity.TracialMatrixUnitColumnFamily

def OAI.KadisonSimilarity.tracialMatrixUnitColumnFamilyOfNonempty line 106
Source documentation
A nonempty finite matrix index type provides a distinguished corner without an additional choice of frame data.
```
def tracialMatrixUnitColumnFamilyOfNonempty [Nonempty α]
    (τ : P →ₗ[ℂ] ℂ) (ι : Matrix α α ℂ →⋆ₐ[ℂ] P)
    (htrace : ∀ a, τ (ι a) = (Fintype.card α : ℂ)⁻¹ * Matrix.trace a) :
    TracialMatrixUnitColumnFamily τ α :=
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixUnitColumnFamily
def OAI.KadisonSimilarity.MatrixUnitColumnFamily.reindex line 117
Source documentation
Relabeling a finite frame preserves its initial projection and resolution.
```
def reindex (F : MatrixUnitColumnFamily P α) (e : β ≃ α) : MatrixUnitColumnFamily P β where
…
```
Mentions: OAI.KadisonSimilarity.MatrixUnitColumnFamily
theorem OAI.KadisonSimilarity.MatrixUnitColumnFamily.reindex_corner line 126
theorem OAI.KadisonSimilarity.MatrixUnitColumnFamily.reindex_column line 129
def OAI.KadisonSimilarity.TracialMatrixUnitColumnFamily.reindex line 139
Source documentation
The normalized corner trace is preserved when a finite frame is relabeled.
```
def reindex (F : TracialMatrixUnitColumnFamily τ α) (e : β ≃ α) :
    TracialMatrixUnitColumnFamily τ β where
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixUnitColumnFamily
def OAI.KadisonSimilarity.NestedTracialMatrices.columnFamily line 156
Source documentation
Each actual tracial matrix stage supplies its finite corner frame.
```
def NestedTracialMatrices.columnFamily (M : NestedTracialMatrices (A := A) τ V)
…
```
Mentions: OAI.KadisonSimilarity.NestedTracialMatrices
def OAI.KadisonSimilarity.NestedTracialMatrices.finColumnFamily line 162
Source documentation
The same actual frame on Fin(card(A s)), as required by finite Hilbert amplification and the full-column coordinate construction.
```
def NestedTracialMatrices.finColumnFamily (M : NestedTracialMatrices (A := A) τ V)
…
```
Mentions: OAI.KadisonSimilarity.NestedTracialMatrices
theorem OAI.KadisonSimilarity.NestedTracialMatrices.finColumnFamily_corner line 166
theorem OAI.KadisonSimilarity.NestedTracialMatrices.finColumnFamily_column line 170
theorem OAI.KadisonSimilarity.NestedTracialMatrices.finColumnFamily_base line 176
def OAI.KadisonSimilarity.NestedTracialMatrices.nonemptyFinColumnFamily line 182
Source documentation
A nonempty stage gives the finite amplification frame without any additional existence hypothesis.
```
def NestedTracialMatrices.nonemptyFinColumnFamily [∀ s, Nonempty (A s)]
    (M : NestedTracialMatrices (A := A) τ V) (s : ℕ) :
…
```
Mentions: OAI.KadisonSimilarity.NestedTracialMatrices