WStarAlgebras have Unique Preduals

8. Unitality and Other Topologies🔗

The results in this chapter are not needed for the proof that a W^*-algebra has a unique predual, and nothing outside this chapter depends on them. They record parts of Sakai's development that the formalization was able to avoid, together with what has been formalized of them.

8.1. Unitality of WStarAlgebras🔗

Sakai does not assume that a W^*-algebra has a unit; it is a consequence of the definition (Lemma 8.1.8), via the Krein–Milman theorem and the following characterization of unital C^*-algebras by the extreme points of their unit balls. The formalization assumes a unit from the outset, and these results justify that choice.

Lemma8.1.1
Statement uses 2
Statement dependency previews
Preview
Lemma 2.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

In a unital C^*-algebra \mathcal{A}, the identity 1 is an extreme point of the closed unit sphere S.

Lean code for Lemma8.1.1●1 theorem
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem CStarAlgebra.one_mem_extremePoints_unitClosedBall.{u_1} {A : Type u_1}
  [CStarAlgebra A] : 1 ∈ Set.extremePoints ℝ (Metric.closedBall 0 1)
    theorem CStarAlgebra.one_mem_extremePoints_unitClosedBall.{u_1}
  {A : Type u_1} [CStarAlgebra A] :
  1 ∈
    Set.extremePoints ℝ
      (Metric.closedBall 0 1)
Proof for Lemma 8.1.1
uses 0

Suppose a, b \in S and 1 = \frac{a + b}{2}. Then, since 1 = 1^*, we have 1 = \frac{a^* + b^*}{2} and one checks that 1 = \frac{c + d}{2}, where c = \frac{a + a^*}{2} and d = \frac{b + b^*}{2}. Now d = 2 - c and so d and c commute and each are self-adjoint (hence normal), and therefore C^*\{1, d, c\} is commutative and can be identified with C(K) for a compact Hausdorff space K. The self-adjointness of c and d, the triangle inequality and Lemma 2.1.2 imply that the ranges of the associated functions f, g are in [-1, 1]. In order for f(t) + g(t) = 2 for all t \in K it must be that f(t) and g(t) are always 1, and thus c = d = 1. Now 2 = 2c = a + a^* and so a = 2 - a^*, hence a is normal and so the unital C^*-subalgebra generated by a is commutative. Again represent the unital C^*-algebra as C(K) for some compact Hausdorff K. Let f be the function corresponding to a. We have \Re(f)(t) = 1 for all t, and hence \Re(f)(t)^2 = |f(t)| = 1 for all t and \Im(f)(t) = 0 for all t, and therefore a = 1.

Lemma8.1.2
uses 1used by 1XL∃∀N

Let x be an extreme point of the norm unit ball of a C^*-algebra \mathcal{A}, so that the C^*-subalgebra generated by x^* x is identified with C_0(\Omega) as in Corollary 2.1.4. There exists a sequence (y_n) of positive elements in C_0(\Omega) with \|y_n\| \le 1 for all n, such that \|(x^* x) y_n - x^* x\| \to 0 and \|(x^* x) y_n^2 - x^* x\| \to 0 as n \to \infty.

Lemma8.1.3
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

If x is an extreme point of the norm unit ball of a C^*-algebra \mathcal{A}, then x^* x is a projection. That is, x is a partial isometry.

Lean code for Lemma8.1.3●2 theorems
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A] {a : A}
  (ha : a ∈ Set.extremePoints ℝ (Metric.closedBall 0 1)) :
  IsStarProjection (star a * a)
    theorem isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A]
  {a : A}
  (ha :
    a ∈
      Set.extremePoints ℝ
        (Metric.closedBall 0 1)) :
  IsStarProjection (star a * a)
    Every extreme point in the closed unit ball of a `NonUnitalCStarAlgebra` is a
partial isometry (in other words, `star a * a` is a projection).
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A] {a : A}
  (ha : a ∈ Set.extremePoints ℝ (Metric.closedBall 0 1)) :
  IsStarProjection (a * star a)
    theorem isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A]
  {a : A}
  (ha :
    a ∈
      Set.extremePoints ℝ
        (Metric.closedBall 0 1)) :
  IsStarProjection (a * star a)
    Every extreme point in the closed unit ball of a `NonUnitalCStarAlgebra` is a
