Disjointness and quasi-equivalence of representations #
Building on UnitaryEquiv, this file introduces the two coarser comparisons of
*-representations from superselection theory:
- an intertwiner is a bounded operator
T : H₁ →L H₂withT π₁(a) = π₂(a) T; - two representations are disjoint (
AreDisjoint) when the only intertwiner is0— equivalently, they share no unitarily equivalent subrepresentation; - two representations are quasi-equivalent (
QuasiEquiv) when there is a*-isomorphism of the generated von Neumann algebrasπ₁(A)'' ≃⋆ₐ π₂(A)''carryingπ₁(a)toπ₂(a).
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.
Supporting lemmas #
intertwines_zero—0is always an intertwiner, alongsideIntertwines.addandIntertwines.smul.restrictStarAlgEquiv'— restricts a*-isomorphism across two ambient spaces to given subalgebras; an implementation step feedingUnitaryEquiv.quasiEquiv's proof.
Intertwiners #
An intertwiner from π₁ to π₂: a bounded operator T : H₁ → H₂ with T π₁(a) = π₂(a) T for all a.
An intertwiner maps the action of A on H₁ to its action on H₂. Intertwiners form a vector space
closed under composition and adjoints (Intertwines.comp, Intertwines.adjoint); a unitary
intertwiner is a unitary equivalence. The intertwiners from π to itself are the commutant π(A)'
(intertwines_self_iff_mem_centralizer), so π is irreducible exactly when they are the scalars.
Two representations are disjoint when 0 is their only intertwiner (AreDisjoint).
Implementation note: the condition is stated pointwise, T(π₁(a)x) = π₂(a)(Tx) for all x ∈ H₁.
Blueprint: the intertwiners of def:disjoint-representations
Equations
- Physicslib4.GNS.Intertwines π₁ π₂ T = ∀ (a : A) (x : H₁), T ((π₁ a) x) = (π₂ a) (T x)
Instances For
The composition of intertwiners is an intertwiner.
The adjoint of an intertwiner π₁ → π₂ is an intertwiner π₂ → π₁.
Disjointness #
Disjoint representations: the only intertwiner from π₁ to π₂ is 0.
Disjoint representations have nothing in common: no nonzero subrepresentation of one is
unitarily equivalent to a subrepresentation of the other. Disjointness is symmetric
(AreDisjoint.symm), and unitarily equivalent representations on a nonzero space are never disjoint
(UnitaryEquiv.not_areDisjoint). Two irreducible representations are either disjoint or
unitarily equivalent (areDisjoint_or_unitaryEquiv_of_isIrreducible), so distinct
superselection sectors give disjoint representations. Equilibrium (KMS) states of an infinite
system at different temperatures typically give disjoint representations too.
Blueprint: def:disjoint-representations
Equations
- Physicslib4.GNS.AreDisjoint π₁ π₂ = ∀ (T : H₁ →L[ℂ] H₂), Physicslib4.GNS.Intertwines π₁ π₂ T → T = 0
Instances For
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).
Unitarily equivalent representations are not disjoint (on nonzero spaces): the implementing unitary is a nonzero intertwiner.
Schur's lemma and the irreducible dichotomy #
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.
The irreducible dichotomy. Two irreducible representations are either disjoint or unitarily equivalent.
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.
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 #
The commutant π(A)' of a representation, as a von Neumann algebra.
π(A)' consists of the bounded operators commuting with every π(a), that is, the intertwiners from
π to itself (mem_commutantVonNeumann_iff_intertwines). It is a von Neumann algebra because π(A)
is closed under adjoints and a commutant equals its own bicommutant (S''' = S'). π is
irreducible exactly when π(A)' is the scalars
(isIrreducible_iff_commutantVonNeumann_eq_scalars), and π(A)' and π(A)'' are each other's
commutants (commutant_gnsVonNeumannAlgebra, commutant_commutantVonNeumann).
Implementation note: the algebra is vonNeumannOfSelfAdjoint applied to the commutant
Set.centralizer (Set.range π), whose underlying set is again that commutant
(coe_commutantVonNeumann).
Blueprint: thrm:commutant-von-neumann
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 #
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 #
Conjugation by a unitary preserves the adjoint (star).
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
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)''.
Quasi-equivalence: a *-isomorphism π₁(A)'' → π₂(A)'' sending π₁(a) to π₂(a) for every a.
Quasi-equivalent representations generate the same von Neumann algebra up to isomorphism.
Mathematically, they therefore have the same normal states (the states given by density matrices),
which form the folium of a representation, so quasi-equivalence means having the same folium; they
may differ in multiplicity, as a representation and its amplification do. The library proves none of
these three facts. Quasi-equivalence is an equivalence relation (QuasiEquiv.refl,
QuasiEquiv.symm, QuasiEquiv.trans) and is coarser than unitary equivalence
(UnitaryEquiv.quasiEquiv).
Implementation note: the isomorphism is a StarAlgEquiv between the underlying *-subalgebras of
the bundled algebras gnsVonNeumannAlgebra π₁ and gnsVonNeumannAlgebra π₂; normality (weak
continuity) of the isomorphism is not required, since a *-isomorphism of von Neumann algebras is
automatically normal.
Blueprint: def:quasi-equivalence
Equations
- One or more equations did not get rendered due to their size.
Instances For
Quasi-equivalence is reflexive.
Quasi-equivalence is symmetric.
Quasi-equivalence is transitive.
Unitary equivalence implies quasi-equivalence. The conjugation
*-isomorphism restricts to a *-isomorphism of the generated von Neumann
algebras carrying π₁(a) to π₂(a).