MATHLIBANNEX / CANONICAL DECLARATION CARD

Finite-dimensional algebra from a separable representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_algebra_of_singleton_amongNonUnital

theorem

Shows that a nonzero unital C*-algebra is finite-dimensional when it has a representative of its unique irreducible-representation class on a separable Hilbert space.

Statement

Let A be a nonzero unital complex C*-algebra, H a separable complex Hilbert space, and π a unital representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. Then A is finite-dimensional over ℂ; finite dimension of A is the conclusion, not an initial hypothesis.

Assumptions

Let A be a nonzero unital complex C*-algebra, H a separable complex Hilbert space, and π a unital representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A.

Conclusion

A itself is finite-dimensional over ℂ; finite dimension of A is the conclusion, not an initial hypothesis.

Proof route

The source converts the quantifier and applies the unital algebra-finiteness theorem. The underlying argument first makes H finite-dimensional and π injective, then embeds A into the finite-dimensional bounded-operator space on H.

Proof steps
  1. Exact Lean statement: ∀ {A : Type u} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {H : Type v} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace ℂ H] [inst_5 : CompleteSpace H] [Nontrivial A] [TopologicalSpace.SeparableSpace H] (pi : MathlibAnnex.Analysis.CStarAlgebra.Representation A H), pi.IsSingletonIrreducibleModelAmongNonUnital → FiniteDimensional ℂ A
  2. FiniteDimensional ℂ A.
  3. The source converts the quantifier and applies the unital algebra-finiteness theorem. The underlying argument first makes H finite-dimensional and π injective, then embeds A into the finite-dimensional bounded-operator space on H.

Main citations

Lean source signature (exact)

theorem finiteDimensional_algebra_of_singleton_amongNonUnital
    [Nontrivial A] [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) :
    FiniteDimensional ℂ A

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON

Exact Card identity

Stable Card ID: f34adabc1cac70dceb32acb212d5f7c0b85c259c2c330087932a6f3fe9f5e8a9

Card revision: 2

Card SHA-256: ecc79438064f62aae0bbacb681b74e61a1bdf6907db81f63936cc28abaaa4b2d

Approved exposition revision: 6

Approved exposition SHA-256: 3910c52590590990ffd018d67dee9f0baf1b08920998b22a4402c0781b9282db

Source: MathlibAnnex v0.4.0