partial isometry (in other words, `a * star a` is a projection).
Theorem8.1.4
Statement uses 2
Statement dependency previews
Preview
Lemma 8.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

(Sakai 1.6.1) A C^*-algebra is unital if and only if its closed unit ball has an extreme point.

Lean code for Theorem8.1.4●3 theorems
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem CStarAlgebra.isUnital_iff.{u_2} {A : Type u_2}
  [NonUnitalCStarAlgebra A] :
  IsUnital A ↔ (Set.extremePoints ℝ (Metric.closedBall 0 1)).Nonempty
    theorem CStarAlgebra.isUnital_iff.{u_2}
  {A : Type u_2}
  [NonUnitalCStarAlgebra A] :
  IsUnital A ↔
    (Set.extremePoints ℝ
        (Metric.closedBall 0 1)).Nonempty
    A C⋆-algebra is unital iff there exists an extreme point of the closed unit ball.

To upgrade a non-unital C⋆-algebra to a unital one, use `IsUnital.toCStarAlgebra`.
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem CStarAlgebra.mul_ofExtremePtOne.{u_2} {A : Type u_2}
  [NonUnitalCStarAlgebra A] {x : A}
  (hx : x ∈ Set.extremePoints ℝ (Metric.closedBall 0 1)) (a : A) :
  a * (star x * x + x * star x - x * star x * (star x * x)) = a
    theorem CStarAlgebra.mul_ofExtremePtOne.{u_2}
  {A : Type u_2} [NonUnitalCStarAlgebra A]
  {x : A}
  (hx :
    x ∈
      Set.extremePoints ℝ
        (Metric.closedBall 0 1))
  (a : A) :
  a *
      (star x * x + x * star x -
        x * star x * (star x * x)) =
    a
    When `x` is an extreme point of the closed unit ball in an a priori non-unital C⋆-algebra,
then `star x * x + x * star x - x * star x * star x * x` is a right identity.
(See also `CStarAlgebra.ofExtremePtOne_mul` for the left identity.)
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem CStarAlgebra.ofExtremePtOne_mul.{u_2} {A : Type u_2}
  [NonUnitalCStarAlgebra A] {x : A}
  (hx : x ∈ Set.extremePoints ℝ (Metric.closedBall 0 1)) (a : A) :
  (star x * x + x * star x - x * star x * (star x * x)) * a = a
    theorem CStarAlgebra.ofExtremePtOne_mul.{u_2}
  {A : Type u_2} [NonUnitalCStarAlgebra A]
  {x : A}
  (hx :
    x ∈
      Set.extremePoints ℝ
        (Metric.closedBall 0 1))
  (a : A) :
  (star x * x + x * star x -
        x * star x * (star x * x)) *
      a =
    a
    When `x` is an extreme point of the closed unit ball in an a priori non-unital C⋆-algebra,
then `star x * x + x * star x - x * star x * star x * x` is a left identity.
(See also `CStarAlgebra.mul_ofExtremePtOne` for the right identity.)
Proposition8.1.5
uses 1used by 1✓L∃∀N
Tagsmathlib

(Sakai 1.6.2) Let P be the set of positive elements in a C^*-algebra \mathcal{A} with unit sphere S. Then the extreme points of P \cap S are the projections of \mathcal{A}.

Lean code for Proposition8.1.5●1 theorem
  • theoremdefined in Mathlib/Analysis/CStarAlgebra/Extreme.lean
    complete
    theorem isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A]
  [StarOrderedRing A] {e : A} :
  IsStarProjection e ↔
    e ∈ Set.extremePoints ℝ ({x | 0 ≤ x} ∩ Metric.closedBall 0 1)
    theorem isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A]
  [PartialOrder A] [StarOrderedRing A]
  {e : A} :
  IsStarProjection e ↔
    e ∈
      Set.extremePoints ℝ
        ({x | 0 ≤ x} ∩
          Metric.closedBall 0 1)
    The star projections in a non-unital C⋆-algebra are exactly the extreme points of
