PhyslibAlpha.AlgebraicFramework.WStarAlgebra.Mathlib

`WStarAlgebraStructure A` gives Mathlib's `WStarAlgebra A`

This file closes the connection `Basic.lean`'s module docstring flags as unattempted: every `WStarAlgebraStructure A` (a *chosen* predual and identification, a `class`) gives a proof of Mathlib's `WStarAlgebra A` (mere *existence* of a predual, a `Prop`, `Mathlib.Analysis.VonNeumannAlgebra.Basic`).

There are exactly two mismatches between `toDual : A ≃ₗᵢ[ℂ] StrongDual ℂ (Predual A)` and what `WStarAlgebra`'s `exists_predual` wants (`StrongDual ℂ X ≃ₗᵢ⋆[ℂ] A` for some `X`), and this file closes each in turn.

* **Direction.** `toDual` points from `A` to the dual of its predual; `exists_predual` wants a map the other way, from the dual of some Banach space *to* `A`. This half is free: `toDual.symm : StrongDual ℂ (Predual A) ≃ₗᵢ[ℂ] A` is still linear, just reversed.

* **Linearity.** `toDual` (and hence `toDual.symm`) is linear (`≃ₗᵢ[ℂ]`); `exists_predual` wants a *conjugate*-linear identification (`≃ₗᵢ⋆[ℂ]`, notation for `LinearIsometryEquiv (starRingEnd ℂ)`). There is no canonical conjugate-linear self-map of an arbitrary Banach space, so this cannot be fixed by post- or pre-composing `toDual.symm` with some fixed conjugate-linear equivalence of `Predual A` or of `A`. Instead, `ConjSpace.lean`'s scalar-conjugation twist of the *type* of the predual supplies exactly the missing conjugate-linear step: `Phi : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] StrongDual ℂ (ConjSpace X)`, `f ↦ (x ↦ conj (f (ofConj x)))`, for any Banach space `X`. This is well-defined precisely because reinterpreting `conj ∘ f` as a function on `ConjSpace X` (rather than on `X`) turns its conjugate-linearity in `x` into honest `ConjSpace X`-linearity — the twisted scalar action absorbs the extra conjugation. `Phi` is bijective (inverse `Psi`, the same construction run the other way) and isometric (postcomposing with `starRingEnd ℂ`, itself an isometry, does not change the operator norm).

Chaining `Phi.symm : StrongDual ℂ (ConjSpace (Predual A)) ≃ₗᵢ⋆[ℂ] StrongDual ℂ (Predual A)` with `toDual.symm : StrongDual ℂ (Predual A) ≃ₗᵢ[ℂ] A` composes a conjugate-linear equivalence with a linear one, giving a conjugate-linear equivalence overall (Mathlib's `RingHomCompTriple`/ `RingHomInvPair` instances for `starRingEnd ℂ` handle the bookkeeping); this is exactly the witness `exists_predual` needs, with `X := ConjSpace (Predual A)`.

One further subtlety, purely about universes, is worth recording: `WStarAlgebraStructure A`'s `Predual A` is universe-polymorphic *independently* of `A` (`WStarAlgebraStructure.{u, v}`), while Mathlib's `WStarAlgebra (M : Type u)` demands its predual witness live in the *same* universe `u` as `M` (`exists_predual : ∃ (X : Type u), ...`). `toWStarAlgebra` below is therefore stated for `WStarAlgebraStructure.{u, u} A`, pinning the predual to `A`'s own universe. Every concrete instance in this development (`WStarAlgebra/Concrete.lean`'s trace-class predual included) already satisfies this, so it costs nothing in practice; it is only a genuine restriction for a hypothetical `WStarAlgebraStructure A` whose chosen predual deliberately lives in a strictly larger universe than `A`, which no construction here does.

Main declarations

- `Phi`, `Psi` : the mutually inverse conjugate-linear maps `StrongDual ℂ X → StrongDual ℂ (ConjSpace X)` and back, for any Banach space `X`. - `PhiEquiv : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] StrongDual ℂ (ConjSpace X)` : the bundled conjugate-linear isometric equivalence. - `WStarAlgebraStructure.toWStarAlgebra` : the theorem closing the connection, `WStarAlgebraStructure A → WStarAlgebra A` (universe-pinned as above).

The conjugate-linear self-duality `Phi` of the strong dual, via `ConjSpace`

Closing the connection to Mathlib's `WStarAlgebra`

15 declarations

definition

Linear map $\text{PhiLM}(f) : \bar{X} \to \mathbb{C}$ defined by $x \mapsto \overline{f(x)}$

