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.
The unit object of a multitensor category is semisimple
Statement
The unit object of a multitensor category is semisimple.
Facts & Assumptions
Given: A multitensor category .
is locally finite and its unit has finite length (Tensor and multitensor categories, Object of finite length).
Tensoring is exact and dualization is exact (Tensor product in a multitensor category is biexact, Dualization in a multitensor category is exact).
Images commute with tensor products (Images commute with tensor products in a multitensor category).
A semisimple object is a finite direct sum of simple objects (Semisimple objects and semisimple abelian categories).
Proof
The Eckmann--Hilton argument makes a finite-dimensional commutative -algebra. If , put and . By [F3], and . Tensoring by and using [F2] then gives , hence . A nonzero nilpotent has a nonzero square-zero power, so is reduced. Thus the commutative Artinian algebra is a finite product of fields. Its primitive idempotents split as a finite direct sum of indecomposable component units , each with a field (not necessarily ).
Fix a component and a simple subobject , which exists by [F1]. Dualizing and then tensoring on the left by gives an exact sequence . The last object is nonzero by the coevaluation zig-zag, so simplicity of makes an isomorphism.
The coevaluation followed by the inverse of the isomorphism in step 2.1 is a nonzero epimorphism . If is the inclusion, then is a nonzero element of the field , hence an isomorphism. Therefore is also epic and thus an isomorphism. So every component unit is simple, and step 1.1 together with [F4] makes semisimple.
Depends on
Used by
Dependency tree · two levels
21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Etingof, Gelaki, Nikshych, Ostrik, Tensor Categories, Theorem 4.3.8(ii) (standard reference, not scraped)