the nonnegative closed unit ball.
Proposition8.1.6
uses 1used by 1✓L∃∀N

(Sakai 1.6.3) Let \mathcal{A}^s be the set of self-adjoint elements in a C^*-algebra \mathcal{A} with unit sphere S. Then the set of extreme points of \mathcal{A}^s \cap S is the set of all self-adjoint unitary elements of \mathcal{A}.

Lean code for Proposition8.1.6●2 theorems
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary.{u_1}
  {A : Type u_1} [CStarAlgebra A] {e : A} :
  e ∈
      Set.extremePoints ℝ
        {x | IsSelfAdjoint x ∧ x ∈ Metric.closedBall 0 1} ↔
    IsSelfAdjoint e ∧ e ∈ unitary A
    theorem mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary.{u_1}
  {A : Type u_1} [CStarAlgebra A]
  {e : A} :
  e ∈
      Set.extremePoints ℝ
        {x |
          IsSelfAdjoint x ∧
            x ∈ Metric.closedBall 0 1} ↔
    IsSelfAdjoint e ∧ e ∈ unitary A
    The extreme points of the self-adjoint closed unit ball is exactly the set of self-adjoint
unitaries.
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary.{u_1}
  {A : Type u_1} [CStarAlgebra A] {e : ↥(selfAdjoint A)} :
  e ∈ Set.extremePoints ℝ (Metric.closedBall 0 1) ↔ ↑e ∈ unitary A
    theorem selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary.{u_1}
  {A : Type u_1} [CStarAlgebra A]
  {e : ↥(selfAdjoint A)} :
  e ∈
      Set.extremePoints ℝ
        (Metric.closedBall 0 1) ↔
    ↑e ∈ unitary A
    An alternate statement for
`mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary`.
Theorem8.1.7
uses 0used by 1✓L∃∀N
Tagsmathlib

(Krein–Milman) A nonempty compact convex subset of a Hausdorff locally convex space has an extreme point; indeed, it is the closed convex hull of its extreme points.

Lean code for Theorem8.1.7●2 theorems
  • theoremdefined in Mathlib/Analysis/Convex/KreinMilman.lean
    complete
    theorem IsCompact.extremePoints_nonempty.{u_1} {E : Type u_1} [AddCommGroup E]
  [Module ℝ E] [TopologicalSpace E] [T2Space E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s)
  (hsnemp : s.Nonempty) : (Set.extremePoints ℝ s).Nonempty
    theorem IsCompact.extremePoints_nonempty.{u_1}
  {E : Type u_1} [AddCommGroup E]
  [Module ℝ E] [TopologicalSpace E]
  [T2Space E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] {s : Set E}
  (hscomp : IsCompact s)
  (hsnemp : s.Nonempty) :
  (Set.extremePoints ℝ s).Nonempty
    **Krein-Milman lemma**: In an LCTVS, any nonempty compact set has an extreme point.
  • theoremdefined in Mathlib/Analysis/Convex/KreinMilman.lean
    complete
    theorem closure_convexHull_extremePoints.{u_1} {E : Type u_1} [AddCommGroup E]
  [Module ℝ E] [TopologicalSpace E] [T2Space E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s)
  (hAconv : Convex ℝ s) :
  closure ((convexHull ℝ) (Set.extremePoints ℝ s)) = s
    theorem closure_convexHull_extremePoints.{u_1}
  {E : Type u_1} [AddCommGroup E]
  [Module ℝ E] [TopologicalSpace E]
  [T2Space E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] {s : Set E}
  (hscomp : IsCompact s)
  (hAconv : Convex ℝ s) :
  closure
      ((convexHull ℝ)
        (Set.extremePoints ℝ s)) =
    s
    **Krein-Milman theorem**: In an LCTVS, any compact convex set is the closure of the convex hull
of its extreme points.
Lemma8.1.8
Statement uses 4
Statement dependency previews
Preview
Theorem 1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Every W^*-algebra is unital, even if it is not assumed to be so in Definition 2.1.6.

