FiniteCornerGeneration.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Matrix entries generated by the finite corner groups

theorem OAI.KadisonKastler.FullMatrixCorner.scalarBlockHom_single line 22

theorem OAI.KadisonKastler.FullMatrixCorner.finiteSignedRepresentation_reflection line 28

Source documentation

A single sign reflection isolates a diagonal matrix projection.

theorem finiteSignedRepresentation_reflection {n : ℕ} (i : Fin n) :
    (F.finiteSignedRepresentation n
      (SemidirectProduct.inl (Function.update (1 : Fin n → ℤˣ) i (-1))) : H →L[ℂ] H) =
      1 - (2 : ℂ) • F.entry i i := by
…

theorem OAI.KadisonKastler.FullMatrixCorner.entry_scalarBlock_sandwich line 57

theorem OAI.KadisonKastler.FullMatrixCorner.entry_finiteSigned_sandwich line 65

Source documentation

Sandwiching any finite group element recovers its matrix coefficient.

theorem entry_finiteSigned_sandwich {n : ℕ} (i j : Fin n) (g : SignedPermutation (Fin n)) :
    F.entry i i * (F.finiteSignedRepresentation n g : H →L[ℂ] H) * F.entry j j =
      (signedPermutationHom g : Matrix (Fin n) (Fin n) ℂ) i j • F.entry i j := by
…

Mentions: OAI.KadisonKastler.SignedPermutation, OAI.KadisonKastler.signedPermutationHom

theorem OAI.KadisonKastler.FullMatrixCorner.entries_mem_of_finiteSigned line 83
Source documentation
Containing the finite signed groups forces containment of all countable matrix entries.
```
theorem entries_mem_of_finiteSigned (Q : VonNeumannAlgebra H)
    (hQ : ∀ n (g : SignedPermutation (Fin n)),
      (F.finiteSignedRepresentation n g : H →L[ℂ] H) ∈ Q) :
    ∀ i j, F.entry i j ∈ Q := by
…
```
Mentions: OAI.KadisonKastler.SignedPermutation