Documentation

Physicslib4.GNS.Superselection

Disjointness and quasi-equivalence of representations #

Building on UnitaryEquiv, this file introduces the two coarser comparisons of *-representations from superselection theory:

We prove the basic algebra of intertwiners, that disjointness is symmetric and irreflexive (unitarily equivalent representations are never disjoint), that quasi-equivalence is an equivalence relation, and that unitary equivalence implies quasi-equivalence.

Intertwiners #

def Physicslib4.GNS.Intertwines {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] (π₁ : A →⋆ₐ[] H₁ →L[] H₁) (π₂ : A →⋆ₐ[] H₂ →L[] H₂) (T : H₁ →L[] H₂) :

T : H₁ →L H₂ intertwines π₁ and π₂ when T π₁(a) = π₂(a) T.

Equations
Instances For
    theorem Physicslib4.GNS.intertwines_zero {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} :
    Intertwines π₁ π₂ 0
    theorem Physicslib4.GNS.Intertwines.add {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} {S T : H₁ →L[] H₂} (hS : Intertwines π₁ π₂ S) (hT : Intertwines π₁ π₂ T) :
    Intertwines π₁ π₂ (S + T)
    theorem Physicslib4.GNS.Intertwines.smul {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} {T : H₁ →L[] H₂} (c : ) (hT : Intertwines π₁ π₂ T) :
    Intertwines π₁ π₂ (c T)
    theorem Physicslib4.GNS.Intertwines.comp {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {H₃ : Type u_4} [NormedAddCommGroup H₃] [InnerProductSpace H₃] [CompleteSpace H₃] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} {π₃ : A →⋆ₐ[] H₃ →L[] H₃} {S : H₂ →L[] H₃} {T : H₁ →L[] H₂} (hS : Intertwines π₂ π₃ S) (hT : Intertwines π₁ π₂ T) :
    Intertwines π₁ π₃ (S ∘SL T)

    The composition of intertwiners is an intertwiner.

    theorem Physicslib4.GNS.Intertwines.adjoint {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} {T : H₁ →L[] H₂} (hT : Intertwines π₁ π₂ T) :

    The adjoint of an intertwiner π₁ → π₂ is an intertwiner π₂ → π₁.

    Disjointness #

    def Physicslib4.GNS.AreDisjoint {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] (π₁ : A →⋆ₐ[] H₁ →L[] H₁) (π₂ : A →⋆ₐ[] H₂ →L[] H₂) :

    Two representations are disjoint when the only operator intertwining them is 0.

    Equations
    Instances For
      theorem Physicslib4.GNS.AreDisjoint.symm {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} (h : AreDisjoint π₁ π₂) :
      AreDisjoint π₂ π₁

      Disjointness is symmetric (take adjoints of intertwiners).

      A representation on a nonzero Hilbert space is never disjoint from itself (the identity is a nonzero intertwiner).

      theorem Physicslib4.GNS.UnitaryEquiv.not_areDisjoint {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} [Nontrivial H₁] (h : UnitaryEquiv π₁ π₂) :
      ¬AreDisjoint π₁ π₂

      Unitarily equivalent representations are not disjoint (on nonzero spaces): the implementing unitary is a nonzero intertwiner.

      Schur's lemma and the irreducible dichotomy #

      theorem Physicslib4.GNS.UnitaryEquiv.of_intertwines_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} (h1 : IsIrreducible π₁) (h2 : IsIrreducible π₂) {T : H₁ →L[] H₂} (hT : Intertwines π₁ π₂ T) (hT0 : T 0) :
      UnitaryEquiv π₁ π₂

      Schur's lemma. A nonzero intertwiner between two irreducible representations rescales to a unitary: π₁ and π₂ are unitarily equivalent. The operator T⋆T commutes with π₁, hence is a positive scalar r · 1; the normalisation (√r)⁻¹ · T is then a linear isometry, and T T⋆ being a nonzero scalar makes it surjective, i.e. a unitary equivalence.

      theorem Physicslib4.GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} (h1 : IsIrreducible π₁) (h2 : IsIrreducible π₂) :
      AreDisjoint π₁ π₂ UnitaryEquiv π₁ π₂

      The irreducible dichotomy. Two irreducible representations are either disjoint or unitarily equivalent.

      theorem Physicslib4.GNS.eq_smul_of_intertwines_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} (h1 : IsIrreducible π₁) (h2 : IsIrreducible π₂) {S T : H₁ →L[] H₂} (hS : Intertwines π₁ π₂ S) (hT : Intertwines π₁ π₂ T) (hS0 : S 0) :
      ∃ (lam : ), T = lam S

      Schur multiplicity. The space of intertwiners between two irreducible representations is at most one-dimensional: any two intertwiners with S ≠ 0 are proportional, T = λ • S.

      The endomorphism algebra of an irreducible representation #

      A self-intertwiner is exactly an operator in the commutant of the representation.

      theorem Physicslib4.GNS.intertwines_self_iff_isScalar {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {π : A →⋆ₐ[] H₁ →L[] H₁} (h : IsIrreducible π) {T : H₁ →L[] H₁} :
      Intertwines π π T ∃ (c : ), T = c 1

      The endomorphism algebra of an irreducible representation is ℂ · 1. Every self-intertwiner of an irreducible representation is a scalar multiple of the identity.

      The commutant (self-intertwiner) von Neumann algebra #

      noncomputable def Physicslib4.GNS.commutantVonNeumann {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] (π : A →⋆ₐ[] H₁ →L[] H₁) :

      The commutant π(A)' as a von Neumann algebra: the algebra of self-intertwiners of π — its "gauge"/intertwiner algebra. The centralizer of π(A) is self-adjoint, and a commutant is always a von Neumann algebra (S''' = S').

      Equations
      Instances For

        Membership in the commutant von Neumann algebra is exactly being a self-intertwiner of π.

        A representation is irreducible iff its commutant von Neumann algebra is trivial, π(A)' = ℂ · 1. This is the von Neumann form of Schur's lemma: the gauge/intertwiner algebra collapses to the scalars exactly for irreducibles.

        Double-commutant duality #

        Double-commutant duality (I). The commutant of the generated von Neumann algebra π(A)'' is the commutant von Neumann algebra π(A)'. This is the triple-commutant collapse S''' = S' applied to the self-adjoint image π(A).

        Double-commutant duality (II). The commutant of the commutant von Neumann algebra π(A)' is the generated von Neumann algebra π(A)'' — this is exactly the definition of the bicommutant. So π(A)'' and π(A)' are each other's commutants.

        A factor and its commutant. A von Neumann algebra and its commutant share the same center (their intersection is symmetric), so the generated algebra π(A)'' is a factor if and only if its commutant π(A)' is a factor.

        Triviality duality. The commutant collapses to the scalars π(A)' = ℂ · 1 if and only if the generated algebra is everything π(A)'' = B(H). This is the commutant form of the equivalence "irreducible ⟺ generates B(H)".

        The pure-state dichotomy #

        theorem Physicslib4.GNS.exists_gns_areDisjoint_or_unitaryEquiv_of_isPure {A : Type u} [CStarAlgebra A] {ω₁ ω₂ : State A} (h1 : IsPure ω₁) (h2 : IsPure ω₂) :
        ∃ (K₁ : Type u) (x : NormedAddCommGroup K₁) (x_1 : InnerProductSpace K₁) (x_2 : CompleteSpace K₁) (π₁ : A →⋆ₐ[] K₁ →L[] K₁) (Ω₁ : K₁) (K₂ : Type u) (x_3 : NormedAddCommGroup K₂) (x_4 : InnerProductSpace K₂) (x_5 : CompleteSpace K₂) (π₂ : A →⋆ₐ[] K₂ →L[] K₂) (Ω₂ : K₂), (∀ (a : A), ω₁ a = inner Ω₁ ((π₁ a) Ω₁)) (∀ (a : A), ω₂ a = inner Ω₂ ((π₂ a) Ω₂)) (AreDisjoint π₁ π₂ UnitaryEquiv π₁ π₂)

        The pure-state dichotomy. The GNS representations of two pure states are either disjoint or unitarily equivalent. Pure states thus fall into superselection sectors: the sector of a pure state is the unitary-equivalence class of its (irreducible) GNS representation.

        Quasi-equivalence #

        theorem Physicslib4.GNS.conjCLM_add {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] (U : H₁ ≃ₗᵢ[] H₂) (S T : H₁ →L[] H₁) :
        conjCLM U (S + T) = conjCLM U S + conjCLM U T
        theorem Physicslib4.GNS.conjCLM_mul {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] (U : H₁ ≃ₗᵢ[] H₂) (S T : H₁ →L[] H₁) :
        conjCLM U (S * T) = conjCLM U S * conjCLM U T
        theorem Physicslib4.GNS.conjCLM_smul {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] (U : H₁ ≃ₗᵢ[] H₂) (c : ) (T : H₁ →L[] H₁) :
        conjCLM U (c T) = c conjCLM U T
        theorem Physicslib4.GNS.conjCLM_leftInv {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] (U : H₁ ≃ₗᵢ[] H₂) (T : H₁ →L[] H₁) :
        conjCLM U.symm (conjCLM U T) = T
        theorem Physicslib4.GNS.conjCLM_star {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] (U : H₁ ≃ₗᵢ[] H₂) (T : H₁ →L[] H₁) :
        conjCLM U (star T) = star (conjCLM U T)

        Conjugation by a unitary preserves the adjoint (star).

        noncomputable def Physicslib4.GNS.conjStarAlgEquiv {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] (U : H₁ ≃ₗᵢ[] H₂) :
        (H₁ →L[] H₁) ≃⋆ₐ[] H₂ →L[] H₂

        Conjugation by a unitary as a *-algebra isomorphism of the operator algebras.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Physicslib4.GNS.conjStarAlgEquiv_apply {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] (U : H₁ ≃ₗᵢ[] H₂) (T : H₁ →L[] H₁) :
          @[simp]
          def Physicslib4.GNS.restrictStarAlgEquiv' {B : Type u_5} {C : Type u_6} [Ring B] [StarRing B] [Algebra B] [StarModule B] [Ring C] [StarRing C] [Algebra C] [StarModule C] (e : B ≃⋆ₐ[] C) {S : StarSubalgebra B} {T : StarSubalgebra C} (hfwd : xS, e x T) (hbwd : yT, e.symm y S) :
          S ≃⋆ₐ[] T

          A *-isomorphism carrying the underlying set of one star-subalgebra onto that of another restricts to a *-isomorphism between them (cross-space form).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The generators π(a) lie in the generated von Neumann algebra π(A)''.

            def Physicslib4.GNS.QuasiEquiv {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] (π₁ : A →⋆ₐ[] H₁ →L[] H₁) (π₂ : A →⋆ₐ[] H₂ →L[] H₂) :

            Two representations are quasi-equivalent when there is a *-isomorphism of their generated von Neumann algebras carrying π₁(a) to π₂(a).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Physicslib4.GNS.QuasiEquiv.refl {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] (π : A →⋆ₐ[] H₁ →L[] H₁) :

              Quasi-equivalence is reflexive.

              theorem Physicslib4.GNS.QuasiEquiv.symm {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} (h : QuasiEquiv π₁ π₂) :
              QuasiEquiv π₂ π₁

              Quasi-equivalence is symmetric.

              theorem Physicslib4.GNS.QuasiEquiv.trans {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {H₃ : Type u_4} [NormedAddCommGroup H₃] [InnerProductSpace H₃] [CompleteSpace H₃] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} {π₃ : A →⋆ₐ[] H₃ →L[] H₃} (h₁₂ : QuasiEquiv π₁ π₂) (h₂₃ : QuasiEquiv π₂ π₃) :
              QuasiEquiv π₁ π₃

              Quasi-equivalence is transitive.

              theorem Physicslib4.GNS.UnitaryEquiv.quasiEquiv {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[] H₁ →L[] H₁} {π₂ : A →⋆ₐ[] H₂ →L[] H₂} (h : UnitaryEquiv π₁ π₂) :
              QuasiEquiv π₁ π₂

              Unitary equivalence implies quasi-equivalence. The conjugation *-isomorphism restricts to a *-isomorphism of the generated von Neumann algebras carrying π₁(a) to π₂(a).