Actions in Top are jointly continuous actions

Proved

QAlgorithms.Papers.Independent.Intake100.P20.actionsInTop

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $G$ be a topological group, let $X$ be any topological space, and let $n:G\times X\to X$ . The map defines an action in Top if and only if it is the scalar multiplication of an ordinary left action and is jointly continuous. Its requirements are

n(1,x)=x,\qquad n(gh,x)=n(g,n(h,x)),\qquad n:G\times X\to X\text{ continuous}.

The recovered action has exactly the given map, and neither space is assumed compact or separated. This transports the Set action correspondence to Top.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P20

Formal statement

namespace QAlgorithms.Papers.Independent.Intake100.P20

open CategoryTheory

open scoped TensorProduct Manifold ContDiff

universe u v w z

/-- PDF p. 5: actions in Top are jointly continuous ordinary actions.
There is no separation, compactness, or nonemptiness hypothesis on X. -/
theorem actionsInTop {G : Type u} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] {X : Type v} [TopologicalSpace X] (n : G × X → X) :
    (ActionDiagrams n ∧ Continuous n) ↔
      ∃ a : MulAction G X,
        (∀ g x, @SMul.smul G X a.toSMul g x = n (g, x)) ∧
        (letI : MulAction G X := a; ContinuousSMul G X) := by sorry

end QAlgorithms.Papers.Independent.Intake100.P20

Source

Group Objects and Internal Categories, arXiv:math/0212065v1, PDF p. 5, §1, Group Actions

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For any group $G$ equipped with a topology making multiplication and inversion continuous, any topological space $X$ , and any function $n:G\times X\to X$ , the conjunction of joint continuity of $n$ and the equations

n(1,x)=x,\qquad n(ab,x)=n(a,n(b,x))

for every $a,b\in G$ and $x\in X$ holds if and only if there exists a monoid action of $G$ on $X$ such that $g\cdot x=n(g,x)$ for every $g\in G$ and $x\in X$ , and the resulting scalar operation $G\times X\to X$ is jointly continuous. The type $X$ may be empty; then the action equations are vacuous and the function from $G\times X$ is continuous.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph