OAI/Analysis/KadisonKastler/TracialQuotientRepresentation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.tracialSequenceAlgebra_in_range line 24
2. theorem OAI.KadisonKastler.tracialSequenceRepresentation_mem line 37
3. def OAI.KadisonKastler.tracialSequenceHom line 42
4. theorem OAI.KadisonKastler.tracialSequenceHom_injective line 46
5. theorem OAI.KadisonKastler.tracialSequenceHom_surjective line 52
6. def OAI.KadisonKastler.tracialSequenceEquiv line 58
7. theorem OAI.KadisonKastler.tracialSequenceEquiv_coe line 63
8. def OAI.KadisonKastler.representedTracialQuotientTrace line 66
9. theorem OAI.KadisonKastler.representedTracialQuotientTrace_equiv line 71
10. theorem OAI.KadisonKastler.FaithfulTracialState.finite line 78

    Source documentation

    Faithfulness and traciality force every isometry to be unitary.

    theorem FaithfulTracialState.finite {A : Type*} [CStarAlgebra A]
        (σ : FaithfulTracialState A) (v : A) (hv : star v * v = 1) : v * star v = 1 := by
    …

    Mentions: OAI.KadisonKastler.FaithfulTracialState

11. theorem OAI.KadisonKastler.tracialSequenceAlgebra_finite line 88