Diagrammatic actions are ordinary left actions

Proved

QAlgorithms.Papers.Independent.Intake100.P20.actionsInSet

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

prove2quantum

Let $M$ be a monoid (in particular a group), let $X$ be any set, and fix $n:M\times X\to X$ . The diagrammatic action axioms are exactly

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

They hold if and only if there is an ordinary left $M$ -action whose scalar multiplication is $a\cdot x=n(a,x)$ . The correspondence preserves the actual action map. This includes the source's monoid extension on page 5 and permits the empty set $X$ .

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 pp. 4–5: diagrammatic actions in Set are ordinary left actions,
preserving the given map. As the source observes, this includes monoids.
The type X is allowed to be empty. -/
theorem actionsInSet {M : Type u} [Monoid M] {X : Type v} (n : M × X → X) :
    ActionDiagrams n ↔
      ∃ a : MulAction M X, ∀ g x, @SMul.smul M X a.toSMul g x = n (g, x) := by sorry

end QAlgorithms.Papers.Independent.Intake100.P20

Source

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

Read-back

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

For any monoid $M$ , any type $X$ , and any function $n:M\times X\to X$ , the equations

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

for every $a,b\in M$ and $x\in X$ hold if and only if there exists a monoid action of $M$ on $X$ whose scalar operation satisfies $g\cdot x=n(g,x)$ for every $g\in M$ and $x\in X$ . The type $X$ may be empty, in which case these universally quantified equations are vacuous.

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