CompatibleMatrixFrames.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Compatible finite groups for an increasing matrix chain

The finite index set is retained as data, so tensor refinements do not require changing the represented operators or reindexing to a fixed type.

structure OAI.KadisonKastler.FullMatrixFrame line 21
Source documentation
A full matrix system for a concrete algebra, with a finite nonempty index.
```
structure FullMatrixFrame (A : StarSubalgebra ℂ (H →L[ℂ] H)) where
…
```
instance OAI.KadisonKastler.FullMatrixFrame.index_nonempty line 35
def OAI.KadisonKastler.FullMatrixFrame.ambientUnits line 37
def OAI.KadisonKastler.FullMatrixFrame.group line 40
instance OAI.KadisonKastler.FullMatrixFrame.group_finite line 43
theorem OAI.KadisonKastler.FullMatrixFrame.ambientUnits_algebra line 46
theorem OAI.KadisonKastler.FullMatrixFrame.group_mem line 60
theorem OAI.KadisonKastler.FullMatrixFrame.commutes_of_group line 67
Source documentation
The represented finite group determines the full matrix commutant.
```
theorem commutes_of_group (F : FullMatrixFrame A) (T : H →L[ℂ] H)
    (hT : ∀ u : F.group, Commute (u : H →L[ℂ] H) T) :
    ∀ a ∈ A, Commute a T := by
…
```
Mentions: OAI.KadisonKastler.FullMatrixFrame
def OAI.KadisonKastler.FullMatrixFrame.ofUnits line 79
Source documentation
A full matrix frame is obtained from a specified matrix-unit range.
```
def ofUnits {ι : Type} [Fintype ι] [DecidableEq ι]
    (E : Generator.MatrixUnitSystem ι (H →L[ℂ] H)) (o : ι) : FullMatrixFrame E.algebra := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.FullMatrixFrame
theorem OAI.KadisonKastler.FullMatrixFrame.exists_refinement line 104
Source documentation
Refine a frame inside a larger full matrix algebra while retaining the actual ambient finite group.
```
theorem exists_refinement (E : FullMatrixFrame A) (P : FullMatrixFrame B) (hAB : A ≤ B) :
    ∃ F : FullMatrixFrame B, E.group ≤ F.group := by
…
```
Mentions: OAI.KadisonKastler.FullMatrixFrame

def OAI.KadisonKastler.compatibleMatrixFrames line 124

Source documentation

Choose compatible frames without changing any algebra in the chain.

def compatibleMatrixFrames (F : ∀ n, FullMatrixFrame (A n)) (hA : Monotone A) :
    ∀ n, FullMatrixFrame (A n)
  | 0 => F 0
  | n + 1 => Classical.choose
      (FullMatrixFrame.exists_refinement (compatibleMatrixFrames F hA n) (F (n + 1))
        (hA (Nat.le_succ n)))

Mentions: OAI.KadisonKastler.FullMatrixFrame, OAI.KadisonKastler.FullMatrixFrame.exists_refinement

theorem OAI.KadisonKastler.compatibleMatrixFrames_group_monotone line 131