Singleton condition tested against all irreducible representations

MathlibAnnex.Analysis.CStarAlgebra.Representation.IsSingletonIrreducibleModelAmongNonUnital

def

Defines the unital singleton condition while allowing the quantified representations to be presented without a unit equation.

Statement

Let be a unital complex -algebra, let be a complex Hilbert space, and let be a unital -representation. The predicate below requires to be nonzero irreducible and compares it with every nonzero irreducible -representation , even when the data type used for does not initially record .

Definition

For every complete complex Hilbert space and every -representation that is nonzero irreducible, irreducibility forces Indeed, is an idempotent whose range is a nonzero closed reducing subspace, hence all of . The source expression rho.toUnital hrho therefore packages the same operator-valued map as a unital representation. The required conclusion is a unitary satisfying

Assumptions

No separability or faithfulness assumption is included. The distinction is between a unital algebra and whether unit preservation is recorded in the representation interface; it is not a claim that or lacks a unit.

Conclusion

The predicate says that represents the unique unitary-equivalence class of nonzero irreducible -representations of the unital algebra , with the same operator maps whether or not the input interface initially records the unit equation.

The two implications in Both directions of the singleton comparison identify this condition with the corresponding comparison restricted to unital representations: one direction regards the same unital representation through the interface that does not require a unit equation, the other uses the forced equation just proved. These remain distinct declared predicates and distinct Cards.

/-- Raw singleton-spectrum hypothesis for a unital algebra, with every
ordinary nonzero irreducible representation included and no faithfulness
built into the definition. -/
def IsSingletonIrreducibleModelAmongNonUnital
    (pi : Representation A H) : Prop :=
  pi.IsIrreducible ∧
    ∀ (K : Type w) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
      [CompleteSpace K] (rho : NonUnitalRepresentation (A := A) (H := K)),
      ∀ hrho : rho.IsIrreducible,
        pi.UnitaryEquivalent (rho.toUnital hrho)

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF