MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion
The same concrete target has a literal representation on the selected atomic Hilbert space.
Statement
Let
Definition
The generic ambient-inclusion construction takes a concrete generated star algebra to its inclusion in the existing operator algebra. Using the atomic CAR action and the fixed links gives exactly
Assumptions
The representative shell family is the only input beyond the fixed CAR construction. Both
Conclusion
The definition supplies the displayed unital representation
Main citations
- Definition and its exact construction · Exact source
- The CAR atomic representation on the ambient Hilbert space · Exact source
- One fixed choice of the realized unitary links · Exact source
- The concrete target from that choice · Exact source
- Generic literal ambient inclusion · Exact source
- The source map into the same target · Exact source
- Underlying-operator identity giving the composition · Exact source
- Separate injectivity of this inclusion · Exact source
- Separate irreducibility from the CAR realization · Exact source
Lean source signature (exact)
noncomputable def shellFamilyInclusion (family : RepresentativeShellFamily) :
Representation (ShellFamilyTarget family)
(MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=
MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation
(shellFamilyLinks family)Here family fixes the shell data, shellFamilyLinks family is ShellFamilyTarget family is completedRootPureState is the CAR root state SelectedAtomicHilbert completedRootPureState is AtomicConstruction.ambientInclusion is shellFamilySourceHom family is
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF
Lean realization notes
The inclusion and source map have different domains:
Exact Card identity
Language: en
CARD_CONTENT_COMPLETE
Card UID: lfh:lfh-declaration-card:sha256:ffdf67ba93b5d952ceffbf6ff392cad78042152bb56e5805d8aa38814343e57d
Card revision: 1 · SHA-256: 608748718c9b2fa8d4a3f8b34ab899dc76f70c13f6b41b13231b5aa918686622
Exposition revision: 1 · SHA-256: dcb3559cfc538c702d2b99364db637cf2e502471606b7a64efecd50aae28b11e
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73
Header SHA-256: a61bce75172a10087824d5bebaffac33cdcf1c3284cf7494435313367660be91