Actual skeletal objects form a group

Proved

QAlgorithms.Papers.Independent.Intakenext100.P06.skeletalObjectsGroup

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

prove2quantum

Let $\mathcal C$ be a skeletal Gr-category. Its actual object set, without passage to a quotient, carries a group structure such that

x\cdot y=x\otimes y,\qquad 1=I,\qquad x^{-1}=y \quad\text{whenever }x\otimes y\cong I\cong y\otimes x.

Skeletality means that isomorphic objects are equal. This identifies the group law and every possible weak inverse with the original monoidal data.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P06

Formal statement

namespace QAlgorithms.Papers.Independent.Intakenext100.P06

open CategoryTheory CategoryTheory.MonoidalCategory

open QAlgorithms.Papers.Independent.Gap48.P14

open QAlgorithms.Papers.Independent.Renew46.P18

universe u v u1 v1 w

attribute [local instance] QAlgorithms.Papers.Independent.Intakenext100.P06.singletonSymmetric

/-- Section 3, PDF p. 7: the group is on actual skeletal objects,
with exactly the given tensor product and unit, rather than a quotient. -/
theorem skeletalObjectsGroup {C : Type u} [Category.{v} C]
    [MonoidalCategory C] (h : IsWeakTwoGroup C) (hs : Skeletal C) :
    ∃ k : Group C,
      letI := k
      (∀ x y : C, x * y = x ⊗ y) ∧ (1 : C) = 𝟙_ C ∧
      (∀ x y : C, IsWeakInverse x y → x⁻¹ = y) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P06

Source

Hoàng Xuân Sính's Thesis: Categorifying Group Theory, arXiv:2308.05119v2, PDF p. 7, §3: actual objects of a skeletal Gr-category form a group

Read-back

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

Let $C$ be a monoidal category in which every morphism is invertible, every object $x$ has some object $y$ with $x\otimes y\cong I$ and $y\otimes x\cong I$ , and any two isomorphic objects are equal. Then there exists a group structure on the actual type of objects of $C$ such that

xy=x\otimes y\quad\text{for every }x,y\in C,\qquad 1=I,

and, for every pair $x,y\in C$ , if there exist isomorphisms $x\otimes y\cong I$ and $y\otimes x\cong I$ , then the group inverse satisfies $x^{-1}=y$ .

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