Definition. sequence [leinster2016basic, sec. 3.1] [tt-003D]
✍️source

A function with domain \(\mathbb N\) is usually called a sequence.

Related to § [tt-004T].

References

Reference. Basic category theory [leinster2016basic]

2016
Tom Leinster
https://arxiv.org/abs/1612.09375

@article{leinster2016basic,
 title = {Basic category theory},
 author = {Leinster, Tom},
 year = {2016},
 url = {https://arxiv.org/abs/1612.09375},
 journal = {arXiv preprint arXiv:1612.09375}
}

Related

Subobject classifier [tt-004T]

Definition. category of elements [leinster2016basic, 6.2.16] [tt-004C]

Let \({\cal C}\) be a category and \(\mathscr {X} : {\cal C}^{op} \to \mathbf {Set}\) a presheaf on \({\cal C}\). The category of elements \({\cal E}(\mathscr {X})\) of \(\mathscr {X}\) is the category in which:

$\text{[math]}$

There is a projection functor \(\mathscr {P}: \mathbf {E}(\mathscr {X}) \rightarrow {\cal C}\) defined by \(\mathscr {P}(X, x) = X\) and \(\mathscr {P}(f) = f\).

The Yoneda lemma implies that for a presheaf \(\mathscr {X}\), the generalized elements of \(\mathscr {X}\) of representable shape correspond to objects of the category of elements.

Theorem. density [leinster2016basic, 6.2.17] [tt-004D]

Let \({\cal C}\) be a small category and \(\mathscr {X}\) a presheaf on \({\cal C}\). Then \(\mathscr {X}\) is the colimit of the diagram \[ {\cal E}(\mathscr {X}) \xrightarrow {\mathscr {P}} \mathbf {{\cal C}} \xrightarrow {H_{\bullet }}\left [\mathbf {{\cal C}}^{op}, \text { Set }\right ] \] in \(\left [\mathbf {{\cal C}}^{op}, \mathbf {Set} \right ]\), i.e. \[\mathscr {X} \cong \lim \limits _{\rightarrow {\cal E}(\mathscr {X})}\left (\mathscr {P} \mathbin {\bullet } H_{\bullet } \right )\] where \({\cal E}(\mathscr {X})\) is the category of elements, \(\mathscr {P}\) the projection functor in it, and \(H_{\bullet }\) the (contravariant) Yoneda embedding.

This theorem states that every presheaf is a colimit of representables in a canonical way. It is secretly dual to the Yoneda lemma. This becomes apparent if one expresses both in suitably lofty categorical language (that of ends, or that of bimodules).

Definition. subobject classifier [kostecki2011introduction, 6.4] [tt-004I]

A subobject classifier is an object \(\Omega \) in \({\cal C}\), together with an arrow \(\top : \mathbf {1} \to \Omega \), called the true arrow, such that for each monic arrow \(m: Y \mapsto X\) there is a unique arrow \(\chi : X \to \Omega \), called the characteristic arrow of \(m\) (or of \(Y\)), such that the diagram

$\text{[math]}$ is a pullback, where \(!\) is the unique functor.

\(\Omega \) is also called a generalized truth-value object.

The arrow \((! \mathbin {\bullet } T) : Y \stackrel {!}{\to } \mathbf {1} \rightarrowtail \Omega \) is often denoted as \(\top _Y: Y \to \Omega \).

Lemma. isomorphism to class of subobjects [kostecki2011introduction, 6.7] [tt-004K]

In any category \({\cal C}\) with a subobject classifier \(\Omega \), \[ \operatorname {Sub}(X) \cong {\cal C}(X, \Omega ) \] i.e. the class of subobjects of an object \(X\) in \({\cal C}\) is isomorphic to the class of arrows from \(X\) to \(\Omega \).

Proof.

It follows from the definitions and Lemma [tt-003J] that for every \(f : Y \to X\) and \([f] \in \operatorname {Sub}(X)\),

(surjection) \(\chi (f) \in {\cal C}(X, \Omega )\)
(injection) for every \(h : X \to \Omega \), \(\chi (f) = h\) since $\text{[math]}$ is a pullback.

Definition. power object functor [kostecki2011introduction, 6.8] [tt-004M]

The contravariant power object functor \(\mathscr {P}: {\cal C}^{o p} \to {\cal C}\), given by \[\mathscr {P}: X \mapsto \Omega ^X\] for \(X \in \mathrm {Ob}({\cal C})\) and such that \(\mathscr {P}(f): \Omega ^Y \mapsto \Omega ^X\) for \(f: X \to Y\) in \({\cal C}\) is given by \[\mathscr {P}(f)(Y)=\{x \in X \mid f(x) \in Y\}\]

When power object is defined for cartesian closed categories, we have \[ \frac {X \times Y \to \Omega }{Y \to \Omega ^X} \] thus for every category with power objects \[ \operatorname {Hom}(X \times Y, \Omega ) \cong \operatorname {Hom}\left (Y, \Omega ^X\right ) \] This equation, together with Lemma [tt-004K] written in the form \(\operatorname {Sub}(X \times Y) \cong \operatorname {Hom}(X \times Y, \Omega )\), gives the isomorphism \[ \operatorname {Sub}(X \times Y) \cong \operatorname {Hom}(Y, \mathscr {P}(X)) \]