A weak representation of a functor (presheaf) is like a representable functor but only satisfying the representability condition up to retract rather than isomorphism. Unlike a representable, this structure is not unique up to isomorphism, and so we speak of representations as structure rather than representability as a property.
In type theoretic terms, this is an object that only satisfies the equation of a universal property and not the equation.
A weak representation of a presheaf consists of
Equivalently, by the Yoneda lemma, a weak representation is
A weak representation of induces an idempotent on the representable sets such that is the idempotent splitting of the representable in the presheaf category. By the Yoneda lemma, this induces an idempotent on in , and an object represents if and only if is the idempotent splitting of . As a consequence, a representable has a canonical section to any weak representation .
In type theoretic terms, the idempotent performs expansion, and so this says that a representable can be constructed from a weak representable as the fixed points of expansion, or dually as a quotient equating the expansion with the identity.
Created on August 19, 2022 at 14:05:20. See the history of this page for a list of all contributions to it.