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.
A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible
Statement
Every monoid is a one-object category. Under this identification, the monoid is a group exactly when every morphism is invertible.
Facts & Assumptions
Given: A monoid .
A monoid has associative multiplication and a two-sided identity (Semigroup and monoid), exactly the composition and identity laws required by Category, object, morphism, domain, codomain, identity, composition, and hom-collection.
A group is a monoid in which every element has a two-sided inverse (Group and abelian group).
Proof
Take one object , put , define composition by , and take ; [L1] verifies the category axioms.
A morphism is an isomorphism precisely when some satisfies .
By [L2], every morphism in this one-object category is invertible exactly when is a group.
Depends on
Used by
- A wrong counit can be natural while both triangle identities fail Counterexample
- A commutative monoid as a one-object strict monoidal category Example
- Actions of a group G on sets are functors BG toSet Example
- An action groupoid has the acted-on set as objects, orbits as connected components, and stabilizers as automorphism groups Example
- For a monoid action, Yoneda says that an equivariant map from the regular action is determined by the identity element Example
- Induction and coinduction of permutation representations as Kan extensions Example
- The coend of the hom-bifunctor Example
- The orbit-set and fixed-point constructions as Kan extensions Example
- The tensor product of monoid sets as a coend Example
- A unit and counit determine an adjunction without the triangle identities False statement
- Under the Axiom of Choice, a connected small groupoid is equivalent to the automorphism group of any one of its objects Proposition
- The endomorphisms of the tensor unit form a commutative monoid Theorem
Dependency tree · two levels
10 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
- Emily Riehl, Category Theory in Context, Chapter 1 (standard reference, not scraped)