Mission

A complex semigroup approach to group algebras of infinite dimensional Lie groupsResearch Paper

Motivation

A host algebra of a topological group G is a C^-algebra whose representations are in one-to-one correspondence with certain continuous unitary representations of G. In this paper we present an approach to host algebras for infinite dimensional Lie groups which is based on complex involutive semigroups. Any locally bounded absolute value αon such a semigroup S leads in a natural way to a C^-algebra C^(S,α), and we describe a setting which permits us to conclude that this C^-algebra is a host algebra for a Lie group G. We further explain how to attach to any such host algebra an invariant weak-*-closed convex set in the dual of the Lie algebra of G enjoying certain nice convex geometric properties. If G is the additive group of a locally convex space, we describe all host algebras arising this way. The general non-commutative case is left for the future.

This mission is the statement-level formalization of A complex semigroup approach to group algebras of infinite dimensional Lie groups (arXiv:0709.1062v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 4.1 (Proposition 4.1, PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

18 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 1.5: Canonical weighted semigroup C*-completion and its delta map (hard)
Lemma 1.8: Complex locally convex manifold holomorphy into operator-norm Banach spaces (hard)
Proposition 2.3: Holomorphic semigroup multiplier monoid and canonical C*-completion (hard)
Proposition 2.9: Locally exponential complex Lie groups with real-form conjugation and host axioms (hard)
Proposition 2.19: Constructed host-semigroup action and host-algebra H1/H2 (hard)
Example 2.10: Complexified locally convex tube with its actual translation host structure (hard)
Remark 3.1: Full locally compact group C*-algebra and strict integrated-action correspondence (hard)
Remark 3.3: Finite-dimensional strict smoothness through genuine Lie orbit maps (hard)
Remark 3.5: Smooth-vector transport by canonical multiplier representations (hard)
Lemma 3.6: Derived operators on the actual smooth domain, unbounded adjoints and generators (hard)
Lemma 3.7: Momentum set and spectrum of the unbounded selfadjoint Stone generator (hard)
Proposition 3.10: Spectral quotient factorization, smooth-state momentum and strict half-plane extension (hard)
Remark 3.11: Continuous multiplier subalgebra and induced holomorphic half-plane extension (hard)
Proposition 3.12: Canonical host momentum support and continuous Exp (hard)
Lemma 4.3: Convention for a compact equicontinuous base of the zero cone (source-ambiguity)
Theorem 5.1: Canonical tube completion and character isomorphism with C0(C) (hard)
Tube classification, unnumbered: All-tube character classification and host representation correspondence (hard)
Theorem 6.2: Full group C*-quotient and momentum-annihilator quotient with polar diffeomorphism (hard)

Selected references

A complex semigroup approach to group algebras of infinite dimensional Lie groups, arXiv:0709.1062v1, https://arxiv.org/abs/0709.1062v1

Goal · Proposition 4.1

OPEN

namespace QAlgorithms.Papers.Independent.Intake100.P13

open Set Filter Topology

noncomputable section

universe u v w

/-- Proposition 4.1, PDF p. 24: all four clauses, including sequence
witnesses and topological boundedness. Local convexity is not assumed.
The translation set is computed in the statement: the accepted recession
constant requires a normed space and cannot express this general TVS case. -/
theorem proposition_4_1
    {V : Type u} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V]
    [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [T2Space V]
    (C : Set V) (hC : C.Nonempty) (hClosed : IsClosed C) (hConvex : Convex ℝ C) :
    let R : Set V := {x | ∀ c ∈ C, c + x ∈ C}
    (IsClosed (R) ∧ Convex ℝ (R) ∧
      ∀ (t : ℝ), 0 ≤ t → ∀ x ∈ R, t • x ∈ R) ∧
    R = {x | ∃ (t : ℕ → ℝ) (c : ℕ → V),
      (∀ n, c n ∈ C) ∧ Tendsto t atTop (𝓝 0) ∧ (∀ n, 0 ≤ t n) ∧
        Tendsto (fun n => t n • c n) atTop (𝓝 x)} ∧
    (∀ c ∈ C, ∀ x : V,
      (∀ t : ℝ, 0 ≤ t → c + t • x ∈ C) → x ∈ R) ∧
    (Bornology.IsVonNBounded ℝ C → R = {0}) := by sorry

end

end QAlgorithms.Papers.Independent.Intake100.P13

Let $V$ be a Hausdorff real topological vector space and let $C\subseteq V$ be nonempty, closed and convex. Define its recession set by

\operatorname{lim}(C)=\{v\in V: C+v\subseteq C\}.

Then the following four assertions hold.

The set $\operatorname{lim}(C)$ is a closed convex cone.
A vector $v$ belongs to $\operatorname{lim}(C)$ if and only if there are sequences $c_n\in C$ and $t_n\ge0$ with $t_n\to0$ and $t_nc_n\to v$ in the topology of $V$ .
If $c\in C$ and $c+tx\in C$ for every real $t\ge0$ , then $x\in\operatorname{lim}(C)$ .
If $C$ is bounded in the topological vector space sense, then $\operatorname{lim}(C)=\{0\}$ .

This describes recession directions without requiring a norm, local convexity, completeness, or a sequential description of the topology.

Frontier · Open leaf nodes

Recent activity

Mission

A complex semigroup approach to group algebras of infinite dimensional Lie groups

Goal

Frontier · Open leaf nodes

Recent activity

A complex semigroup approach to group algebras of infinite dimensional Lie groupsResearch Paper

Motivation

What is formalized

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

18 results of the paper are not stated yet, because the library lacks an interface they need:

Theorem 1.5: Canonical weighted semigroup C*-completion and its delta map (hard)
Lemma 1.8: Complex locally convex manifold holomorphy into operator-norm Banach spaces (hard)
Proposition 2.3: Holomorphic semigroup multiplier monoid and canonical C*-completion (hard)
Proposition 2.9: Locally exponential complex Lie groups with real-form conjugation and host axioms (hard)
Proposition 2.19: Constructed host-semigroup action and host-algebra H1/H2 (hard)
Example 2.10: Complexified locally convex tube with its actual translation host structure (hard)
Remark 3.1: Full locally compact group C*-algebra and strict integrated-action correspondence (hard)
Remark 3.3: Finite-dimensional strict smoothness through genuine Lie orbit maps (hard)
Remark 3.5: Smooth-vector transport by canonical multiplier representations (hard)
Lemma 3.6: Derived operators on the actual smooth domain, unbounded adjoints and generators (hard)
Lemma 3.7: Momentum set and spectrum of the unbounded selfadjoint Stone generator (hard)
Proposition 3.10: Spectral quotient factorization, smooth-state momentum and strict half-plane extension (hard)
Remark 3.11: Continuous multiplier subalgebra and induced holomorphic half-plane extension (hard)
Proposition 3.12: Canonical host momentum support and continuous Exp (hard)
Lemma 4.3: Convention for a compact equicontinuous base of the zero cone (source-ambiguity)
Theorem 5.1: Canonical tube completion and character isomorphism with C0(C) (hard)
Tube classification, unnumbered: All-tube character classification and host representation correspondence (hard)
Theorem 6.2: Full group C*-quotient and momentum-annihilator quotient with polar diffeomorphism (hard)

Selected references

A complex semigroup approach to group algebras of infinite dimensional Lie groups, arXiv:0709.1062v1, https://arxiv.org/abs/0709.1062v1

namespace QAlgorithms.Papers.Independent.Intake100.P13 open Set Filter Topology noncomputable section universe u v w /-- Proposition 4.1, PDF p. 24: all four clauses, including sequence witnesses and topological boundedness. Local convexity is not assumed. The translation set is computed in the statement: the accepted recession constant requires a normed space and cannot express this general TVS case. -/ theorem proposition_4_1 {V : Type u} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [T2Space V] (C : Set V) (hC : C.Nonempty) (hClosed : IsClosed C) (hConvex : Convex ℝ C) : let R : Set V := {x | ∀ c ∈ C, c + x ∈ C} (IsClosed (R) ∧ Convex ℝ (R) ∧ ∀ (t : ℝ), 0 ≤ t → ∀ x ∈ R, t • x ∈ R) ∧ R = {x | ∃ (t : ℕ → ℝ) (c : ℕ → V), (∀ n, c n ∈ C) ∧ Tendsto t atTop (𝓝 0) ∧ (∀ n, 0 ≤ t n) ∧ Tendsto (fun n => t n • c n) atTop (𝓝 x)} ∧ (∀ c ∈ C, ∀ x : V, (∀ t : ℝ, 0 ≤ t → c + t • x ∈ C) → x ∈ R) ∧ (Bornology.IsVonNBounded ℝ C → R = {0}) := by sorry end end QAlgorithms.Papers.Independent.Intake100.P13