MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget
Places a represented algebra and a chosen family of bounded operators in one concrete closed algebra.
Statement
Let
Definition
Put
Assumptions
The algebra
Conclusion
The construction provides a closed unital star subalgebra
Main citations
- Exact declaration and proof · Exact source
- MathlibAnnex.Analysis.CStarAlgebra.generated · Exact source
- MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom · Exact source
- MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom_coe · Exact source
- MathlibAnnex.CStarAlgebra.AtomicConstruction.generator · Exact source
- MathlibAnnex.CStarAlgebra.AtomicConstruction.generator_coe · Exact source
- MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion · Exact source
- MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom_injective · Exact source
- MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion_injective · Exact source
- MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget.instIsClosed · Exact source
Lean source signature (exact)
noncomputable def concreteTarget (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))
(U : J → H →L[ℂ] H) : StarSubalgebra ℂ (H →L[ℂ] H) :=
generated (Set.range pi ∪ Set.range U)In the code, pi is U is the family concreteTarget pi U is H →L[ℂ] H means a bounded complex-linear operator on →⋆ₐ[ℂ] denotes a unital complex-linear
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF
Lean realization notes
The closure is taken inside the given operator algebra. The construction does not assert simplicity or irreducibility, and it introduces no universal completion of
Exact Card identity
Language: en
CARD_CONTENT_COMPLETE
Card UID: lfh:lfh-declaration-card:sha256:b05645c888ce4601c51f1b4fcfe1fa9e0fc9f8489024601e9bf3e1e9811d4e26
Card revision: 1 · SHA-256: 66b7b6935dd913a75006fffad6343b623e595b2a5ebbf7846d262b0d4849e125
Exposition revision: 1 · SHA-256: 8655c1a4a3f7e3a761fd34c830e74020310fd0c47245f74aaf8efcc1dec6ad4c
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73
Header SHA-256: e2dd36aeb72f45769069686cd03a443777c047101e021627f9ae23a900051b26