FiniteMatrixPolar.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Actual unitary polar decompositions in finite matrix models

The scalar algebra is represented on the one-dimensional Hilbert space. The proved matrix-von-Neumann bridge supplies concrete representations of its finite matrix amplifications. Finite faithful trace and scalar center then give the unitary polar decomposition.

def OAI.KadisonKastler.coefficientMatrixEquiv line 24
Source documentation
Entrywise transport along a star-algebra equivalence.
```
def coefficientMatrixEquiv (e : A ≃⋆ₐ[ℂ] B) : CStarMatrix ι ι A ≃⋆ₐ[ℂ] CStarMatrix ι ι B :=
…
```
theorem OAI.KadisonKastler.coefficientMatrixEquiv_apply line 39
def OAI.KadisonKastler.matrixRepresentationEquiv line 46
Source documentation
Amplify a concrete representation by a finite matrix algebra.
```
def matrixRepresentationEquiv (e : A ≃⋆ₐ[ℂ] Algebra M) :
    CStarMatrix ι ι A ≃⋆ₐ[ℂ] Algebra (matrixVonNeumann (ι := ι) M) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann

theorem OAI.KadisonKastler.scalar_center_equiv line 51

Source documentation

Scalar center transports along any star equivalence.

theorem scalar_center_equiv (e : A ≃⋆ₐ[ℂ] B)
    (hA : ∀ a : A, (∀ b : A, b * a = a * b) → ∃ z : ℂ, a = z • (1 : A))
    (b : B) (hb : ∀ c : B, c * b = b * c) : ∃ z : ℂ, b = z • (1 : B) := by
…

theorem OAI.KadisonKastler.unitary_polar_of_representation line 75
Source documentation
The finite-factor polar theorem needs a concrete von Neumann representation, scalar center, and finite faithful trace; no diffuseness.
```
theorem unitary_polar_of_representation (e : A ≃⋆ₐ[ℂ] Algebra M)
    (τ : FaithfulTracialState A)
    (hA : ∀ a : A, (∀ b : A, b * a = a * b) → ∃ z : ℂ, a = z • (1 : A))
    (x : A) : ∃ u : unitary A, (u : A) * CFC.abs x = x := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.scalarVonNeumann line 94
Source documentation
The full operator algebra on the one-dimensional Hilbert space.
```
def scalarVonNeumann : VonNeumannAlgebra ℂ where
…
```
theorem OAI.KadisonKastler.scalar_ofId_apply line 98
def OAI.KadisonKastler.scalarRepresentation line 104
Source documentation
Multiplication on C identifies it with its full bounded-operator algebra.
```
def scalarRepresentation : ℂ ≃⋆ₐ[ℂ] Algebra scalarVonNeumann :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.scalarVonNeumann
def OAI.KadisonKastler.finiteMatrixRepresentation line 123
Source documentation
The concrete Hilbert-space representation of each nested finite matrix model.
```
def finiteMatrixRepresentation (n j : ℕ) : FiniteMatrixModel n j ≃⋆ₐ[ℂ]
    Algebra (matrixVonNeumann (ι := Fin n)
…
```
Mentions: OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.finiteMatrixModel_scalar_center line 128
theorem OAI.KadisonKastler.finiteMatrixModel_unitary_polar line 152
Source documentation
Every element of the actual finite-matrix coordinate has a unitary polar factor; the statement supplies the hypothesis used for varying lifts.
```
theorem finiteMatrixModel_unitary_polar (n j : ℕ) [NeZero n] (x : FiniteMatrixModel n j) :
    ∃ u : unitary (FiniteMatrixModel n j), (u : FiniteMatrixModel n j) * CFC.abs x = x :=
…
```
Mentions: OAI.KadisonKastler.FiniteMatrixModel