No nonzero irreducible closed subrepresentation of the tracial model

MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_restrictToReducing_separableCounterexampleRepresentation

theorem

Extends the separable irreducibility exclusion to every closed reducing subspace of the fixed representation.

Statement

The faithful tracial representation ρ: A → B(Hτ) has no nonzero irreducible closed subrepresentation.

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 Hτ = L²(C, τC) be the GNS Hilbert space of the normalized CAR trace τC. Let ρ be the specified tracial representation, and let M be a closed complex-linear subspace of Hτ invariant under every ρ(a) and its adjoint.

Conclusion

The restricted representation ρ|M: A → B(M) is not both nonzero and irreducible. This includes M = {0}, for which nonzeroness already fails.

Proof route

A closed subspace M is complete, and as a subspace of the separable Hilbert space Hτ it is separable. Apply the exclusion of separable irreducible representations to the exact restriction.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable

  Exact source attribution.

Lean source declaration (exact)

theorem not_isIrreducible_restrictToReducing_separableCounterexampleRepresentation
    (M : Submodule ℂ SeparableCounterexampleHilbertSpace)
    (hM : separableCounterexampleRepresentation.Reduces M) :
    letI : CompleteSpace M := hM.1.completeSpace_coe
    ¬ Representation.IsIrreducible
      (Representation.restrictToReducing separableCounterexampleRepresentation M hM) := by
  letI : CompleteSpace M := hM.1.completeSpace_coe
  letI : TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace :=
    separableSpace_separableCounterexampleHilbertSpace
  letI : TopologicalSpace.SeparableSpace M := inferInstance
  exact not_isIrreducible_of_separable
    (Representation.restrictToReducing
      separableCounterexampleRepresentation M hM).toNonUnitalStarAlgHom

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

Lean realization notes

The source argument hM : ρ.Reduces M contains closedness and invariance under both operators and their adjoints. The conclusion is about the defined restriction, not an arbitrary subset or a nonclosed algebraic subspace. It does not assert that all invariant subspaces are absent.