Tensor actions give left modules

Proved

QAlgorithms.Papers.Independent.Intake100.P20.tensorActionsGiveModules

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

prove2quantum

Let $(M,m,e)$ be a tensor monoid in abelian groups, and give $M$ the ring structure with $xy=m(x\otimes y)$ and $1=e(1)$ . Let $A$ be an abelian group and $n:M\otimes_{\mathbb Z}A\to A$ a $\mathbb Z$ -linear map satisfying the monoidal unit and action associativity diagrams. There is a left $M$ -module structure on the same additive group $A$ , with

r\cdot a=n(r\otimes a).

The unit and associativity requirements are $n(e(1)\otimes a)=a$ and $n(m(r\otimes s)\otimes a)=n(r\otimes n(s\otimes a))$ . Tensor linearity supplies additivity in each argument, so both distributivity laws belong to the resulting module. This uses the ring constructed from the given monoid.

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: a tensor action makes the SAME abelian group a left module
 over the ring computed from the given monoid. Scalar multiplication is the
 given tensor map on pure tensors, so neither distributivity can be dropped. -/
theorem tensorActionsGiveModules (M : ModuleCat.{0} ℤ) [MonObj M]
    (A : Type v) [AddCommGroup A] (n : TensorProduct ℤ M A →ₗ[ℤ] A)
    (h : TensorActionDiagrams M A n) :
    letI : Ring M := tensorRing M
    ∃ a : Module M A, ∀ r x, @SMul.smul M A a.toSMul r x = n (r ⊗ₜ[ℤ] 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 small $\mathbb Z$ -module $M$ equipped with a tensor monoid object structure with linear unit $\eta:\mathbb Z\to M$ and linear multiplication $\mu:M\otimes_{\mathbb Z}M\to M$ , any additive commutative group $A$ , and any $\mathbb Z$ -linear map $n:M\otimes_{\mathbb Z}A\to A$ , assume that

n(\eta(1)\otimes x)=x,\qquad n(\mu(r\otimes s)\otimes x)=n(r\otimes n(s\otimes x))

for every $r,s\in M$ and $x\in A$ . Equip $M$ with the ring structure obtained from this tensor monoid object, whose addition is the existing addition on $M$ , whose unit is $\eta(1)$ , and whose multiplication is $\mu(r\otimes s)$ . Then there exists a module structure of this ring on the existing additive commutative group $A$ such that $r\cdot x=n(r\otimes x)$ for every $r\in M$ and $x\in A$ . Trivial groups are allowed; if $\eta(1)=0$ , the assumed unit equation forces $A$ to be trivial.

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