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.
An ambient object lies in the essential image of a reflective inclusion exactly when its reflection unit is invertible
Statement
For a reflection with unit , an object is isomorphic to an object in the image of if and only if is an isomorphism.
Facts & Assumptions
Given: A reflection as in Reflective full subcategory and reflector, with unit , and an object .
For a reflector onto a full subcategory, every component of the counit is an isomorphism (The counit of a reflection is an isomorphism).
A morphism is an isomorphism if there is with and ; such a is unique and is denoted (Isomorphism, groupoid, and connected category).
For an adjunction with unit and counit , the triangle identities hold componentwise: and (Adjunction by unit, counit, and the triangle identities).
Proof
If is invertible, it itself displays as isomorphic to the included object , so lies in the essential image.
Conversely, let be an isomorphism. Naturality of gives . The map is invertible because a functor sends the inverse of to its inverse. Applying in [L3] at gives , and is invertible because is by [L1] and functors preserve inverses; composing that identity with on the left gives , which is therefore an isomorphism. Hence . A composite of isomorphisms is an isomorphism, since is a two-sided inverse for it by associativity and the identity laws; applying this twice and using [L2] makes invertible.
Depends on
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 15 results over 9 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)