NonunitalFunctionalRepresentation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite functional representation needed in KR02 Lemma 7.18. Real functionals on the nonunital algebra are extended by the continuous self-adjoint second-coordinate projection of its unitization. The existing bounded GNS domination theorem then realizes all of them in one commutant. No faithfulness or simplicity hypothesis is used.

lemma OAI.WeakPureInfiniteness.unitizationSnd_isSelfAdjoint line 23
def OAI.WeakPureInfiniteness.selfAdjointUnitizationSnd line 31
Source documentation
The self-adjoint second coordinate is real linear and continuous, although it need not preserve positivity. Positivity is supplied later by domination.
```
def selfAdjointUnitizationSnd : selfAdjoint (Unitization ℂ A) →L[ℝ] selfAdjoint A where
…
```
lemma OAI.WeakPureInfiniteness.selfAdjointUnitizationSnd_inr line 39

theorem OAI.WeakPureInfiniteness.finite_nonunital_functional_representation line 46

Source documentation

Simultaneous commutant realization of a finite family of real functionals. The representation acts on the unitization so its GNS vector is cyclic; restriction to the original algebra gives precisely the requested values.

theorem finite_nonunital_functional_representation
    (l : I → selfAdjoint A →L[ℝ] ℝ) :
    ∃ f : Unitization ℂ A →ₚ[ℂ] ℂ, f 1 = 1 ∧
      ∃ T : I → f.GNS →L[ℂ] f.GNS,
        (∀ i, IsSelfAdjoint (T i)) ∧
        (∀ i a, Commute (T i) (f.gnsStarAlgHom a)) ∧
        ∀ i (a : selfAdjoint A), l i a =
          (⟪Pureness.stateGNSVector f,
            T i (f.gnsStarAlgHom (a : Unitization ℂ A)
              (Pureness.stateGNSVector f))⟫_ℂ).re := by
…

Mentions: OAI.Pureness.stateGNSVector