OAI/Analysis/KadisonKastler/StarCorrection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The involution in multiplication correction

This is the algebraic star-preserving part of the UCP criterion. The linear correction itself remains an explicit hypothesis.

  1. theorem OAI.KadisonKastler.linearEquiv_symm_map_star line 18
  2. theorem OAI.KadisonKastler.transportedMul_star line 24
  3. def OAI.KadisonKastler.correctedStarAlgEquiv line 32

    Source documentation

    The star-algebra equivalence furnished by a star-preserving linear correction of the transported multiplication.

    noncomputable def correctedStarAlgEquiv (F : A ≃ₗ[ℂ] B) (L : A ≃ₗ[ℂ] A)
    (hL : ∀ x y, L (transportedMul F x y) = L x * L y)
    (hFstar : ∀ x, F (star x) = star (F x))
    (hLstar : ∀ x, L (star x) = star (L x)) : A ≃⋆ₐ[ℂ] B :=
…

    Mentions: OAI.KadisonKastler.transportedMul

  4. theorem OAI.KadisonKastler.correctedStarAlgEquiv_apply line 44