support object (changes) in nLab
Showing changes from revision #5 to #6: Added | Removed | Changed
Context
Category theory
Contents
Idea
In set theory, the support of a set turns the set into a subsingleton. In dependent type theory, propositional truncation or the bracket type is an operation which takes a type and turns it into a h-propositions, which are the type theoretic equivalent of subsingletons. By the relation between type theory and category theory and the relation between set theory and topos theory, it should be possible to do the same process and turn an object of a category into a subterminal object. These are the support objects, bracket objects, or propositional truncation objects in category theory.
Definition
The support object [X][X] of an object XX in a category CC with a terminal object 11 is the image of the unique morphism X→1X \to 1.
In category theory
X→[X]↪1X \to [X] \hookrightarrow 1 The support object [X][X] of an object XX in a regular category CC is the image of the unique morphism into the terminal object X→1X \to 1. X→[X]↪1X \to [X] \hookrightarrow 1 As a result, that all support objects exist is equivalent to the condition that every morphism into the terminal object has an image factorization. The support object [X][X] of an object XX in a unitary tabular allegory CC is the tabulation? of the unique map from XX into the allegorical unit 11. In any well-pointed pretopos ℰ\mathcal{E}, the support is the coequalizer of the product projection morphisms π 1:X×X→X\pi_1:X \times X \to X and π 2:X×X→X\pi_2:X \times X \to X X×X ⟶π 2⟶π 1 X ↘ ↙ p [X].\array{
X \times X
&&
\stackrel{\overset{\pi_1}{\longrightarrow}}{\underset{\pi_2}{\longrightarrow}}
&&
X
\\
& \searrow && \swarrow_{\mathrlap{p}}
\\
&& [X]
}.
computational trinitarianism = \linebreak propositions as types +programs as proofs +relation type theory/category theoryIn allegory theory
Properties
See also
Last revised on July 28, 2024 at 18:04:09. See the history of this page for a list of all contributions to it.