#PhiLM

For a continuous linear functional $f$ in the strong dual $X^*$ of a complex Banach space $X$ , the map $\text{PhiLM}(f)$ is the $\mathbb{C}$ -linear map from the conjugate space $\bar{X}$ (denoted as `ConjSpace X`) to $\mathbb{C}$ defined by $x \mapsto \overline{f(x)}$ . Here, the complex conjugation $\overline{f(x)}$ ensures that the map is linear with respect to the twisted scalar action on $\bar{X}$ .

definition

Map $\Phi: X^* \to \bar{X}^*$ sending $f$ to $x \mapsto \overline{f(x)}$

#Phi

Let $X$ be a complex Banach space and $X^*$ be its strong dual. The function $\Phi$ maps a continuous linear functional $f \in X^*$ to a continuous linear functional on the conjugate space $\bar{X}$ (denoted `ConjSpace X`), such that for any $x \in \bar{X}$ , its value is given by $\Phi(f)(x) = \overline{f(x)}$ . The continuity of $\Phi(f)$ is guaranteed by the bound $\|\Phi(f)\| \le \|f\|$ , which follows from the fact that complex conjugation is an isometry.

theorem

$\Phi(f)(x) = \overline{f(x)}$

#Phi_apply

Let $X$ be a complex Banach space, and let $X^*$ be its strong dual. Let $\bar{X}$ (denoted as `ConjSpace X`) be the conjugate space of $X$ . For any continuous linear functional $f \in X^*$ and any element $x \in \bar{X}$ , the map $\Phi: X^* \to \bar{X}^*$ satisfies the identity $\Phi(f)(x) = \overline{f(x)},$ where $\overline{\cdot}$ denotes complex conjugation.

definition

Linear map $\Psi_{LM}(g)(x) = \overline{g(x)}$ for $g \in (X_{\text{conj}})^*$

#PsiLM

Let $X$ be a complex Banach space and $X_{\text{conj}}$ be its conjugate space (the same underlying set but with scalar multiplication $\lambda \cdot x$ defined as $\bar{\lambda} x$ ). Given a continuous linear functional $g$ on $X_{\text{conj}}$ , $\Psi_{LM}(g)$ is the linear map from $X$ to $\mathbb{C}$ defined by $\Psi_{LM}(g)(x) = \overline{g(x)}$ for all $x \in X$ , where $\overline{\cdot}$ denotes the complex conjugate.

definition

Continuous linear map $\Psi(g)(x) = \overline{g(x)}$ for $g \in (X_{\text{conj}})^*$

#Psi

Let $X$ be a complex Banach space and $X_{\text{conj}}$ be its conjugate space (the space with the same underlying set but where scalar multiplication is twisted by complex conjugation). For any continuous linear functional $g \in (X_{\text{conj}})^*$ , $\Psi(g)$ is the continuous linear functional on $X$ defined by $\Psi(g)(x) = \overline{g(x)}$ for all $x \in X$ , where $\overline{\cdot}$ denotes the complex conjugate.

theorem

$\Psi(g)(x) = \overline{g(x)}$

#Psi_apply

Let $X$ be a complex Banach space and $X_{\text{conj}}$ be its conjugate space (the space sharing the same underlying set as $X$ but where scalar multiplication is twisted by complex conjugation). For any continuous linear functional $g$ in the strong dual of $X_{\text{conj}}$ and for any $x \in X$ , the application of the map $\Psi(g)$ to $x$ is given by $\Psi(g)(x) = \overline{g(x)}$ , where $\overline{\cdot}$ denotes the complex conjugate.

theorem

$\Psi(\Phi(f)) = f$

#Psi_Phi

