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.
Torsion-free abelian groups give a conservative right adjoint that is not monadic
Statement refuted
The assertion that every conservative right adjoint is monadic is false. Torsion-free abelian groups give a conservative right adjoint that is not monadic.
Facts & Assumptions
Given: The category of torsion-free abelian groups and group homomorphisms, with underlying-set functor .
The full subcategory of torsion-free abelian groups is reflective in (Torsion-free abelian groups form a reflective full subcategory of abelian groups).
For , the Eilenberg–Moore category of the free-module monad is isomorphic over to the category of abelian groups (For a unital ring R, the free-R-module monad on sets has left R-modules as its Eilenberg–Moore algebras).
A -module is torsion-free when no nonzero integer annihilates a nonzero element (Annihilators, torsion elements and the torsion subset of a module).
The quotient group is on the same underlying congruence classes (For every , the congruence-class group is the quotient group ).
Counterexample
Free abelian groups are torsion-free, so the usual free-abelian-group functor lands in and is left adjoint to . Equivalently, this adjunction is obtained by combining the free-abelian adjunction with the reflective inclusion in [L1].
A bijective homomorphism of torsion-free abelian groups has an inverse that preserves addition, so it is an isomorphism. Hence reflects isomorphisms and is conservative.
The induced monad is the usual free-abelian-group monad: applying the torsion-free reflector to a free abelian group changes nothing. By [L2], its full Eilenberg–Moore category is over .
The comparison from to is the inclusion and misses the group in [L4]. The nonzero class of is killed by the nonzero integer , so this group is not torsion-free by [L3].
Thus the comparison is not essentially surjective and is not an equivalence, so is not monadic, while step 1.2 shows it is conservative.
Depends on
- Conservative functor
- Monadic and strictly monadic functors
- Torsion-free abelian groups form a reflective full subcategory of abelian groups
- The free-module functor is left adjoint to the underlying-set functor
- For a unital ring R, the free-R-module monad on sets has left R-modules as its Eilenberg–Moore algebras
- Annihilators, torsion elements and the torsion subset of a module
- For every $n\in\mathbb N$, the congruence-class group $(\mathbb Z/n,+)$ is the quotient group $(\mathbb Z,+)/n\mathbb Z$
Used by
- FALSE: every conservative right adjoint is monadic False statement
Dependency tree · two levels
31 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
- D. Mehrle, Category Theory Part III, Example 5.20(d) (standard reference, not scraped)
- E. Riehl, Category Theory in Context, 2nd ed., monadicity examples in Section 5.5 (standard reference, not scraped)