Completion of a C*-normed *-algebra #
This file completes a normed *-algebra satisfying the C*-inequality to a
C*-algebra. It is stated for an arbitrary such algebra; the quasilocal colimit of
Physicslib4/AQFT/HaagKastler/QuasilocalColimit.lean is only one instance, and
nothing here mentions the quasilocal setting.
Blueprint references: def:completion-standing-hypotheses, def:completion-star,
lmm:star-extends-to-completion, lmm:completion-normed-algebra,
lmm:completion-cstar-identity, lmm:completion-of-cstar-normed-star-algebra.
Why this development exists #
There is no C-completion construction anywhere in Mathlib*: no enveloping
C*-algebra, no universal C*-algebra of a *-algebra, no full or reduced group
C*-algebra. Unitization is the only C*-norm construction present and is not a
usable template, since it builds its norm from the left regular representation
rather than completing a given C*-norm.
The compensation is that each obligation is short. The recurring move is
UniformSpace.Completion.induction_on together with isClosed_eq or
isClosed_le, pushing the claim through norm_coe, coe_mul, coe_add and
coe_smul to the corresponding law on A.
What is free and what is not #
Free: the ring and norm structure on the completion (Completion.ring,
Completion.algebra, and the anonymous NormedRing/NormedSpace/
NormedAddCommGroup instances), CompleteSpace, and — once CStarRing is in
place — isometry of the involution, via CStarRing.to_normedStarGroup.
Not free, and the substance of this file:
- the involution. Mathlib puts no
Star,InvolutiveStarorStarRingonUniformSpace.Completionat all, so it must be built withUniformSpace.Completion.map. NotemapRingHomis the wrong tool:staris anti-multiplicative, so it is not a ring homomorphismA → A. - the
NormedAlgebra ℂinstance. Mathlib's instance for a completion (Analysis/Normed/Module/Completion.lean) is gated onSeminormedCommRing, so it does not fire for a noncommutative C*-algebra and must be supplied here.
The standing hypotheses of this file, and the notation Â
(def:completion-standing-hypotheses).
CStarCompletion A is the completion of a type A carrying a NormedRing, a
StarRing, a NormedAlgebra ℂ, a StarModule ℂ and a CStarRing structure.
Every result below is stated under exactly these five hypotheses, so this
abbreviation is the blueprint's standing-hypotheses node: it names the setting
and introduces the notation  for the completion, whose canonical map has dense
range by UniformSpace.Completion.denseRange_coe.
Two remarks on the hypothesis list. No isometry hypothesis is imposed on star:
‖a⋆‖ = ‖a‖ follows from the C*-inequality, since CStarRing.to_normedStarGroup
produces the NormedStarGroup A instance. And StarModule ℂ A and
NormedAlgebra ℂ A are listed because they are genuinely used and are not
consequences of the others — the former is what star_smul on the completion
reduces to on the dense range, and the latter is what NormedAlgebra needs to
complete.
StarModule ℂ A and CStarRing A are not used by the right-hand side, which
needs only the uniform structure. They are listed anyway, and the
unusedArguments lint is suppressed, because naming the setting is the whole
point of this abbreviation: it is the blueprint's standing-hypotheses node, and
every result below is stated under exactly these five. Dropping the two would
make the notation say less than the node it stands for.
Equations
Instances For
The involution on a completion (def:completion-star).
star on A is an isometry — not assumed, but obtained from the C*-inequality
through CStarRing.to_normedStarGroup — hence uniformly continuous, so
UniformSpace.Completion.map lifts it to the completion.
Equations
The involution on the completion agrees with the involution on A along the
canonical map. This is the characterisation every proof below runs through.
The involution extends to the completion (lmm:star-extends-to-completion),
StarRing half: the operation is involutive, additive and anti-multiplicative.
All the laws share one skeleton — Completion.induction_on plus isClosed_eq
plus star_completion_coe — and differ only in which coercion lemma and which
component law of A are cited at the end.
Equations
- Physicslib4.instStarRingCompletion = { toStar := Physicslib4.instStarCompletion, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }
The involution extends to the completion (lmm:star-extends-to-completion),
StarModule half: conjugate-linearity (c • x)⋆ = conj c • x⋆.
On the dense range of the canonical map this reduces to star_smul in A, which
is exactly the StarModule ℂ A hypothesis.
The completion is a normed algebra over ℂ
(lmm:completion-normed-algebra).
This instance exists to work around a real trap: Mathlib's NormedAlgebra
instance for a completion is gated on SeminormedCommRing, so it does not fire
for a noncommutative C*-algebra. The body is nevertheless the same as Mathlib's,
since that proof never uses commutativity — it borrows the NormedSpace instance
and supplies norm_smul_le.
Equations
- Physicslib4.instNormedAlgebraCompletion = { toAlgebra := UniformSpace.Completion.algebra A ℂ, norm_smul_le := ⋯ }
The C-inequality passes to the completion*
(lmm:completion-cstar-identity).
CStarRing is a Prop class with the single field
norm_mul_self_le : ∀ x, ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖, a non-strict inequality between
continuous functions of x, so it transports by isClosed_le plus
Completion.induction_on in a few lines.
Two consequences worth recording: isometry of the involution on the completion is
not a separate obligation, since CStarRing.to_normedStarGroup supplies it; and
CStarRing itself does not require completeness.
The completion of a C-normed *-algebra is a C-algebra**
(lmm:completion-of-cstar-normed-star-algebra).
Assembly only: CStarAlgebra extends NormedRing, StarRing, CompleteSpace,
CStarRing, NormedAlgebra ℂ and StarModule ℂ with no additional fields, and
every parent is now in place — completeness being the ambient CompleteSpace
instance on a completion rather than anything to prove.
Equations
- One or more equations did not get rendered due to their size.
The completion coercion as a bundled *-algebra homomorphism
(lmm:completion-coe-star-alg-hom).
The canonical map η : A → Â is a unital *-algebra homomorphism over ℂ,
bundled as a StarAlgHom. This is a node rather than a citation because Mathlib
supplies the coercion only as a ring homomorphism,
UniformSpace.Completion.coeRingHom; there is no bundled AlgHom or StarAlgHom
version of the completion coercion anywhere, so the assembly must be done by hand.
The ring laws come from coeRingHom, the AlgHom scalar law commutes' reduces
by rfl from UniformSpace.Completion.algebraMap_def, and map_star' is
star_completion_coe in reverse. Its consumer is lmm:quasilocal-embedding, which
needs a bundled morphism.
Equations
- Physicslib4.coeStarAlgHom = { toAlgHom := let __RingHom := UniformSpace.Completion.coeRingHom; { toRingHom := __RingHom, commutes' := ⋯ }, map_star' := ⋯ }