No nonzero irreducible representation on a separable Hilbert space

MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable

theorem

Distinguishes separable representability from separable irreducible representability.

Statement

The fixed CAR-based C*-algebra A has no nonzero irreducible representation on any separable complex Hilbert space.

Assumptions

Let A ⊆ B(Hₐₜ) be the fixed unital C*-algebra obtained by adjoining the chosen shell-link unitaries to the atomic representation of the CAR algebra C, and then taking the norm-closed unital *-algebra they generate. Let K be any separable complex Hilbert space, and let σ: A → B(K) be any complex-linear multiplicative *-preserving map. It need not preserve the unit, and no faithfulness is assumed.

Conclusion

σ is not both nonzero and irreducible. Equivalently, no such K and σ give a nonzero irreducible representation of A.

Proof route

If σ were nonzero and irreducible, it would be unital. The uniqueness of the atomic irreducible model would make it a separable singleton model, so the proved Rosenberg consequence would force A to be finite-dimensional, a contradiction.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint

  Exact source attribution.

• MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_algebra_of_singleton_amongNonUnital

  Exact source attribution.

Lean source declaration (exact)

/-- The main target admits no nonzero irreducible ordinary representation on
a separable complete complex Hilbert space.  The input representation is not
assumed to preserve the unit. -/
theorem not_isIrreducible_of_separable
    {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
    (rho : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H)) :
    ¬ rho.IsIrreducible := by
  intro hrho
  let pi : Representation AtomicCounterexampleAlgebra H := rho.toUnital hrho
  have hpi : Representation.IsIrreducible pi :=
    NonUnitalRepresentation.isIrreducible_toUnital rho hrho
  have hambient_pi : atomicCounterexampleRepresentation.UnitaryEquivalent pi := by
    obtain ⟨U, hU⟩ := (atomicCounterexampleEndpoint.{v}).captures_nonunital H rho hrho
    refine ⟨U, ?_⟩
    intro a x
    simpa [atomicCounterexampleRepresentation, pi] using hU a x
  have hsingleton :
      Representation.IsSingletonIrreducibleModelAmongNonUnital.{0, v, 0} pi := by
    refine ⟨hpi, ?_⟩
    intro K _ _ _ sigma hsigma
    have hambient_sigma :
        atomicCounterexampleRepresentation.UnitaryEquivalent (sigma.toUnital hsigma) := by
      obtain ⟨U, hU⟩ := (atomicCounterexampleEndpoint.{0}).captures_nonunital K sigma hsigma
      refine ⟨U, ?_⟩
      intro a x
      change U (atomicCounterexampleRepresentation a x) = sigma a (U x)
      simpa [atomicCounterexampleRepresentation] using hU a x
    exact Representation.unitaryEquivalent_trans
      (Representation.unitaryEquivalent_symm hambient_pi) hambient_sigma
  exact (atomicCounterexampleEndpoint.{v}).not_finiteDimensional_target
    (Representation.finiteDimensional_algebra_of_singleton_amongNonUnital
      pi hsingleton)

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

Lean realization notes

The source predicate IsIrreducible includes nonzeroness, so the zero map is no counterexample to this statement. K ranges over an arbitrary independent universe v. This is not a claim that A is nonprimitive: its faithful atomic irreducible representation remains available. The comma in ∀ σ, ¬ σ.IsIrreducible separates the quantified variable from the proposition; it is not a substitute for an implication arrow.