NormalizedContractions.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Naturality of normalized permutation contractions under trace-preserving matrix algebra maps, proved by deleting one permutation vertex at a time.

def OAI.KadisonSimilarity.insertPermutationVertex line 20
Source documentation
Insert one new vertex after b in its permutation cycle.
```
def insertPermutationVertex (p : Equiv.Perm ι) (b : ι) : Equiv.Perm (Option ι) :=
…
```
theorem OAI.KadisonSimilarity.insertPermutationVertex_none line 24
theorem OAI.KadisonSimilarity.insertPermutationVertex_self line 29
theorem OAI.KadisonSimilarity.insertPermutationVertex_other line 34
def OAI.KadisonSimilarity.insertedCycleLabelingsEquiv line 40
Source documentation
Removing an inserted vertex preserves the set of cycle-constant labels.
```
def insertedCycleLabelingsEquiv (p : Equiv.Perm ι) (b : ι) (β : Type*) :
    CycleConstantLabelings (insertPermutationVertex p b) β ≃ CycleConstantLabelings p β where
…
```
Mentions: OAI.KadisonSimilarity.CycleConstantLabelings, OAI.KadisonSimilarity.insertPermutationVertex
def OAI.KadisonSimilarity.fixedCycleLabelingsEquiv line 73
Source documentation
A new fixed point contributes an independent constant label.
```
def fixedCycleLabelingsEquiv (p : Equiv.Perm ι) (β : Type*) :
    CycleConstantLabelings p.optionCongr β ≃ β × CycleConstantLabelings p β where
…
```
Mentions: OAI.KadisonSimilarity.CycleConstantLabelings
theorem OAI.KadisonSimilarity.permutationCycleCount_insert line 87
theorem OAI.KadisonSimilarity.permutationCycleCount_optionCongr line 93
def OAI.KadisonSimilarity.splicePermutationWord line 103
Source documentation
Splicing two adjacent slots multiplies their matrix arguments in cycle order.
```
def splicePermutationWord (v : Option ι → Matrix α α ℂ) (b : ι) : ι → Matrix α α ℂ :=
…
```

theorem OAI.KadisonSimilarity.permutationContraction_optionCongr line 108

Source documentation

A fixed vertex contributes the ordinary matrix trace.

theorem permutationContraction_optionCongr (p : Equiv.Perm ι)
    (v : Option ι → Matrix α α ℂ) :
    permutationContraction p.optionCongr v =
      Matrix.trace (v none) * permutationContraction p (fun i => v (some i)) := by
…

Mentions: OAI.KadisonSimilarity.permutationContraction

theorem OAI.KadisonSimilarity.permutationContraction_insert line 125
Source documentation
Summing the label at an inserted nonfixed vertex is matrix multiplication.
```
theorem permutationContraction_insert (p : Equiv.Perm ι) (b : ι)
    (v : Option ι → Matrix α α ℂ) :
    permutationContraction (insertPermutationVertex p b) v =
      permutationContraction p (splicePermutationWord v b) := by
…
```
Mentions: OAI.KadisonSimilarity.permutationContraction, OAI.KadisonSimilarity.insertPermutationVertex, OAI.KadisonSimilarity.splicePermutationWord

theorem OAI.KadisonSimilarity.normalizedPermutationContraction_optionCongr line 164

Source documentation

Normalized fixed-point deletion carries precisely one normalized trace.

theorem normalizedPermutationContraction_optionCongr (p : Equiv.Perm ι)
    (v : Option ι → Matrix α α ℂ) :
    normalizedPermutationContraction p.optionCongr v =
      ((Fintype.card α : ℂ)⁻¹ * Matrix.trace (v none)) *
        normalizedPermutationContraction p (fun i => v (some i)) := by
…

Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction

theorem OAI.KadisonSimilarity.normalizedPermutationContraction_insert line 175
Source documentation
Insertion into an existing cycle adds no trace-normalization factor.
```
theorem normalizedPermutationContraction_insert (p : Equiv.Perm ι) (b : ι)
    (v : Option ι → Matrix α α ℂ) :
    normalizedPermutationContraction (insertPermutationVertex p b) v =
      normalizedPermutationContraction p (splicePermutationWord v b) := by
…
```
Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.insertPermutationVertex, OAI.KadisonSimilarity.splicePermutationWord
def OAI.KadisonSimilarity.reindexedCycleLabelingsEquiv line 185
Source documentation
Vertex reindexing does not change cycle-constant labels.
```
def reindexedCycleLabelingsEquiv (e : ι ≃ κ) (p : Equiv.Perm ι) (β : Type*) :
    CycleConstantLabelings (e.permCongr p) β ≃ CycleConstantLabelings p β where
…
```
Mentions: OAI.KadisonSimilarity.CycleConstantLabelings
theorem OAI.KadisonSimilarity.permutationCycleCount_permCongr line 202
theorem OAI.KadisonSimilarity.permutationContraction_permCongr line 209
theorem OAI.KadisonSimilarity.normalizedPermutationContraction_permCongr line 221

theorem OAI.KadisonSimilarity.normalizedPermutationContraction_map line 230

Source documentation

Normalized permutation contractions are natural for every trace-preserving unital matrix algebra map; no normal-form hypothesis on that map is needed.

theorem normalizedPermutationContraction_map
    [Fintype β] [DecidableEq β]
    (φ : Matrix α α ℂ →ₐ[ℂ] Matrix β β ℂ)
    (htrace : ∀ a, (Fintype.card β : ℂ)⁻¹ * Matrix.trace (φ a) =
      (Fintype.card α : ℂ)⁻¹ * Matrix.trace a)
    (p : Equiv.Perm ι) (v : ι → Matrix α α ℂ) :
      normalizedPermutationContraction p (fun i => φ (v i)) =
      normalizedPermutationContraction p v := by
…

Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction

theorem OAI.KadisonSimilarity.NestedTracialMatrices.normalizedPermutationContraction_inclusion line 301
Source documentation
The stable-stage contraction compatibility follows from the raw tracial matrix inclusions and is not an additional tensor-classification hypothesis.
```
theorem NestedTracialMatrices.normalizedPermutationContraction_inclusion
    (M : NestedTracialMatrices (A := A) τ V) (s t : ℕ) (h : s ≤ t)
…
```
Mentions: OAI.KadisonSimilarity.NestedTracialMatrices