Alphabeta MathHow 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.
Reflective full subcategory and reflector
Definition
Let be a full subcategory of a category , with inclusion (Subcategory and full subcategory). The subcategory is reflective in when has a left adjoint The functor is a reflector. The unit is the reflection unit, and its component is the reflection arrow of .
Thus a reflection includes the full-subcategory data, the functor , and the adjunction data of Adjunction by unit, counit, and the triangle identities. It does not merely assert that some object of receives a map from each object of .
Depends on
Used by
- A reflective inclusion need not preserve even the empty colimit Counterexample
- Coreflective full subcategory and coreflector Definition
- FALSE: A reflective inclusion creates colimits False statement
- FALSE: Every reflective subcategory is closed under ambient colimits False statement
- A full subcategory is reflectively structured exactly when universal arrows are supplied at every ambient object Theorem
- A reflective inclusion creates every ambient limit in the ordinary isomorphism-invariant sense Theorem
- A reflective subcategory has every ambient colimit, obtained by reflecting an ambient colimit Theorem
- Abelian groups form a reflective full subcategory of groups Theorem
- An ambient object lies in the essential image of a reflective inclusion exactly when its reflection unit is invertible Theorem
- Commutative rings form a reflective full subcategory of rings Theorem
- The counit of a reflection is an isomorphism Theorem
- Torsion-free abelian groups form a reflective full subcategory of abelian groups Theorem
- With the ultrafilter lemma, dependent choice, and a supplied family of SAFT initial objects, compact Hausdorff spaces form a reflective full subcategory of topological spaces Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 10 results over 7 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- E. Riehl, Category Theory in Context, section 4.5 (standard reference, not scraped)
- T. Leinster, Basic Category Theory, section 6.3 (standard reference, not scraped)