ProjectionJordanMap.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Projection preservation from unitary preservation

Two scalar phases on a projection determine both its adjoint and its square. Thus a unital complex-linear map preserving unitaries preserves projections and orthogonal projection products, without an analytic expansion of the exponential.

def OAI.KadisonKastler.projectionPhaseUnitary line 24
Source documentation
Put one unit-modulus scalar on a projection and one on its complement.
```
def projectionPhaseUnitary (p : A) (hp : IsStarProjection p)
    (z : ℂ) (hz : star z * z = 1) : unitary A :=
…
```
theorem OAI.KadisonKastler.phase_square_expansion line 40
theorem OAI.KadisonKastler.unitary_phase_equation line 49

theorem OAI.KadisonKastler.map_isStarProjection_of_map_unitary line 61

Source documentation

A unital complex-linear unitary-preserving map preserves projections.

theorem map_isStarProjection_of_map_unitary
    (F : A →ₗ[ℂ] B) (hF1 : F 1 = 1)
    (hFu : ∀ u : unitary A, F u ∈ unitary B)
    (p : A) (hp : IsStarProjection p) : IsStarProjection (F p) := by
…

theorem OAI.KadisonKastler.map_projection_mul_eq_zero_of_map_unitary line 97

Source documentation

Projection preservation also preserves orthogonality.

theorem map_projection_mul_eq_zero_of_map_unitary
    (F : A →ₗ[ℂ] B) (hF1 : F 1 = 1)
    (hFu : ∀ u : unitary A, F u ∈ unitary B)
    (p q : A) (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = 0) :
    F p * F q = 0 := by
…