Let $X$ be a complex Banach space and $X^*$ be its strong dual. Let $\bar{X}$ denote the conjugate space of $X$ (the space with the same underlying set but with scalar multiplication twisted by complex conjugation). For any continuous linear functional $f \in X^*$ , the composition of the maps $\Phi: X^* \to \bar{X}^*$ and $\Psi: \bar{X}^* \to X^*$ (both defined by taking the complex conjugate of the functional's value) satisfies $\Psi(\Phi(f)) = f$ .

theorem

$\Phi(\Psi(g)) = g$ for $g \in \bar{X}^*$

#Phi_Psi

Let $X$ be a complex Banach space and $\bar{X}$ be its conjugate space (the space with the same elements as $X$ but where scalar multiplication is defined by $\lambda \cdot x = \bar{\lambda} x$ ). Let $X^*$ and $\bar{X}^*$ be their respective strong duals. Given the map $\Psi: \bar{X}^* \to X^*$ defined by $(\Psi g)(x) = \overline{g(x)}$ and the map $\Phi: X^* \to \bar{X}^*$ defined by $(\Phi f)(x) = \overline{f(x)}$ , then for any continuous linear functional $g \in \bar{X}^*$ , it holds that $\Phi(\Psi(g)) = g$ .

definition

Conjugate-linear map $\Phi: X^* \to \bar{X}^*$ mapping $f \mapsto (x \mapsto \overline{f(x)})$

#PhiLM'

Let $X$ be a complex Banach space, $X^*$ its continuous dual space, and $\bar{X}$ its conjugate space (represented by `ConjSpace X`). The mapping $\Phi$ is the conjugate-linear map from $X^*$ to $\bar{X}^*$ defined by $\Phi(f)(x) = \overline{f(x)}$ for all $f \in X^*$ and $x \in \bar{X}$ . This map is additive and satisfies the conjugate-linear property $\Phi(c \cdot f) = \bar{c} \cdot \Phi(f)$ for scalars $c \in \mathbb{C}$ .

theorem

$\|\Phi(f)\| \leq \|f\|$

#norm_Phi_le

Let $X$ be a complex Banach space and $X^*$ its strong dual. Let $\Phi : X^* \to \bar{X}^*$ be the map that sends a continuous linear functional $f \in X^*$ to a functional on the conjugate space $\bar{X}$ defined by $\Phi(f)(x) = \overline{f(x)}$ . Then for any $f \in X^*$ , the operator norm of the image is bounded by the norm of the original functional, such that $\|\Phi(f)\| \leq \|f\|$ .

theorem

$\|\Psi(g)\| \leq \|g\|$

#norm_Psi_le

Let $X$ be a complex Banach space and $X_{\text{conj}}$ be its conjugate space (the space with the same underlying set but where scalar multiplication is twisted by complex conjugation). For any continuous linear functional $g \in (X_{\text{conj}})^*$ , let $\Psi(g)$ be the continuous linear functional on $X$ defined by $\Psi(g)(x) = \overline{g(x)}$ . The operator norm of $\Psi(g)$ is less than or equal to the operator norm of $g$ , i.e., $\|\Psi(g)\| \le \|g\|$ .

theorem

$\|\Phi(f)\| = \|f\|$ for the conjugate-linear duality map $\Phi$

#norm_Phi_eq

Let $X$ be a complex Banach space and $X^*$ be its strong dual. Let $\bar{X}$ denote the conjugate space of $X$ (the space with the same underlying additive group but with scalar multiplication twisted by complex conjugation). For any continuous linear functional $f \in X^*$ , let $\Phi(f)$ be the functional on $\bar{X}$ defined by $\Phi(f)(x) = \overline{f(x)}$ . Then the operator norm of $\Phi(f)$ is equal to the operator norm of $f$ , i.e., $\|\Phi(f)\| = \|f\|$ .

definition

Conjugate-linear isometric embedding $\Phi: X^* \to \bar{X}^*$

#PhiLI

Let $X$ be a complex Banach space, $X^*$ its strong dual, and $\bar{X}$ its conjugate space (the space with the same underlying additive group but where scalar multiplication is twisted by complex conjugation). The mapping $\Phi : X^* \to \bar{X}^*$ is the conjugate-linear isometric embedding defined by $(\Phi f)(x) = \overline{f(x)}$ for all $f \in X^*$ and $x \in \bar{X}$ . This mapping is an isometry, meaning it preserves the operator norm: $\|\Phi(f)\| = \|f\|$ .

definition

Conjugate-linear isometric equivalence $\Phi : X^* \cong \bar{X}^*$

#PhiEquiv

Let $X$ be a complex Banach space and $X^*$ be its strong dual. Let $\bar{X}$ denote the conjugate space of $X$ (the space with the same underlying additive group but where scalar multiplication is twisted by complex conjugation). The definition $\Phi$ is the conjugate-linear isometric equivalence between $X^*$ and $\bar{X}^*$ defined by mapping each continuous linear functional $f \in X^*$ to the functional $\Phi(f)$ such that $(\Phi f)(x) = \overline{f(x)}$ for all $x \in \bar{X}$ .

theorem

`WStarAlgebraStructure A` implies `WStarAlgebra A`

#toWStarAlgebra

Let $A$ be a type in universe $u$ . If $A$ is equipped with a $W^*$ -algebra structure (the class `WStarAlgebraStructure`), which provides a chosen predual $P$ in universe $u$ and a linear isometric equivalence between $A$ and the strong dual $P^*$ , then $A$ is a $W^*$ -algebra in the sense of Mathlib (the property `WStarAlgebra A`), which requires the existence of some Banach space $X$ such that there is a conjugate-linear isometric equivalence between $X^*$ and $A$ .

PhyslibAlpha.AlgebraicFramework.WStarAlgebra.Mathlib

`WStarAlgebraStructure A` gives Mathlib's `WStarAlgebra A`

Main declarations

The conjugate-linear self-duality `Phi` of the strong dual, via `ConjSpace`

Closing the connection to Mathlib's `WStarAlgebra`

Linear map PhiLM(f):Xˉ→C\text{PhiLM}(f) : \bar{X} \to \mathbb{C}PhiLM(f):Xˉ→C defined by x↦f(x)‾x \mapsto \overline{f(x)}x↦f(x)​

Map Φ:X∗→Xˉ∗\Phi: X^* \to \bar{X}^*Φ:X∗→Xˉ∗ sending fff to x↦f(x)‾x \mapsto \overline{f(x)}x↦f(x)​

Φ(f)(x)=f(x)‾\Phi(f)(x) = \overline{f(x)}Φ(f)(x)=f(x)​

Linear map ΨLM(g)(x)=g(x)‾\Psi_{LM}(g)(x) = \overline{g(x)}ΨLM​(g)(x)=g(x)​ for g∈(Xconj)∗g \in (X_{\text{conj}})^*g∈(Xconj​)∗

Continuous linear map Ψ(g)(x)=g(x)‾\Psi(g)(x) = \overline{g(x)}Ψ(g)(x)=g(x)​ for g∈(Xconj)∗g \in (X_{\text{conj}})^*g∈(Xconj​)∗

Ψ(g)(x)=g(x)‾\Psi(g)(x) = \overline{g(x)}Ψ(g)(x)=g(x)​

Ψ(Φ(f))=f\Psi(\Phi(f)) = fΨ(Φ(f))=f

Φ(Ψ(g))=g\Phi(\Psi(g)) = gΦ(Ψ(g))=g for g∈Xˉ∗g \in \bar{X}^*g∈Xˉ∗

Conjugate-linear map Φ:X∗→Xˉ∗\Phi: X^* \to \bar{X}^*Φ:X∗→Xˉ∗ mapping f↦(x↦f(x)‾)f \mapsto (x \mapsto \overline{f(x)})f↦(x↦f(x)​)

∥Φ(f)∥≤∥f∥\|\Phi(f)\| \leq \|f\|∥Φ(f)∥≤∥f∥

∥Ψ(g)∥≤∥g∥\|\Psi(g)\| \leq \|g\|∥Ψ(g)∥≤∥g∥

∥Φ(f)∥=∥f∥\|\Phi(f)\| = \|f\|∥Φ(f)∥=∥f∥ for the conjugate-linear duality map Φ\PhiΦ

Conjugate-linear isometric embedding Φ:X∗→Xˉ∗\Phi: X^* \to \bar{X}^*Φ:X∗→Xˉ∗

Conjugate-linear isometric equivalence Φ:X∗≅Xˉ∗\Phi : X^* \cong \bar{X}^*Φ:X∗≅Xˉ∗

`WStarAlgebraStructure A` implies `WStarAlgebra A`

Linear map $\text{PhiLM}(f) : \bar{X} \to \mathbb{C}$ defined by $x \mapsto \overline{f(x)}$

Map $\Phi: X^* \to \bar{X}^*$ sending $f$ to $x \mapsto \overline{f(x)}$

$\Phi(f)(x) = \overline{f(x)}$

Linear map $\Psi_{LM}(g)(x) = \overline{g(x)}$ for $g \in (X_{\text{conj}})^*$

Continuous linear map $\Psi(g)(x) = \overline{g(x)}$ for $g \in (X_{\text{conj}})^*$

$\Psi(g)(x) = \overline{g(x)}$

$\Psi(\Phi(f)) = f$

$\Phi(\Psi(g)) = g$ for $g \in \bar{X}^*$

Conjugate-linear map $\Phi: X^* \to \bar{X}^*$ mapping $f \mapsto (x \mapsto \overline{f(x)})$

$\|\Phi(f)\| \leq \|f\|$

$\|\Psi(g)\| \leq \|g\|$

$\|\Phi(f)\| = \|f\|$ for the conjugate-linear duality map $\Phi$

Conjugate-linear isometric embedding $\Phi: X^* \to \bar{X}^*$

Conjugate-linear isometric equivalence $\Phi : X^* \cong \bar{X}^*$