MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective
theorem
The ideal dichotomy of the same target forces the constructed nonzero representation to be injective.
Statement
Let be the completed CAR algebra and its normalized trace. Fix a representative shell family and its chosen unitary links in the selected atomic representation . Write for the resulting concrete target and , , for its faithful unital source map. This fixes one target and one source map throughout. Choose the state extension of supplied by state extension along . Its GNS representation is , with
The inner product is linear in its second argument. The -orbit of is dense by the GNS construction. The representation is injective.
Assumptions
The representative shell family is fixed. The established closed two-sided ideal dichotomy of this same is available as a theorem. The GNS space is nonzero because its canonical vector has norm .
Conclusion
If , then . Thus the GNS representation of the chosen state on is faithful as an algebra representation.
This does not infer faithfulness of an arbitrary vector state from faithfulness of its representation. State faithfulness requires its own argument. No irreducibility of , purity of , or separability of is assumed.
Proof route
Apply the closed-ideal dichotomy to the kernel and exclude the whole-algebra case using the unit on the nonzero GNS space.
Proof steps
The kernel is a norm-closed two-sided ideal. The previously established result
shellFamilyTarget_closedIdeal_dichotomygives or .If , then . But is unital, so
contradicting
.
Hence
,
which is precisely injectivity. The source applies
Representation.injective_of_closed_ideal_dichotomy after
installing the separately proved nontriviality of
.
Main citations
- The
stated existence or structural result —
MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective - The
fixed concrete target and source map —
MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom - Faithfulness
of the source embedding —
MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom_injective - The
target-state GNS definition —
MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation - Nontriviality
witnessed by the unit vector —
MathlibAnnex.CStarAlgebra.CAR.nontrivial_tracialHilbertSpace - Closed-ideal
dichotomy of the fixed target —
MathlibAnnex.CStarAlgebra.CAR.shellFamilyTarget_closedIdeal_dichotomy - The
kernel argument for a nonzero unital representation —
MathlibAnnex.Analysis.CStarAlgebra.Representation.injective_of_closed_ideal_dichotomy
Lean source signature (exact)
theorem tracialRepresentation_injective (family : RepresentativeShellFamily) :
Function.Injective (tracialRepresentation family)| In the source | Mathematical meaning |
|---|---|
family : RepresentativeShellFamily |
The fixed shell family and resulting target , source map and chosen trace extension . |
tracialRepresentation family |
The unital GNS action of on its complete GNS space, with canonical vector of norm one. |
Function.Injective (tracialRepresentation family) |
If as bounded operators on , then in . This is faithfulness of the representation, not irreducibility or a direct assertion of state faithfulness. |
Further source notes: In the linked proof,
| |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective
Accepted content SHA-256: 8d2b084d7109e2dcfa2c7ad5af99f46231cecd7ff86338f53d0b6dd1efb0dc2f
Accepted source guide SHA-256: 30cad76ac775176df90bba2a7039c3c5de56fc41d97ffc7df3514338af0262aa
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73