FiniteCornerGroups.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Finite signed groups in a countable matrix corner

Each finite group acts on the first finitely many matrix summands and as the identity on their orthogonal complement.

theorem OAI.KadisonKastler.FullMatrixCorner.blockElement_scalar line 25
def OAI.KadisonKastler.FullMatrixCorner.scalarBlockHom line 31
Source documentation
The scalar finite-block representation before adjoining the complement.
```
def scalarBlockHom (n : ℕ) : CStarMatrix (Fin n) (Fin n) ℂ →⋆ₙₐ[ℂ] (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.scalarBlockHom_apply line 35
theorem OAI.KadisonKastler.FullMatrixCorner.scalarBlockHom_one line 41
def OAI.KadisonKastler.FullMatrixCorner.signedCStarRepresentation line 49
Source documentation
The signed matrix representation with the C-star matrix type explicit.
```
def signedCStarRepresentation (n : ℕ) : SignedPermutation (Fin n) →*
    unitary (CStarMatrix (Fin n) (Fin n) ℂ) where
…
```
Mentions: OAI.KadisonKastler.SignedPermutation
def OAI.KadisonKastler.FullMatrixCorner.finiteSignedRepresentation line 61
Source documentation
The actual ambient representation of the finite signed-permutation group.
```
def finiteSignedRepresentation (n : ℕ) : SignedPermutation (Fin n) →*
    unitary (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonKastler.SignedPermutation
def OAI.KadisonKastler.FullMatrixCorner.finiteSignedGroup line 67
Source documentation
Its range is a finite subgroup of the ambient unitary group.
```
def finiteSignedGroup (n : ℕ) : Subgroup (unitary (H →L[ℂ] H)) :=
…
```
instance OAI.KadisonKastler.FullMatrixCorner.finiteSignedGroup_finite line 70
theorem OAI.KadisonKastler.FullMatrixCorner.finiteSignedRepresentation_apply line 73

theorem OAI.KadisonKastler.FullMatrixCorner.finiteSignedRepresentation_diagonal line 82

Source documentation

Diagonal signed elements, with identity on the complementary summands.

theorem finiteSignedRepresentation_diagonal (n : ℕ) (d : Fin n → ℤˣ) :
    (F.finiteSignedRepresentation n (SemidirectProduct.inl d) : H →L[ℂ] H) =
      (∑ i : Fin n, ((d i : ℤ) : ℂ) • F.entry i i) +
        (1 - F.partialDiagonal (Finset.range n)) := by
…

theorem OAI.KadisonKastler.FullMatrixCorner.finiteSignedRepresentation_permutation line 94

Source documentation

Permutations of the finite block, with identity on its complement.

theorem finiteSignedRepresentation_permutation (n : ℕ) (σ : Equiv.Perm (Fin n)) :
    (F.finiteSignedRepresentation n (SemidirectProduct.inr σ) : H →L[ℂ] H) =
      (∑ i : Fin n, F.entry (σ i) i) + (1 - F.partialDiagonal (Finset.range n)) := by
…

theorem OAI.KadisonKastler.FullMatrixCorner.finiteSignedGroup_mem line 108

Source documentation

The finite signed groups stay in every algebra containing the original entries.

theorem finiteSignedGroup_mem (M : VonNeumannAlgebra H)
    (hF : ∀ i j, F.entry i j ∈ M) (n : ℕ) (u : F.finiteSignedGroup n) :
    (u : H →L[ℂ] H) ∈ M := by
…