How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Tensor and Fusion Categories — Examples
1 · Prerequisites
- Abelian Categories
- Binary Operations, Monoids, Groups and Subgroups
- Cardinal Arithmetic, Cofinality and the Alephs
- Categories, Functors and Natural Transformations
- Chains, Antichains, Sperner and Dilworth
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Duality and Rigidity in Monoidal Categories
- Exactness and the Member Calculus
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Group Homomorphisms and the Isomorphism Theorems
- Limits and Colimits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monoidal Categories and Monoidal Functors
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Preadditive and Additive Categories and Biproducts
- Reflective Subcategories and the Adjoint Functor Theorems
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Set Theory Beyond Choice: Recorded, Not Proved Here
- Subobject Lattices Generators and the Grothendieck Axioms
- Suprema and Infima
- Tensor and Fusion Categories
- Tensor Products of Modules
- The ZFC Axioms and the Basic Set Constructions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
These examples use finite-dimensional vector spaces and do not reconstruct their tensor product.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Finite-dimensional vector spaces form a fusion category
Example
For a field , the category is a fusion category.
Facts & Assumptions
Given: A field .
-modules are monoidal under with unit (Modules over a commutative ring form a monoidal category).
Every finite-dimensional -vector space is rigid (Finite-dimensional vector spaces are rigid).
Fusion means finite semisimple tensor category (Fusion and multifusion categories).
Verification
By [F1] and [F2], the finite-dimensional subcategory is a rigid -linear monoidal category.
Every finite-dimensional vector space is a finite direct sum of copies of , so is the only simple isomorphism class and the category is finite semisimple. Its unit has endomorphism algebra .
These clauses are exactly those of [F3], so is fusion.
The Grothendieck ring of finite-dimensional vector spaces
Example
The dimension map identifies with as a ring.
Facts & Assumptions
Given: A field and .
This category is fusion (Finite-dimensional vector spaces form a fusion category). Every finite-dimensional vector space is isomorphic to a finite direct sum of copies of , and is simple, so is its only simple class.
The Grothendieck group is generated by object classes modulo short-exact relations; its intended multiplication on generators is (The Grothendieck ring of a tensor category). We verify that this multiplication is well-defined in the present example.
Verification
Dimension is additive on short exact sequences: a basis of a subspace, together with lifts of a basis of the quotient, is a basis of the middle space. Thus respects every relation in [F2] and induces a group homomorphism . Split direct-sum sequences and [F1] give , including . Hence , , satisfies and , proving the asserted additive bijection on all classes, including negative virtual classes.
Transport integer multiplication along this bijection: set . This is a well-defined unital ring structure, with unit . Tensor products of finite bases give , so . Thus the intended tensor multiplication in [F2] descends to the quotient; its bilinear extension is unique because object classes generate the group. The map is therefore an isomorphism of rings, with zero and unit preserved.
A matrix multifusion category with nonsimple unit
Example
For , finite matrices of finite-dimensional vector spaces, with matrix multiplication using and , form a multifusion category whose unit is not simple.
Facts & Assumptions
Given: A field and an integer .
A multifusion category is finite semisimple multitensor category (Fusion and multifusion categories).
Verification
Let objects be matrices and set . The matrix with on the diagonal and off it is a unit.
Entrywise semisimplicity and finite direct sums from [F1] give the finite semisimple rigid structure required in [F2].
But is a nontrivial direct sum when . Hence this is multifusion, not fusion.
Fusion rules for a supplied finite simple family
Example
For the supplied simple family of , the only fusion coefficient is .
Facts & Assumptions
Given: The one-term family .
is a fusion category (Finite-dimensional vector spaces form a fusion category). Every finite-dimensional vector space is a finite direct sum of copies of the simple object , so is its sole simple class.
Fusion coefficients are defined by products of simple classes (Fusion rules).
Verification
The unit isomorphism gives .
Comparing this with the defining expansion in [F2] for the supplied one-element family yields .