MATHLIBANNEX / CANONICAL DECLARATION CARD

The cyclic sum fills every irreducible target representation

MathlibAnnex.CStarAlgebra.CAR.exists_surjective_selectedAtomicCyclicIsometry

theorem

Uses shell reconstruction and residual lines to turn an isometric CAR intertwiner into a unitary equivalence on the source.

Statement

Under the shell-family, generator and irreducibility assumptions below, there exist unit vectors , for , and a surjective complex-linear isometry such that

for every , and for every . In particular, is unitarily equivalent to the selected atomic source representation .

Assumptions

Let be the completed CAR algebra, the completion of the matrix stages under . Let be the image of the first diagonal matrix unit, so and decreases through projections. The root state takes the value on each matrix stage.

Choose one pure state from each unitary-equivalence class of pure-state Gelfand-Naimark-Segal (GNS) representations, with root index and . Write for its complete complex GNS space, unital star representation and unit cyclic vector. Set , , and let be the coordinate embedding. No countability of is assumed. Inner products are linear in the second argument.

A supplied shell family consists of unital complex star automorphisms and elements . Put . The identities are , and . At the root, is the identity and . The family is an input, not an existence conclusion.

Let be unitaries on satisfying for all , and assume . Let be the norm-closed unital star algebra they generate. Write as an element of , and for the element represented by . Let be a unital complex star representation on a complete complex Hilbert space, put , and put . Assume is nonzero and irreducible: its only closed reducing subspaces are and . This theorem does not assume the additional identity . The root normalization is required.

Conclusion

The selected cyclic pieces exhaust the target Hilbert space. The source-restriction equivalence is the direct consequence obtained by viewing the surjective isometry as a unitary. The representation being assumed irreducible is on , not its generally reducible restriction on .

Proof route

The common-root vector-state theorem supplies compatible unit vectors. Cyclic-sum assembly gives an isometry with closed source-reducing range . Shell reconstruction splits each represented generator into a strong shell sum and a residual corner. Both parts and their adjoints preserve . Norm-closed generation then makes a nonzero reducing subspace for , so irreducibility forces .

Proof steps

  1. The common-root construction gives and of norm one with the selected CAR vector states, , and fixedness under their respective flags. Assemble the cyclic pieces into . Its range is closed because is complete and is an isometry. The relations for and show that reduces . Let project onto the common range of and let project onto the common range of . Assembly gives .

  2. Since , the represented root generator is . Thus the root-index member equals the common vector . Consequently and . Reconstruct with , , and . The operators and are strong limits of finite sums of and their adjoints. Closedness and source reduction make invariant under both limits.

  3. Fixedness and the vector transport give and . For , the vector lies in , so . For the adjoint, use and to obtain . Thus reduces the residual corner and, together with the shell sum, every .

  4. The orthogonal projection onto commutes with the represented source and every added generator. The commutation relation is stable under star-algebra operations and operator-norm limits, so reduces all of . It contains the unit vector and is therefore nonzero. Irreducibility gives , which is exactly surjectivity of . Its pointed-vector and source intertwining identities are retained.

Main citations

Lean source signature (exact)

theorem exists_surjective_selectedAtomicCyclicIsometry
    (family : RepresentativeShellFamily)
    (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →
      MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
        MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)
    (hLunit : ∀ i, L i ∈ unitary
      (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
        MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))
    (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation
      (transportedFlag family i n - transportedFlag family i (n + 1))) =
        representedShellLink family i n)
    (hLroot : L completedRootPureState.classOf = 1)
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] (rho : Representation (AtomicTarget L) K)
    (hrho : rho.IsIrreducible) :
    ∃ (eta_o : K) (eta : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → K)
      (W : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →ₗᵢ[ℂ] K),
      Function.Surjective W ∧
      ‖eta_o‖ = 1 ∧
      (∀ i, ‖eta i‖ = 1) ∧
      (∀ i, W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i) ∧
      (∀ i, (Unitary.linearIsometryEquiv
        (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K)
          (eta i) = eta_o) ∧
      ∀ a,
        W.toContinuousLinearMap.comp (selectedAtomicRepresentation a) =
          ((restrictedRepresentation L rho) a).comp
            W.toContinuousLinearMap

Here Limit is , completedRootPureState is the root state bundled with its purity proof, and SelectedAtomicHilbert ... is . AtomicTarget L is and restrictedRepresentation L rho is . Source eta_o denotes the common vector ; eta i denotes at source index i. The equality of eta at the root index with eta_o follows from hLroot, rather than from their names. Function.Surjective W supplies the extra property that the isometry fills . hLsource records the shell action; no hypothesis named hLmap occurs in this declaration.

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

Lean realization notes

The conclusion displayed here intertwines the CAR source. To obtain intertwining for every element of , the full capture theorem also uses the prescribed action . No multiplicity assertion for arbitrary reducible target representations and no unconditional existence of a shell family is claimed.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:0efa27a129d831d1ec7063acc030ac436bf2943bf9740b72e0581bfdea44cb03

Card revision: 1 · SHA-256: 5fb3870842607637f36f0d394546e845aa17652f3b2b9f5363bebcc9c2a4d26d

Exposition revision: 1 · SHA-256: 8d9b9d22f8e6fca5a6f830d653607771e8f448c6d887a8c23a1277b891e9f59b

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 713d3452989e6b62bea9be9f648f017746306982c3f52affdfcd97ba64c3ed34

Back to top ↑