Lean code for Lemma8.1.8●3 theorems
  • theoremdefined in LeanOA/CStarAlgebra/Extreme.lean
    complete
    theorem CStarAlgebra.isUnital_iff.{u_2} {A : Type u_2}
  [NonUnitalCStarAlgebra A] :
  IsUnital A ↔ (Set.extremePoints ℝ (Metric.closedBall 0 1)).Nonempty
    theorem CStarAlgebra.isUnital_iff.{u_2}
  {A : Type u_2}
  [NonUnitalCStarAlgebra A] :
  IsUnital A ↔
    (Set.extremePoints ℝ
        (Metric.closedBall 0 1)).Nonempty
    A C⋆-algebra is unital iff there exists an extreme point of the closed unit ball.

To upgrade a non-unital C⋆-algebra to a unital one, use `IsUnital.toCStarAlgebra`.
  • theoremdefined in Mathlib/Analysis/Convex/KreinMilman.lean
    complete
    theorem IsCompact.extremePoints_nonempty.{u_1} {E : Type u_1} [AddCommGroup E]
  [Module ℝ E] [TopologicalSpace E] [T2Space E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] {s : Set E} (hscomp : IsCompact s)
  (hsnemp : s.Nonempty) : (Set.extremePoints ℝ s).Nonempty
    theorem IsCompact.extremePoints_nonempty.{u_1}
  {E : Type u_1} [AddCommGroup E]
  [Module ℝ E] [TopologicalSpace E]
  [T2Space E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] {s : Set E}
  (hscomp : IsCompact s)
  (hsnemp : s.Nonempty) :
  (Set.extremePoints ℝ s).Nonempty
    **Krein-Milman lemma**: In an LCTVS, any nonempty compact set has an extreme point.
  • theoremdefined in LeanOA/Ultraweak/Basic.lean
    complete
    theorem Ultraweak.isCompact_closedBall.{u_1, u_2, u_3} (𝕜 : Type u_1)
  {M : Type u_2} (P : Type u_3) [RCLike 𝕜] [NormedAddCommGroup M]
  [NormedAddCommGroup P] [NormedSpace 𝕜 M] [NormedSpace 𝕜 P]
  [Predual 𝕜 M P] (x : M) (r : ℝ) :
  IsCompact (ofUltraweak ⁻¹' Metric.closedBall x r)
    theorem Ultraweak.isCompact_closedBall.{u_1, u_2,
    u_3}
  (𝕜 : Type u_1) {M : Type u_2}
  (P : Type u_3) [RCLike 𝕜]
  [NormedAddCommGroup M]
  [NormedAddCommGroup P] [NormedSpace 𝕜 M]
  [NormedSpace 𝕜 P] [Predual 𝕜 M P]
  (x : M) (r : ℝ) :
  IsCompact
    (ofUltraweak ⁻¹'
      Metric.closedBall x r)
Proof for Lemma 8.1.8
uses 0

The norm unit ball of M = (M_*)^* is convex and is compact by Theorem 1.4, and so has an extreme point by the Krein–Milman theorem (Theorem 8.1.7). By Theorem 8.1.4, the result follows.

8.2. WStarSubalgebras and the Projection Lattice🔗

Sakai shows that the projections of a W^*-algebra form a complete lattice by way of W^*-subalgebras and one-sided ideals. The proof of the main theorem only needs suprema of directed sets of projections, which Lemma 4.4 provides directly.

Corollary8.2.1
Statement uses 3
Statement dependency previews
Preview
Definition 2.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 8.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N

(Sakai 1.7.9) Let H be a subset of M and \mathcal{A} be the C^*-subalgebra of M generated by H, and let \overline{\mathcal{A}} be the \sigma(M, M_*)-closure of \mathcal{A}. Then \overline{\mathcal{A}} is a W^*-subalgebra of M; it is called the W^*-subalgebra of M generated by H. Moreover, \overline{\mathcal{A}} is commutative if \mathcal{A} is commutative.

Lemma8.2.2
uses 1used by 0XL∃∀N

A maximal abelian *-subalgebra \mathcal{A} of a W^*-algebra M is also a W^*-algebra.

Proof for Lemma 8.2.2
uses 0

By maximality, \mathcal{A} = \overline{\mathcal{A}}, and so Corollary 8.2.1 implies \mathcal{A} is a W^*-subalgebra of M.

Proposition8.2.3
Statement uses 4
Statement dependency previews
Preview
Lemma 2.2.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1XL∃∀N

(Sakai 1.10.1) Let \mathcal{L} (resp. \mathcal{R}) be a left (resp. right) \sigma(M, M_*)-closed ideal of a W^*-algebra M. Then there exists a unique projection p (resp. q) in M so that \mathcal{L} = Mp (resp. \mathcal{R} = qM).

Proof for Proposition 8.2.3
uses 0

Suppose \mathcal{L} is a \sigma-closed left ideal. By Lemma 2.2.6, \mathcal{L}^* is also \sigma-closed and \mathcal{N} = \mathcal{L} \cap \mathcal{L}^* is a \sigma-closed *-subalgebra of M, and therefore by Corollary 8.2.1 is a W^*-subalgebra of M. Let p be the identity of \mathcal{N}, which exists by Lemma 8.1.8. Since \mathcal{L} is a left ideal, xp \in \mathcal{L} for any x \in M, thus Mp \subseteq \mathcal{L}; conversely, xp = x for any x \in \mathcal{L}, since p is the identity of \mathcal{N}, thus \mathcal{L} \subseteq Mp.

If p_1 is another projection in M such that \mathcal{L} = Mp_1 then Mp = Mp_1 and p_1 = xp for some x \in M. By the self-adjointness of p_1 we have p_1 = px^* xp and therefore p_1 p = p p_1 = p_1, and therefore p_1 \le p by Lemma 4.2. We get p \le p_1 using the same argument. The claim for right ideals follows mutatis mutandis.

Proposition8.2.4
Statement uses 2
Statement dependency previews
Preview
Lemma 4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N

(Sakai 1.10.2) Let M be a W^*-algebra. Its set M^p of projections is a complete lattice with respect to \le.

Proof for Proposition 8.2.4
uses 0

Let \{e_i\}_{i \in \mathbb{I}} be any set of projections in M. Consider \mathcal{L}_1, the \sigma-closed left ideal generated by \{Me_i\}_{i \in \mathbb{I}}, and \mathcal{L}_2 = \bigcap_{i \in \mathbb{I}} Me_i. By Proposition 8.2.3 there exist projections e_1, e_2 in M so that \mathcal{L}_1 = Me_1 and \mathcal{L}_2 = Me_2. By Lemma 4.2, we know e_i \le e_1 and e_2 \le e_i for any i \in \mathbb{I}. (To prove the first of these, since e_i = xe_1 for some x \in M, we have by the self-adjointness of e_i that e_i = e_1 x^* x e_1 and so e_1 e_i = e_i e_1 = e_i and so e_i \le e_1. The other direction is analogous.)

Furthermore, if p \in M^p is another projection that is an upper bound for all the e_i then Me_1 \subseteq Mp since \mathcal{L}_1 = Me_1 is the left ideal generated by the e_i. It follows that e_1 \le p by the same calculation we just did. If p \in M^p is a lower bound for all the e_i then Mp \subseteq Me_i for every i \in \mathbb{I} and so Mp \subseteq \bigcap_i Me_i = Me_2 and we obtain p \le e_2. It follows that e_1 = \sup(e_i) and e_2 = \inf(e_i).

8.3. The Mackey and Strong Topologies🔗

Sakai's proof of Theorem 7.2.6 compares the \sigma-topology with the strong topology, through the Mackey topology. The formalization replaces this with the GNS argument of Lemma 7.2.4. The general theory of the Mackey topology is nevertheless partly formalized.

Definition8.3.1
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 8.3.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let B : E \times F \to \mathbb{K} be a pairing. The locally convex topology on E generated by the seminorms p_K(x) = \sup_{y \in K} |B(x, y)|, ranging over the \sigma(F, E)-compact absolutely convex subsets K of F, is called the Mackey topology on E, and is denoted \tau(E, F). For a W^*-algebra M this gives the Mackey topology \tau(M, M_*).

Lean code for Definition8.3.1●1 definition
  • abbrevdefined in LeanOA/Mackey.lean
    complete
    abbrev Mackey.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Type u_2
    abbrev Mackey.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Type u_2
    The Mackey toplogy on a space `E` relative to a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` is the
polar topology corresponding to all (weakly) compact absolutely convex sets in `F`.

Although it is not required for the definition, the space `F` should be equipped with the weak
topology induced by `B.flip` for any of the usual theorems to be applicable.
Theorem8.3.2
Statement uses 3
Statement dependency previews
Preview
Definition 1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

(Mackey–Arens, first half) If B separates the points of F, the Mackey topology \tau(E, F) is compatible with B.

Lean code for Theorem8.3.2●2 theorems
  • theoremdefined in LeanOA/Mackey.lean
    complete
    theorem Mackey.range_coeLM_eq_range_bilin.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [B.flip.IsWeak] [IsTopologicalAddGroup F]
  [Module ℝ F] [IsScalarTower ℝ 𝕜 F] [T1Space F] [ContinuousSMul 𝕜 F] :
  (PolarTopology.bilin B {s | IsCompact s ∧ AbsConvex 𝕜 s}).range =
    (ContinuousLinearMap.coeLM 𝕜).range
    theorem Mackey.range_coeLM_eq_range_bilin.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [B.flip.IsWeak]
  [IsTopologicalAddGroup F] [Module ℝ F]
  [IsScalarTower ℝ 𝕜 F] [T1Space F]
  [ContinuousSMul 𝕜 F] :
  (PolarTopology.bilin B
        {s |
          IsCompact s ∧
            AbsConvex 𝕜 s}).range =
    (ContinuousLinearMap.coeLM 𝕜).range
  • theoremdefined in LeanOA/Mathlib/Analysis/LocallyConvex/Bipolar.lean
    complete
    theorem Module.dualPairing_flip_polar_polar.{u_4, u_5, u_6} {𝕜 : Type u_4}
  {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [B.IsWeak] {s : Set E} (hs : AbsConvex 𝕜 s)
  (hs' : IsCompact s) (hs_non : s.Nonempty) :
  LinearMap.id.flip.polar (B.polar s) = ⇑B '' s
    theorem Module.dualPairing_flip_polar_polar.{u_4,
    u_5, u_6}
  {𝕜 : Type u_4} {E : Type u_5}
  {F : Type u_6} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace E]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [B.IsWeak]
  {s : Set E} (hs : AbsConvex 𝕜 s)
  (hs' : IsCompact s)
  (hs_non : s.Nonempty) :
  LinearMap.id.flip.polar (B.polar s) =
    ⇑B '' s
Proof for Theorem 8.3.2
uses 0

A functional continuous for \tau(E, F) is bounded by 1 on the polar of some \sigma(F, E)-compact absolutely convex set K, so it lies in the bipolar of K computed in the algebraic dual of E. A variant of Theorem 1.5 (Voigt, Topological Vector Spaces, Lemma 5.3) identifies that bipolar with K itself, since K is compact. Conversely, each B(\cdot, y) is \tau(E, F)-continuous, taking K to be the closed absolutely convex hull of \{y\}.

The second half of the Mackey–Arens theorem, that \tau(E, F) is the finest locally convex topology on E compatible with B, is not yet formalized.

Definition8.3.3
uses 1used by 1XL∃∀N

The locally convex topology on M generated by the seminorms x \mapsto \varphi(x^* x)^{1/2} ranging over positive \varphi \in M_* is called the strong topology, or s-topology, on M. We denote it by s(M, M_*).

By A \le B on topologies below, we mean that A is weaker than B.

Theorem8.3.4
Statement uses 5
Statement dependency previews
Preview
Definition 2.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1XL∃∀N

(Sakai 1.8.9) We have \sigma(M, M_*) \le s(M, M_*) \le \tau(M, M_*).

Corollary8.3.5
uses 1used by 1XL∃∀N

The \sigma-topology is equivalent to the s-topology on the unit ball of M, and hence on bounded sets.

Lemma8.3.6
Statement uses 2
Statement dependency previews
Preview
Definition 2.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N

(Sakai 1.8.10) A linear functional \rho on M is \sigma-continuous on the unit sphere (hence \sigma-continuous) if and only if it is s-continuous on the unit sphere (hence s-continuous).