Prove2Me

Tensor monoid objects in Ab give rings

Proved
QAlgorithms.Papers.Independent.Intake100.P20.tensorMonoidsGiveRings

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

prove2quantum

View an abelian group MM as its canonical Z\mathbb Z-module. Suppose m:M⊗ZM→Mm:M\otimes_{\mathbb Z}M\to M and e:Z→Me:\mathbb Z\to M form a monoid object for the tensor monoidal structure, with its associator and unitors. There is a ring structure with the original additive group and

1M=e(1),xy=m(x⊗y).1_M=e(1),\qquad xy=m(x\otimes y).

It is the ring computed by Mathlib's tensor-monoid construction. Multiplication need not be commutative, and the zero ring is permitted. As footnote 5 explains, Z\mathbb Z is the tensor unit, rather than a terminal object of Ab.

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 monoid in Ab gives a ring with its original addition,
unit e(1), and multiplication m(x tensor y). The zero ring is allowed. -/
theorem tensorMonoidsGiveRings (M : ModuleCat.{0} ℤ) [MonObj M] :
    let originalAddition : AddCommGroup M := inferInstance
    let tensorMultiplication : M → M → M :=
      fun x y => MonObj.mul (X := M) (x ⊗ₜ[ℤ] y)
    ∃ r : Ring M,
      r = tensorRing M ∧ r.toAddCommGroup = originalAddition ∧
      r.one = MonObj.one (X := M) (1 : ℤ) ∧
      (∀ x y : M, r.mul x y = tensorMultiplication x y) := by sorry

end QAlgorithms.Papers.Independent.Intake100.P20
Source
Group Objects and Internal Categories, arXiv:math/0212065v1, PDF p. 5, §1, Group Actions and footnote 5
Read-back

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

For any small Z\mathbb Z-module MM equipped with a monoid object structure for the tensor product, let A0A_0 be its existing additive commutative group structure, let η:Z→M\eta:\mathbb Z\to M be its linear unit map, and let μ:M⊗ZM→M\mu:M\otimes_{\mathbb Z}M\to M be its linear multiplication map. There exists a ring structure rr on the underlying type of MM such that

r=tensorRing⁡(M),radd=A0,1r=η(1),x⋅ry=μ(x⊗y)for every x,y∈M.r=\operatorname{tensorRing}(M),\qquad r_{\mathrm{add}}=A_0,\qquad 1_r=\eta(1),\qquad x\mathbin{\cdot_r}y=\mu(x\otimes y)\quad\text{for every }x,y\in M.

Here tensorRing⁡(M)\operatorname{tensorRing}(M) is the ring structure obtained by converting the given tensor monoid object into a ring, and the equality of additive structures is equality of the entire additive commutative group structures. The zero module is allowed.

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