SpectralJordanMap.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Jordan structure of a unitary-preserving map on a von Neumann algebra

Projection phases give exact algebraic identities on finite spectral sums. Norm approximation by those sums then gives adjoint and square preservation; complex polarization gives the Jordan identity.

theorem OAI.KadisonKastler.orthogonal_sum_square line 23

theorem OAI.KadisonKastler.map_star_square_projection_sum line 41

Source documentation

Finite spectral sums retain adjoints and squares under the map.

theorem map_star_square_projection_sum {I : Type*} [Fintype I]
    (F : A →ₗ[ℂ] B) (hF1 : F 1 = 1)
    (hFu : ∀ u : unitary A, F u ∈ unitary B)
    (p : I → A) (c : I → ℂ) (hp : ∀ i, IsStarProjection (p i))
    (hpq : ∀ i j, i ≠ j → p i * p j = 0) :
    F (star (∑ i, c i • p i)) = star (F (∑ i, c i • p i)) ∧
      F ((∑ i, c i • p i) * (∑ i, c i • p i)) =
        F (∑ i, c i • p i) * F (∑ i, c i • p i) := by
…

theorem OAI.KadisonKastler.map_star_square_normal_of_map_unitary line 71

Source documentation

Normal elements are norm limits of finite spectral sums, so both identities extend by continuity.

theorem map_star_square_normal_of_map_unitary
    (F : Algebra M →L[ℂ] B) (hF1 : F 1 = 1)
    (hFu : ∀ u : unitary (Algebra M), F u ∈ unitary B)
    (x : Algebra M) (hx : IsStarNormal x) :
    F (star x) = star (F x) ∧ F (x * x) = F x * F x := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.complex_square_expansion line 92
theorem OAI.KadisonKastler.map_jordan_of_three_squares line 99
theorem OAI.KadisonKastler.map_star_square_of_map_unitary line 115
Source documentation
A continuous unital linear map preserving unitaries preserves all adjoints and all squares on a von Neumann algebra.
```
theorem map_star_square_of_map_unitary
    (F : Algebra M →L[ℂ] B) (hF1 : F 1 = 1)
    (hFu : ∀ u : unitary (Algebra M), F u ∈ unitary B) (x : Algebra M) :
    F (star x) = star (F x) ∧ F (x * x) = F x * F x := by
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.preservesJordan_of_map_unitary line 139
Source documentation
The same map is a star-preserving Jordan map, ready for the surjective orientation theorem.
```
theorem preservesJordan_of_map_unitary
    (F : Algebra M →L[ℂ] B) (hF1 : F 1 = 1)
    (hFu : ∀ u : unitary (Algebra M), F u ∈ unitary B) :
    PreservesJordan F.toLinearMap := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.PreservesJordan