Appendix [tt-0006]
✍️source

These are my notes on:

Category theory
Topos theory
Type theory
Sheaf theory
Differential sheaves
SDG (Synthetic Differential Geometry)

The primary references for these notes are:

[kostecki2011introduction]
[leinster2016basic]
[kostecki2009differential]
[rosiak2022sheaf]
[mallios2015differential]
[rosiak2022sheaf]
[zhang2021type]
[chen2016infinitely]
[sterling2023models]

[marsden2014category]

[fauser2004grade]

For draft notes, see drafts for Notes on Topos Theory and Type Theory.

Context

Notes on Topos Theory and Type Theory [tt-0001]
📄PDF

May 28, 2024
Utensil Song

category theory [tt-000Z]

Categories [tt-0005]

definition. category [kostecki2011introduction, 1.1] [tt-0002]

A category \({\cal C}\) consists of:

objects \(\operatorname {Ob}({\cal C})\): \(O, X, Y, \dots \)
arrows \(\operatorname {Arr}({\cal C})\): \(f, g, h, \dots \), where for each arrow \(f\),
- a pair of operations \(\operatorname {dom}\) and \(\operatorname {cod}\) assign a domain object \(X=\operatorname {dom}(f)\) and a codomain object \(Y=\operatorname {cod}(f)\) to \(f\),
- thus f can be denoted by \[f : X \to Y\] or \[X \xrightarrow {f} Y\]
compositions: a composite arrow of any pair of arrows \(f\) and \(g\), denoted \(g \circ f\) or \( f \mathbin {\bullet } g \), makes the diagram commute (we say that \(f \mathbin {\bullet } g\) factors through \(Y\)),
a identity arrow for each object \(O\), denoted \(\mathit {1}_O : O \to O\)

satisfying:

associativity of composition: the diagram commutes,
identity law: the diagram commutes.

convention. composition [kostecki2011introduction, 1.1] [tt-003X]

In literatures, composition of arrows in a category is most frequently denoted \(\circ \) or just by juxtaposition, i.e. for the diagram \(g \circ f\) or just \(gf\) mean \(g\) applies to the result of \(f\).

But this is the opposite of the order of arrows in the diagram, so arguably a more natural way could be to denote the above as \(f ; g\) [kostecki2011introduction, 1.1], or as \(f \mathbin {⨟} g\) [fong2018seven, 3.6], or as \(f \mathbin {\bullet } g\) [nakahira2023diagrammatic, sec. 1.1].

We use \(f \mathbin {\bullet } g\) throughout this note, so it can always be understood as \(\xrightarrow {f}\xrightarrow {g}\). This way saves mental energy when reading commuting diagrams, pasting diagrams and string diagrams which we employ heavily.

definition. (locally) small, hom-set [kostecki2011introduction, 1.3] [tt-000A]

A category C is called locally small iff for any of its objects \(X, Y\) , the collection of arrows from \(X\) to \(Y\) is a set, called a hom-set, denoted \[\operatorname {Hom}_{{\cal C}}(X, Y)\]

A category is called small iff the collection of all its arrows is a set.

notation. hom-set, hom-class [zhang2021type, 1.2] [tt-0003]

\(\operatorname {Hom}\) in \(\operatorname {Hom}_{{\cal C}}(X, Y)\) is short for homomorphism, since an arrow in category theory is a morphism (i.e. an arrow), a generalization of homomorphism between algebraic structures.

This notation could be unnecessarily verbose, so when there is no confusion, we follow [leinster2016basic] and [zhang2021type] to simply write \(X,Y \in \operatorname {Ob}({\cal C})\) as \[X,Y \in {\cal C}\] and \(f \in \operatorname {Hom}_{{\cal C}}(X, Y)\) as \[f \in {\cal C}(X, Y)\]

In some other scenarios, when the category in question is clear (and it might be to too verbose to write out, e.g. a functor category), we omit the subscript of the category and write just \[\operatorname {Hom}(X, Y)\]

In general, collection \(\operatorname {Ob}({\cal C})\) and \(\operatorname {Arr}({\cal C})\) are not neccessarily sets, but classes. In that case, \(\operatorname {Hom}_{{\cal C}}(X, Y)\) is called a hom-class.

Later, we will also learn that \(\operatorname {Ob}\) and \(\operatorname {Arr}\) are representable functors.

definition. finite [kostecki2011introduction, 1.3] [tt-0034]

A category is called finite iff it is small and it has only a finite number of objects and arrows.

definition. commuting diagram [kostecki2011introduction, 1.2] [tt-0007]

A diagram in a category \({\cal C}\) is defined as a collection of objects and arrows that belong to the category \({\cal C}\) with specified operations \(\operatorname {dom}\) and \(\operatorname {cod}\).

A commuting diagram is defined as such diagram that any two arrows of this diagram which have the same domain and codomain are equal.

For example, that the diagram commutes means \(f \mathbin {\bullet } g = h \mathbin {\bullet } k\).

It's also called a arrow diagram [nakahira2023diagrammatic, 1.1] when compared to a string diagram, as it represents arrows with \(\to \).

definition. string diagram [nakahira2023diagrammatic, table 1.1] [tt-003V]

A string diagram represents categories as surfaces (2-dimensional), functors as wires (1-dimensional), natural transformations as blocks or just dots (0-dimensional).

String diagrams has the advantage of being able to represent objects, arrows, functors, and natural transformations from multiple categories, and their vertical and horizontal composition, and has various topologically plausible calculational rules for proofs.

notation. string diagrams: category, object and arrow [marsden2014category, sec. 2.1] [tt-0004]

Later, when we have learned about functors and natural transformations, we will see that, in string diagram for 1-category:

A category \({\cal C}\) is represented as a colored region:
Functors of type \(\mathbf {1} \to {\cal C}\) can be identified with objects of the category \({\cal C}\), where \(\mathbf {1}\) is the the terminal category, so an object \(X \in \operatorname {Ob}({\cal C})\) can be represented as:
An arrow \(f : X \to Y\) is then a natural transformation between two of these functors, represented as:

convention. letters [tt-0010]

The general idea is that we try to use visually distinct letters for different concepts:

uppercase calligraphic letters \({\cal C}, {\cal D}, {\cal E}, {\cal J}, {\cal S}\) denote categories
- \({\cal C}, {\cal D}, {\cal E}\) are prefered in concepts about one to three categories, since \({\cal C}\) is the first letter of "category"
- \({\cal J}\) is used in concepts like diagram, and assumed to be small
- \({\cal S}\) is used in concepts like subcategory, or sometimes in concepts about a small category
boldface uppercase Roman letters denote specific categories, e.g. \(\mathbf {Cat}, \mathbf {Set}, \mathbf {Grp}, \mathbf {Top}, \mathbf {1}\)
uppercase Roman letters \(X, Y, Z, W, O, E, V\) denote objects in categories
- \(X, Y\) usually mean objects in \({\cal C}\) and \({\cal D}\), respectively
- \(O\) denotes any object
- \(E\) denotes the equalizer object
- in limit-related concepts, \(\mathrm {-}\) denotes any object, \(V\) denotes the vertex
lowercase Roman letters \(f, g, h, i, k, l, r\) and sometimes the lowercase Roman letter of the corresponding codomain or domain object denote arrows
- occationally, when two arrows are closely related, they are denoted by the same letter with different subscripts, e.g. \(g_1, g_2\)
- as special cases, \(\iota , p, i\) denote the inclusion, projection and injection arrows
uppercase script letters \(\mathscr {F}, \mathscr {G}, \mathscr {H}, \mathscr {I}, \mathscr {K}, \mathscr {L}, \mathscr {R}\) denote functors
- \(\mathscr {D}\) denotes a diagram functor
- \(\mathscr {L}\) and \(\mathscr {R}\) denote the left and right adjoint functors in an adjunction, respectively
- \(\mathscr {H}\) denotes the Yoneda embedding functors
- as a special case, functors with the terminal category (i.e. constant object functors) as the domain are identified with the objects in the codomain category, thus are denoted like an object: \(X : \mathbf {1} \to {\cal C}, \mathrm {*} \mapsto X\)
- \(\mathscr {I}\) is only used in the inclusion functor (note that this is letter "I")
- we do not use \(\mathscr {J}\) and \(\mathscr {S}\) because they are visually ambiguous
lowercase Greek letters \(\alpha , \beta , \eta , \epsilon , \sigma \) denote natural transformations, their components are denoted by them with subscripts.

isomorphism [tt-000F]

definition. monic [kostecki2011introduction, 2.1] [tt-000B]

An arrow \(f : X \to Y\) is monic if the diagram commutes, i.e. \(g_1 \mathbin {\bullet } f = g_2 \mathbin {\bullet } f \implies g_1 = g_2\), denoted \(f : X \rightarrowtail Y\).

"Monic" is short for "monomorphism", which is a generalization of the concept of injective (one-to-one) functions between sets.

definition. epic [kostecki2011introduction, 2.2] [tt-000C]

An arrow \(f : X \to Y\) is epic if the diagram commutes, i.e. \(f \mathbin {\bullet } g_1 = f \mathbin {\bullet } g_2 \implies g_1 = g_2\), denoted \(f : X \twoheadrightarrow Y\).

"Epic" is short for "epimorphism", which is a generalization of the concept of surjective (onto) functions between sets.

definition. iso [kostecki2011introduction, 2.3] [tt-000D]

An arrow \(f : X \to Y\) is iso, or \(X\) and \(Y\) are isomorphic, denoted \(X \cong Y\), or \(X \xrightarrow {\sim } Y\), if the diagram commutes, where \(!g\) means there exists a unique arrow \(g\), and \(g\) is called the inverse of \(f\), denoted \(f^{-1}\).

"Iso" is short for "isomorphism", which is a generalization of the concept of bijective (one-to-one and onto) functions.

convention. uniqueness: dashed arrow [tt-000J]

Uniqueness of an arrow is denoted \(\exists ! f\) or simply \(!f\), and visualized as a dashed arrow in diagrams, and \(!\) is often omitted.

lemma. Iso [kostecki2011introduction, 2.4] [tt-000E]

An iso arrow is always monic and epic. However, not every arrow which is monic and epic is also iso.

proof.

The diagram commutes for the iso arrow \(f\), thus

\(g = h\) i.e. \(f\) is monic,
\(k = l\) i.e. \(f\) is epic.

special objects and categories [tt-000G]

definition. initial, terminal and null objects [kostecki2011introduction, 2.6] [tt-000I]

An initial object in a category \({\cal C}\) is an object \(\mathrm {0} \in \operatorname {Ob}({\cal C})\) such that for any object \(X\) in \({\cal C}\), there exists a unique arrow \(\mathrm {0} \to X\). It's also called a universal object, or a free object.

A terminal object in a category C is an object \(\mathrm {1} \in \operatorname {Ob}({\cal C})\) such that for any object \(X\) in \({\cal C}\), there exists a unique arrow \(X \to \mathrm {1}\). It's also called a final object, or a bound object.

Diagramatically,

A null object is an object which is both terminal and initial, confusingly, it's also called a zero object.

lemma. Uniqueness [kostecki2011introduction, 2.7] [tt-000K]

All initial objects in a category are isomorphic.

All terminal objects in a category are isomorphic.

In other words, they are unique up to isomorphism, respectively.

definition. element [kostecki2011introduction, 2.8, 2.9] [tt-000M]

Let \(X, S \in \operatorname {Ob}({\cal C})\).

An element or a generalized element of \(X\) at stage \(S\) (or, of shape \(S\)) is an arrow \(x : S \to X\) in \({\cal C}\), also denoted \(x \in _{S} X\).

An arrow \(1 \to X\) is called a global element of \(X\), a.k.a. a point of \(X\).

An arrow \(S \to X\), if \(S\) is not isomorphic to \(1\), is called the local element of \(X\) at stage \(S\).

An arrow \(\mathit {1}_X : X \to X\) is called the generic element of \(X\).

remark. element [kostecki2011introduction, 2.8] [tt-002W]

In an element \(x : S \to X\), the object \(S\) is called a stage in order to express the intuition that it is a "place of view" on \(X\). In the same sense, \(S\) is also called a domain of variation, and \(X\) a variable element.

Sometimes, the term shape is used instead [leinster2016basic, 4.1.25], intuitive examples are:

when the object is a set, a generalized element of \(X\) of shape \(\mathbb N\) is a sequence in the set \(X\)
when the object is a topological space, a generalized element of \(X\) of shape \(S^1\) is a loop

In the context of studying solutions to polynomial equations, we may also call it a \(S\)-valued point in \(X\), where \(S\) is the number set where the solution is taken, e.g. the real, complex, and \(\operatorname {Spec} \mathbb F_p\)-valued solutions.

definition. equivalent, equivalence class [kostecki2011introduction, 2.10] [tt-000N]

Two monic arrows \(x\) and \(y\) which satisfy are called equivalent, which is denoted as \(x \sim y\).

The equivalence class of \(x\) is denoted as \([x]\), i.e., \([x]=\{y \mid x \sim y\}\).

definition. subobject, Sub [kostecki2011introduction, 2.10] [tt-004J]

A subobject of any object is defined as an equivalence class of monic arrows into it.

The class of subobjects of an object \(X\) is denoted as \[ \operatorname {Sub}(X):=\{[f] \mid \operatorname {cod}(f)=X \wedge f \text { is monic }\}. \]

definition. Set [kostecki2011introduction, 1.1, example 1] [tt-0008]

\(\mathbf {Set}\), the category of sets, consists of objects which are sets, and arrows which are functions between them. The axioms of composition, associativity and identity hold due to standard properties of sets and functions.

\(\mathbf {Set}\) has the initial object \(\varnothing \), the empty set, and the terminal object, \(\{*\}\), the singleton set.

\(\mathbf {Set}\) doesn't have a null object.

Monic arrows in \(\mathbf {Set}\) are denoted by \(f: X \hookrightarrow Y\), interpreted as an inclusion map (see also inclusion function in nLab).

Given \(X : \mathbf {Set}\), the subobjects of \(X\) are in canonical one-to-one correspondence with the subsets of \(X\).

notation. inclusion [leinster2016basic, 0.8] [tt-000T]

In the symbol \(\hookrightarrow \) is used for inclusions. It is a combination of a subset symbol \(\subset \) and an arrow.

definition. Cat [leinster2016basic, 3.2.10] [tt-003G]

We denote by \(\mathbf {Cat}\) the category of small categories and functors between them.

definition. discrete category [leinster2016basic, 1.1.8] [tt-003K]

A discrete category has no arrows apart from the identity arrow, i.e. it amounts to just a class of objects.

We can regard a set as a discrete category.

definition. terminal category [leinster2016basic, 4.1.6] [tt-003F]

A terminal category, denoted \(\mathbf {1}\), has only one object, denoted \(\mathrm {*}\), and only the identity arrow, denoted \(\mathit {1}\).

definition. opposite category [kostecki2011introduction, 2.5] [tt-000H]

A category is called the opposite category of \({\cal C}\), denoted \(C^{op}\), iff

(reversion of arrows) \[\operatorname {Ob}({\cal C}^{op}) = \operatorname {Ob}({\cal C})\] \[\operatorname {Arr}({\cal C}^{op}) \ni f: Y \to X \Longleftrightarrow \operatorname {Arr}({\cal C}) \ni f: X \to Y\]
(reversion of composition)

definition. product category [leinster2016basic, 1.1.11] [tt-0048]

Given categories \({\cal C}\) and \({\cal D}\), there is a product category, denoted \({\cal C} \times {\cal D}\), in which

an object is a pair \((X, Y)\)
an arrow \((X, Y) \to \left (X', Y'\right )\) is a pair \((f, g)\)
the composition is given by \[(f_1, g_1) \mathbin {\bullet } (f_2, g_2) = (f_1 \mathbin {\bullet } f_2, g_1 \mathbin {\bullet } g_2)\]
the identity on \((X, Y)\), denoted \(\mathit {1}_{(X, Y)}\) is \((\mathit {1}_X, \mathit {1}_Y)\)

where \(X \in {\cal C}\), \(Y \in {\cal D}\), \(f: X \to X' \in {\cal C}\), and \(g: Y \to Y' \in {\cal D}\).

definition. (full) subcategory [leinster2016basic, 1.2.18] [tt-002Y]

Let \({\cal C}\) be a category. A subcategory \({\cal S}\) of \({\cal C}\) consists of a subclass \(\operatorname {Ob}({\cal S})\) of \(\operatorname {Ob}({\cal C})\) together with, for each \(S, S' \in \operatorname {Ob}({\cal S})\), a subclass \({\cal S}\left (S, S'\right )\) of \({\cal C}\left (S, S'\right )\), such that \({\cal S}\) is closed under composition and identities.

It is a full subcategory if \({\cal S}\left (S, S'\right )={\cal C}\left (S, S'\right )\) for all \(S, S' \in \operatorname {Ob}({\cal S})\).

functors [tt-0013]

definition. (covariant) functor [kostecki2011introduction, 3.1] [tt-0014]

A (covariant) functor \(\mathscr {F}: {\cal C} \to {\cal D}\) is given by the diagram i.e. a map of objects and arrows between categories \({\cal C}\) and \({\cal D}\) that preserves the structure of the compositions and identities.

definition. contravariant functor [kostecki2011introduction, 3.1] [tt-0015]

A functor \(\mathscr {F}\) is called a contravariant functor from \({\cal C}\) to \({\cal D}\), and denoted \(\mathscr {F} : {\cal C}^{op} \to {\cal D}\), if it obeys the definition given by the (covariant) functor for \({\cal C}\) replaced by \({\cal C}^{op}\), i.e. it's given by the diagram i.e. a map of objects and arrows between categories \({\cal C}\) and \({\cal D}\) that reverses the structure of the arrows, compositions and identities.

definition. functorial in [leinster2016basic, sec. 4.1] [tt-0041]

For some expression \(E(X)\) containing \(X\), when we say \(E(X)\) is (covariant) functorial in \(X\), we mean that there exists a functor \(\mathscr {F}\) such that for every \(f : X \to X'\).

Dually, we use the term contravariantly functorial in.

convention. functors [tt-001D]

For simplicity, when there is no confusion, we use \(\bullet \) to represent corresponding objects, and omit the arrow names in the codomain of a functor, e.g.

definition. full and faithful [kostecki2011introduction, 3.2] [tt-0017]

A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) is full iff for any pair of objects \(X, Y\) in \({\cal C}\) the induced map \(F_{X, Y}: {\cal C}(X, Y) \to {\cal D}(\mathscr {F}(X), \mathscr {F}(Y))\) is surjective (onto). \(\mathscr {F}\) is faithful if this map is injective (one-to-one).

definition. preserve and reflect [kostecki2011introduction, 3.3] [tt-0018]

A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) is called to preserve a property \(\wp \) of an arrow iff for every \(f \in \operatorname {Arr}({\cal C})\) that has a property \(\wp \) it follows that \(\mathscr {F}(f) \in \operatorname {Arr}({\cal D})\) has this property. A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) is called to reflect a property \(\wp \) of an arrow iff for every \(\mathscr {F}(f) \in \operatorname {Arr}({\cal D})\) that has a property \(\wp \) it follows that \(f \in \operatorname {Arr}({\cal C})\) has this property.

example. full, faithful, preserve and reflect [kostecki2011introduction, 3.3] [tt-0019]

Every inclusion functor is faithful.

Every functor preserves isomorphisms.

Every faithful functor reflects monomorphisms and epimorphisms.

Every full and faithful functor reflects isomorphisms.

special functors [tt-003N]

definition. identity functor [kostecki2011introduction, 3.1, example 1] [tt-003P]

The identity functor \(\mathit {1}_{{\cal C}}: {\cal C} \to {\cal C}\) (denoted also by \( 1_{{\cal C}}: {\cal C} \to {\cal C}\)), defined by \(\mathit {1}_{{\cal C}}(X)=X\) and \(\mathit {1}_{{\cal C}}(f)=f\) for every \(X \in \operatorname {Ob}({\cal C})\) and every \(f \in \operatorname {Arr}({\cal C})\).

definition. constant functor [kostecki2011introduction, 3.1, example 2] [tt-003Q]

The constant functor \(\Delta _O: {\cal C} \to {\cal D}\) which assigns a fixed \(O \in \mathrm {Ob}({\cal D})\) to any object of \({\cal C}\) and \(\mathit {1}_O\), the identity arrow on \(O\), to any arrows from \({\cal C}\) : with compositions and identities preserved in a trivial way.

definition. constant object functor [leinster2016basic, 4.1.6] [tt-003H]

A functor from the terminal category \(\mathbf {1}\) to a category \({\cal C}\) simply picks out an object of \({\cal C}\), called a constant object functor (which is a constant functor), denoted \(\Delta _X : \mathbf {1} \to {\cal C}\) for some \(X \in \operatorname {Ob}({\cal C})\), or simly denoted by the object, e.g. \(X\).

As special cases, constant object functor for initial and terminal objects are denoted by \(\mathrm {0}\) and \(\mathrm {1}\), respectively.

definition. unique functor [nakahira2023diagrammatic, eq. 2.3] [tt-003Z]

A unique functor, is a functor from a category \({\cal C}\) to the terminal category \(\mathbf {1}\), uniquely determined by mapping all arrows in \({\cal C}\) to the identity arrow \(\mathit {1}_{\mathrm {*}}\) of the unique object \(\mathrm {*}\) in \(\mathbf {1}\).

This functor is often denoted by \(! : {\cal C} \to \mathbf {1}\).

Intuitively, the functor \(!\) acts to erase all information about the input.

definition. diagonal functor [leinster2016basic, sec. 6.1] [tt-003T]

Given a small category \({\cal J}\) and a category \({\cal C}\), the diagonal functor \[\Delta _{{\cal J}}: {\cal C} \to [{\cal J}, {\cal C}]\] maps each object \(X \in {\cal C}\) to the constant functor \(\Delta _{{\cal J}}(X): {\cal J} \to {\cal C}\), which in turn maps each object in \({\cal J}\) to \(X\), and all arrows in \({\cal J}\) to \(\mathit {1}_X\).

When \({\cal J}\) is clear in the context, we may write \(\Delta _{{\cal J}}(X)\) as \(\Delta _X\).

Particularly [kostecki2011introduction, 3.1, example 6], when \({\cal J}\) is a discrete category of two objects, \(\Delta : {\cal C} \to {\cal C} \times {\cal C}, \Delta (X)=(X, X)\) and \(\Delta (f)=(f, f)\) for \(f: X \to X^{\prime }\)

\(\Delta _{{\cal J}}(X)\) is the same as \(X \mathbin {\bullet } !\), thus [nakahira2023diagrammatic, eq. 2.12] \[\Delta _{{\cal J}} = - \mathbin {\bullet } !\]

definition. forgetful functor [kostecki2011introduction, 3.1, example 3] [tt-003R]

The forgetful functor, which forgets some part of structure, however arrows, compositions and identities are preserved.

definition. inclusion functor [leinster2016basic, 1.2.18] [tt-003S]

Whenever \({\cal S}\) is a subcategory of a category \({\cal C}\) , there is an inclusion functor \(\mathscr {I} : {\cal S} \hookrightarrow {\cal C}\) defined by \(\mathscr {I}(S) = S\) and \(\mathscr {I}( f ) = f\) , i.e. it sends objects and arrows of \({\cal S}\) into themselves in category \({\cal C}\). It is automatically faithful, and it is full iff S is a full subcategory.

example. other special functors [kostecki2011introduction, 3.1, example 10, 11, 4.6] [tt-0016]

Some other special functors are introduced in later sections in context, e.g. hom-functor, Yoneda embedding functors.

universal properties [tt-003O]

definition. universal arrow [kostecki2011introduction, 3.4, 3.5] [tt-001A]

A universal arrow from \(X \in {\cal D}\) to \(\mathscr {F} : {\cal C} \to {\cal D}\) is a unique pair \((O , u)\) that makes the diagram commute for any \(f \in {\cal D}\).

Conversely, a (co)universal arrow from \(\mathscr {F} : {\cal C} \to {\cal D}\) to \(X \in {\cal D}\) is a unique pair \((O , u)\) that makes the diagram commute for any \(f \in {\cal D}\).

remark. universal property [leinster2016basic, sec. 1] [tt-002Z]

We say universal arrows satisfy some universal property.

The term universal property is used to describe some property (usually some equality of some compositions, or a commuting diagram in general) that is satisfied for all (hence universal) relevant objects/arrows in the "world" (i.e. in the relevant categories), by a corresponding unique object/arrow.

It's usually spell out like this:

In a context where (usually a given diagram), for all (some objects/arrows), there exists a unique (object/arrow) such that (some property).

Diagramatically,

For clarity and brevity, usually the \(\forall \) clauses are specified outside the diagram, and the \(\exists !\) clause is expressed by dashed arrows. For more elaborate diagrams, see [freyd1976properties][fong2018seven][ochs2022missing].

For the diagram above, we also say that \(f\) uniquely factors through \(u\) along \(g\) [riehl2017category, 2.3.7].

A universal property is a property of some construction which boils down to (is manifestly equivalent to) the property that an associated object is an initial object of some (auxiliary) category [nlab2020univ].

definition. comma category [leinster2016basic, 2.3.1] [tt-001C]

Given categories and functors the comma category \(\mathscr {F} \downarrow \mathscr {G}\) (or \((\mathscr {F} \Rightarrow \mathscr {G})\)) is the category given by objects \((X, h, Y)\) and arrows \((f, g)\) that makes the diagram commute.

lemma. universal arrow via initial/terminal object of comma category [kostecki2011introduction, 3.6] [tt-001B]

A universal arrow from \(X \in {\cal D}\) to \(\mathscr {F} : {\cal C} \to {\cal D}\) is an initial object in the comma category \(X \downarrow \mathscr {F}\).

Conversely, a (co)universal arrow from \(\mathscr {F} : {\cal C} \to {\cal D}\) to \(X \in {\cal D}\) is a terminal object in the comma category \(\mathscr {F} \downarrow X\).

natural transformation and functor category [tt-001M]

definition. natural transformation [leinster2016basic, 1.3.1] [tt-001E]

Given categories and functors

the natural transformation \(\alpha : \mathscr {F} \to \mathscr {G}\), denoted

is a collection of arrows \(\left \{\alpha _X : \mathscr {F}(X) \to \mathscr {G}(X) \right \}_{X \in \operatorname {Ob}({\cal C})}\) in \({\cal D}\) which satisfies naturality, i.e. makes the diagram

commute for every arrow \(f : X \to X'\) in \({\cal C}\). The arrows \(\left \{\alpha _X\right \}_{X \in \operatorname {Ob}({\cal C})}\) are called the components of the natural transformation.

definition. pasting diagram [nakahira2023diagrammatic, table 1.1] [tt-003W]

A pasting diagram represents categories as points (0-dimensional), arrows \(\to \) (1-dimensional), natural transformations as surfaces with level-2 arrows \(\Rightarrow \) (0-dimensional).

For example:

It's dual to a corresponding string diagram

definition. Nat [kostecki2011introduction, 4.4] [tt-001N]

The collection of natural transformations from functors \(\mathscr {F}\) to \(\mathscr {G}\) is denoted \(\operatorname {Nat}(\mathscr {F}, \mathscr {G})\).

notation. string diagrams: functor and natural transformation [marsden2014category, sec. 2] [tt-001G]

In string diagrams,

A functor \(\mathscr {F} : {\cal C} \to {\cal D}\) can be represented as an edge, commonly referred to as a wire:
Functors compose from left to right:
A natural transformation \(\alpha : \mathscr {F} \to \mathscr {F}'\) can be represented as a dot on the wire from top to bottem (the opposite direction of [marsden2014category], but the same as [sterling2023models]), connecting the two functors :
Natural transformations (for the same pair of categories) compose vertically from top to bottem:
Natural transformations (from different pairs of categories) compose horizontally from left to right:
The two ways of composing natural transformations are related by the interchange law: i.e. \[(\alpha \mathbin {\bullet } \alpha ') \mathbin {\bullet } (\beta \mathbin {\bullet } \beta ') = (\alpha \mathbin {\bullet } \beta ) \mathbin {\bullet } (\alpha ' \mathbin {\bullet } \beta ')\]
The naturality in natural transformations is equivalent to the following equality: where \(X\) and \(X'\) are objects in \({\cal C}\), understood as functors from the terminal category \(\mathit {1}\) to \({\cal C}\).
👉
Since a string diagrams is composed from top to bottem, left to right, we can read as \[(X \mathbin {\bullet } \mathscr {F}) \mathbin {\bullet } (\alpha _X) \mathbin {\bullet } (f \mathbin {\bullet } \mathscr {G})=(X' \mathbin {\bullet } \mathscr {G}) \quad {\large =} \quad (X \mathbin {\bullet } \mathscr {F}) \mathbin {\bullet } (f \mathbin {\bullet } \mathscr {F}) \mathbin {\bullet } (\alpha '_X)=(X' \mathbin {\bullet } \mathscr {G})\] where each pair of parentheses corresponds to an overlay in the string diagram, or with the notation in the opposite direction that is more familiar to most: \[\mathscr {G}(f) \circ \alpha _X \circ \mathscr {F}(X) = \mathscr {G}(X') \quad {\large =} \quad \alpha '_X \circ \mathscr {F}(f) \circ \mathscr {F}(X) = \mathscr {G}(X')\] Note that we read the wire from \(\mathscr {F}\) to \(\mathscr {G}\) as \(\mathscr {F}\) before the natural transformation, but as \(\mathscr {G}\) after the transformation.
Effectively naturality says that the natural transformation and function \(f\) “slide past each other”, and so we can draw them as two parallel wires to illustrate this.

definition. functor category [leinster2016basic, 1.3.6] [tt-001F]

The functor category from \({\cal C}\) to \({\cal D}\), denoted \([{\cal C}, {\cal D}]\) or \({\cal D}^{{\cal C}}\), is a category whose objects are functors from \({\cal C}\) to \({\cal D}\) and whose arrows are natural transformations between them, where composition is given by and the identity is given by

remark. indexed, labelled [kostecki2011introduction, 4.5] [tt-001P]

One can think of a functor category \([{\cal C}, {\cal D}]\) or \({\cal D}^{{\cal C}}\) as a category of diagrams in \(D\) indexed (or labelled) by the objects from \({\cal C}\).

This particularly makes sense in a diagram.

definition. natural isomorphism [kostecki2011introduction, 4.2] [tt-001H]

A natural transformation \(\sigma : \mathscr {F} \to \mathscr {G}\) between functors \(\mathscr {F}: {\cal C} \to {\cal D}\) and \(\mathscr {G} : {\cal C} \to {\cal D}\) is called a natural isomorphism or a natural equivalence, denoted \(\sigma : \mathscr {F} \cong \mathscr {G}\), if each component \(\sigma _X : \mathscr {F}(X) \to \mathscr {G}(X)\) is an isomorphism in \({\cal D}\), i.e. \(\mathscr {F}(X) \underset {\sigma _X}{\cong } \mathscr {G}(X)\).

We call \(\mathscr {F}\) and \(\mathscr {G}\) naturally isomorphic to each other.

We also say that \(\mathscr {F}(X) \cong \mathscr {G}(X)\) naturally in \(X\) [leinster2016basic, 1.3.12].

Diagramatically,

lemma. natural isomorphism [leinster2016basic, 1.3.10] [tt-001I]

A natural isomorphism between functors from categories \({\cal C}\) and \({\cal D}\) is an isomorphism in the functor category \([{\cal C}, {\cal D}]\).

definition. isomorphism of categories [kostecki2011introduction, 4.3] [tt-001J]

The cateories \({\cal C}\) and \({\cal D}\) are called isomorphic, denoted \({\cal C} \cong {\cal D}\), iff there exists functors such that \[\mathit {1}_{{\cal C}}=\mathscr {F} \mathbin {\bullet } \mathscr {G}\] and \[\mathit {1}_{{\cal D}}=\mathscr {G} \mathbin {\bullet } \mathscr {F} \]

definition. equivalence of categories [kostecki2011introduction, 4.3] [tt-001K]

The categories \({\cal C}\) and \({\cal D}\) are called equivalent, denoted \({\cal C} \simeq {\cal D}\), iff there exist functors together with natural isomorphisms \[\mathit {1}_{{\cal C}} \cong \mathscr {F} \mathbin {\bullet } \mathscr {G}\] and \[\mathscr {G} \mathbin {\bullet } \mathscr {F} \cong \mathit {1}_{{\cal D}} \]

representables [tt-002K]

remark. representables [leinster2016basic, ch. 4, 4.1.15] [tt-002L]

A category is a world of objects, all looking at one another. Each sees the world from a different viewpoint.

We may ask: what objects see? Fix an object, this can be described by the arrows from it, this corresponds to the covariantly representable functor.

We can also ask the dual question: how objects are seen? Fix an object, this can be described by the arrows into it, this corresponds to the contravariantly representable functor.

definition. set-valued [kostecki2011introduction, 4.4] [tt-001L]

A functor \(\mathscr {F} : {\cal C} \to \mathbf {Set}\) is called set-valued.

definition. hom-functor [kostecki2011introduction, 3.1, example 10] [tt-001S]

For every locally small category \({\cal C}\), the covariant hom-functor, denoted \[{\cal C}(X,-): {\cal C} \to \mathbf {Set} \] is given by

Conversely, the contravariant hom-functor, denoted \[{\cal C}(-,X): {\cal C}^{op} \to \mathbf {Set} \] is given by

Further, the hom-bifunctor, denoted \[{\cal C}(-,=): {\cal C}^{op} \times {\cal C} \to \mathbf {Set} \] defined as a contravariant hom-functor at first argument and as a covariant hom-functor at second argument.

We see \(-\) and \(=\) as placeholders for any object and its "associated arrow" (whose domain/codomain is the object, respectively) in the corresponding category. And we use boxes to mark the placeholder objects in diagrams.

Diagramatically [leinster2016basic, 4.1.22],

definition. representable functor [kostecki2011introduction, 4.4] [tt-001O]

A set-valued functor \(\mathscr {F}: {\cal C} \to \mathbf {Set}\) is called covariantly representable if for some \(X \in {\cal C}\), \[\tau : \mathscr {F} \cong {\cal C}(X,-)\] where \(\cong \) denotes a natural isomorphism.

Conversely, a set-valued functor \(\mathscr {G} : {\cal C}^{op} \to \mathbf {Set}\) is called contravariantly representable if for some \(X \in {\cal C}\), \[\tau : \mathscr {G} \cong {\cal C}(-, X)\]

Such an object \(X\) is called a representing object for the functor \(\mathscr {F}\) or \(\mathscr {G}\), respectively.

The pair \((\tau , X)\) is called a representation of the functor \(\mathscr {F}\) (respectively, \(\mathscr {G}\) ).

remark. representation [leinster2016basic, 4.1.3, 4.1.17] [tt-002M]

A representation \((\tau , X)\) of a representable functor \(\mathscr {F}\) is a choice of an object \(X \in {\cal C}\) and an isomorphism \(\tau \) between the corresponding type of hom-functor and \(\mathscr {F}\).

Representable functors are sometimes just called representables. Only set-valued functors can be representable.

definition. Yoneda embedding functors [leinster2016basic, 4.1.15] [tt-002T]

Let \({\cal C}\) be a locally small category. The covariant Yoneda embedding functor of \({\cal C}\) is the functor \[ \mathscr {H}^{\bullet }: {\cal C}^{op} \to [{\cal C}, \mathbf {Set}] \] defined on objects \(X\) by the covariant hom-functor on \(X\).

This functor embeds what every object in \({\cal C}\) sees the "world" of the category \({\cal C}\), i.e. arrows from each object.

Conversely, the (contravariant) Yoneda embedding functor of \({\cal C}\) is the functor \[ \mathscr {H}_{\bullet }: {\cal C} \to [{\cal C}^{op}, \mathbf {Set}] \] defined on objects \(X\) by the contravariant hom-functor on \(X\).

This functor embeds how every object in \({\cal C}\) is "seen", i.e. arrows to each object.

\(\bullet \) is a placeholder for an object. \(\mathscr {H}^X\) and \(\mathscr {H}_X\) denote the corresponding Yoneda embedding functors applied to \(X\), and are called covariant/contravariant Yoneda functors, respectively.

Diagramatically [rosiak2022sheaf, def. 161]:

When one speaks of the Yoneda (embedding) functor without specifying covariant or contravariant, it means the contravariant one, because it's the one used in the Yoneda lemma.

lemma. Yoneda [leinster2016basic, 4.2.1] [tt-002N]

Let \({\cal C}\) be a locally small category. Then \[ \operatorname {Nat}(\mathscr {H}_X, \mathscr {F}) \cong \mathscr {F}(X) \] naturally in \(X \in {\cal C}\) and \(\mathscr {F} \in \left [{\cal C}^{\mathrm {op}}, \mathbf {Set} \right ]\), where \(\mathscr {H}_X\) is the (contravariant) Yoneda embedding functor on \(X\), and Nat denotes all the natural transformations between the two functors.

notation. Yoneda lemma [leinster2016basic, 4.2.1] [tt-002U]

Diagramatically, \(\operatorname {Nat}(\mathscr {H}_X, \mathscr {F})\) is and it's also denoted by \(\left [{\cal C}^{op}, \mathbf {Set}\right ]\left (\mathscr {H}_X, \mathscr {F}\right )\) in the sense of \(\operatorname {Hom}_{\left [{\cal C}^{op}, \mathbf {Set}\right ]}\left (\mathscr {H}_X, \mathscr {F}\right )\) where \(\left [{\cal C}^{op}, \mathbf {Set}\right ]\) is a functor category.

remark. Yoneda philosophy [rosiak2022sheaf, sec. 6.6] [tt-002S]

The Yoneda lemma can be regarded as saying:

To understand an object it suffices to understand all its relationships with other things.

This is similar to the seventeenth-century philosopher Spinoza's idea that what a body is (its “essence”) is inseparable from all the ways that the body can affect (causally influence) and be affected (causally influenced) by other bodies.

The idea of Yoneda is that we can be assured that if a robot wants to learn whether some object \(X\) is the same thing as object \(Y\), it will suffice for it learn whether \[{\cal C}(-, X) \cong {\cal C}(-, Y)\] or, dually, \[{\cal C}(X, -) \cong {\cal C}(Y, -)\] i.e. whether all the ways of probing \(X\) with objects of its environment amount to the same as all the ways of probing \(Y\) with objects of its environment.

lemma. full and faithful [kostecki2011introduction, 4.8] [tt-002X]

The Yoneda embedding functor \(\mathscr {H}_{\bullet }: {\cal C} \to [{\cal C}^{op}, \mathbf {Set}]\) is full and faithful.

definition. Ob, Arr [leinster2016basic, 4.1.6] [tt-003U]

Given a small category \({\cal C}\), there is a functor \(\operatorname {Ob} : \mathbf {Cat} \to \mathbf {Set}\) that sends \({\cal C}\) to its set of objects where \(\mathbf {Cat}\) is the category of small categories. Thus, \[ \mathscr {H}^{\mathrm {1}}({\cal C}) \cong \operatorname {Ob}({\cal C}) \] where \(\mathscr {H}\) is a Yoneda embedding functor.

This isomorphism is natural in \({\cal C}\); hence \(\operatorname {Ob} \cong \mathbf {Cat}(\mathrm {1}, -)\) where \(\mathbf {Cat}(\mathrm {1}, -)\) is a covariant hom-functor.

Functor \(\operatorname {Ob}\) is representable. Similarly, the functor \(\operatorname {Arr} : \mathbf {Cat} \to \mathbf {Set}\) sending a small category to its set of arrows is representable.

definition. presheaf [leinster2016basic, 1.2.15] [tt-002Q]

Let \({\cal C}\) be a category. A presheaf \(\mathscr {F}\) on \({\cal C}\) is a functor \({\cal C}^{op} \to \mathbf {Set}\).

It is called representable if \(\mathscr {F} \cong \mathscr {H}_X\) for some \(X\).

notation. presheaf [tt-004B]

We'll use \(\mathscr {F}\) to denote a presheaf since sheaf in French is faisceau.

remark. presheaf and Yoneda lemma [leinster2016basic, 4.2.1] [tt-002V]

The Yoneda lemma says that for any \(X \in {\cal C}\) and presheaf \(\mathscr {F}\) on \({\cal C}\), a natural transformation \(\mathscr {H}_X \to \mathscr {F}\) is an element of \(\mathscr {F}(X)\) of shape \(\mathscr {H}_X\).

We may ask the question [chen2016infinitely, 68.6.4]:

What kind of presheaves are already "built in" to the category \({\cal C}\)?

The answer by the Yoneda lemma is, the Yoneda embedding \(\mathscr {H}_{\bullet }: {\cal C} \to [{\cal C}^{op}, \mathbf {Set}]\) embeds \({\cal C}\) into its own presheaf category.

In mathematics at large, the word "embedding" is used (sometimes informally) to mean a map \(i: X \to Y\) that makes \(X\) isomorphic to its image in \(Y\), i.e. \(X \cong i(X)\). [leinster2016basic, 1.3.19] tells us that in category theory, a full and faithful functor \(\mathscr {I}: X \to Y\) can reasonably be called an embedding, as it makes \(X\) equivalent to a full subcategory of \(Y\).

So, \({\cal C}\) is equivalent to the full subcategory of the presheaf category \([{\cal C}^{op}, \mathbf {Set}]\) whose objects are the representables.

definition. The category of presheaves [kostecki2011introduction, 4.5, example 1] [tt-002R]

The functor category of contravariant set-valued functors \([{\cal C}^{op}, \mathbf {Set}]\), called the category of presheaves or varying sets, the objects of which are contravariant functors \({\cal C}^{op} \to \) Set. It may be regarded as a category of diagrams in \(\mathbf {Set}\) indexed contravariantly by the objects of \({\cal C}\).

By definition, objects of \({\cal C}\) play the role of stages, marking the "positions" (in passive view) or "movements" (in active view) of the varying set \(\mathscr {F}: {\cal C}^{op} \to \mathbf {Set}\). For every \(X\) in \({\cal C}^{op}\), the set \(\mathscr {F}(X)\) is a set of elements of \(\mathscr {F}\) at stage \(X\).

An arrow \(f: Y \to X\) between two objects in \({\cal C}^{op}\) induces a transition arrow \(\mathscr {F}(f): \mathscr {F}(X) \to \mathscr {F}(Y)\) between the varying set \(\mathscr {F}\) at stage \(A\) and the varying set \(\mathscr {F}\) at stage \(B\).

basic types of diagrams [tt-000P]

By "basic types of diagrams", we mean some basic structures inside a category.

definition. diagram, shape [leinster2016basic, 5.1.18] [tt-0025]

Let \({\cal C}\) be a category and \({\cal J}\) a small category. A functor \(\mathscr {D} : {\cal J} \to {\cal C}\) is called a diagram in \({\cal C}\) of shape \({\cal J}\).

\({\cal J}\) is also called the indexing category of the diagram, and we say that \(\mathscr {D}\) is a diagram indexed by \({\cal J}\) [rosiak2022sheaf, example 35]. \(J\) is also called the template.

definition. shape E [leinster2016basic, 5.14] [tt-000O]

The diagram is called a diagram of shape E.

For simplicity, we refer to a diagram of shape E by "a shape \(E(f, g)\)".

"E" in "shape E" stands for "equal", and the reason will unfold in the definition of equalizer.

definition. fork [leinster2016basic, 5.4] [tt-000R]

A fork over a shape \(E(f, g)\) is the diagram that makes the diagram commute.

For simplicity, we refer to a fork by "a fork \((E, \iota )\) (over the shape \(E(f, g)\))".

convention. grey arrow [tt-000S]

We use grey arrows to represent the composition arrow in a fork. This convention is not from literatures and is subject to change.

definition. equalizer [leinster2016basic, 5.1.11] [tt-000Q]

An equalizer of a shape \(E(f, g)\) is a fork \((E, \iota )\) over it, such that, for any \((\mathrm {-}, d)\) over the fork, the diagram commutes (i.e. any arrow \(d : \mathrm {-} \to X\) must uniquely factor through \(E\)).

For simplicity, we refer to the equalizer of a shape \(E(f, g)\) as \(\operatorname {Eq}(f, g)\), and \(\iota \) is the canonical inclusion.

We say that a category \({\cal C}\) has equalizers iff every shape E in \({\cal C}\) has an equalizer.

remark. equalizing set [kostecki2011introduction, eq. 32] [tt-000U]

Equalizer in a category is a generalisation of a subset which consists of elements of a given set such that two given functions are equal on them, formally:

For any two arrows \(f, g: X \to Y\), their equalizing set \(E \subseteq X\) is defined as \[ E:=\{e \mid e \in X \wedge f(e)=g(e)\} \]

definition. shape P [leinster2016basic, 5.14] [tt-000W]

The diagram is called a diagram of shape P.

For simplicity, we refer to a diagram of shape P by "a shape \(P(f, g)\)".

"P" in "shape P" may stand for "product/projection/pullback", and the reason will unfold in the definition of pullback.

definition. pullback (fiber product) [kostecki2011introduction, 2.12] [tt-000V]

A pullback of a shape \(P(f, g)\) is an object \(X \times _O Y\) in \({\cal C}\) together with arrows \(p_X\) and \(p_Y\), called projections, such that, for any object \(\mathrm {-}\) and arrows \(h\) and \(k\), the diagram commutes.

We say that a category \({\cal C}\) has pullbacks iff every shape \(P(f, g)\) in \({\cal C}\) has a pullback in \({\cal C}\).

A pullback is also called a fiber product.

The square is called the pullback square of \(f\) and \(g\). The object \(X \times _O Y\) in \({\cal C}\) is called the fiber product object.

lemma. pasting pullbacks [spivak2013category, 2.5.1.17] [tt-0056]

Pullbacks can be pasted together, i.e. for diagram given that the right-hand square is a pullback, the left-hand square is a pullback if and only if the outer rectangle is a pullback.

definition. shape T [leinster2016basic, 5.14] [tt-0026]

The diagram is called a diagram of shape T.

For simplicity, we refer to a diagram of shape T by "a shape \(T(X, Y)\)" where \(X\) and \(Y\) are the 2 objects.

"T" in "shape T" stands for "two". Shape T is useful in the definition of binary product [kostecki2011introduction, 2.18].

definition. binary product [kostecki2011introduction, 2.18] [tt-000Y]

A binary product of objects \(X\) and \(Y\) is an object \(X \times Y\) in \({\cal C}\) together with arrows \(p_X\) and \(p_Y\), called projections, such that, for any object \(\mathrm {-}\) and arrows \(h\) and \(k\), the diagram

commutes.

We say that a category \({\cal C}\) has binary products iff every pair \(X, Y\) in \({\cal C}\) has a binary product \(X \times Y\) in \({\cal C}\).

When there is no confusion, we simply call bianry products products.

definition. coshape, coequalizer, pushout (fiber coproduct), binary coproduct [kostecki2011introduction, 2.14, 2.16, 2.19] [tt-000X]

coshape, coequalizer, pushout (fiber coproduct), binary coproduct can be defined by reversing all arrows in the definitions of shape, equalizer, pullback (fiber product), binary product respectively.

The pushout equivalent of the fiber product object in pullback is the fiber coproduct object, denoted \(X +_{O} Y\), and the pushout equivalent of projections in pullback are injections, denoted \(i_X\) and \(i_Y\), respectively. The unique arrow of a pushout is denoted \([f, g]\).

The binary coproduct equivalent of the binary product object in binary product is the binary coproduct object, denoted \(X + Y\), and the binary coproduct equivalent of projections in binary product are injections, denoted \(i_X\) and \(i_Y\), respectively. The unique arrow of a binary coproduct is denoted \([f, g]\).

Diagramatically,

Coshapes:
- \(T\) =
- \(E\) =
- \(P\) =
coequalizer:
pushout (fiber coproduct):
binary coproduct:

lemma. monic and pullback [leinster2016basic, 5.1.32] [tt-003J]

An arrow \(X \xrightarrow {f} Y\) is monic iff the square is a pullback.

The significance of this lemma is that whenever we prove a result about limits, a result about monics will follow.

lemma. epic and pushout [leinster2016basic, sec. 5.2] [tt-003M]

An arrow \(X \xrightarrow {f} Y\) is epic iff the square is a pushout.

This is dual to lemma [tt-003J].

definition. n-fold (co)products [kostecki2011introduction, 2.22] [tt-0011]

In any category with binary products the objects \(X \times (Y \times Z)\) and \((X \times Y) \times Z\) are isomorphic. In any category with binary coproducts the objects \(X+(Y+Z)\) and \((X+Y)+Z\) are isomorphic.

This allows to consider \(n\)-fold products \(X_1 \times \dots \times X_n\) and \(n\)-fold coproducts \(X_1 + \dots + X_n\) of objects of a given category.

definition. have finite (co)products [kostecki2011introduction, 2.23] [tt-0012]

A category which has n-fold (co)products for any \(n \in \mathbb N\) is said to have finite (co)products.

limits [tt-0023]

remark. Limits [leinster2016basic, ch. 5] [tt-0024]

Adjointness is about the relationships between categories. Representability is a property of set-valued functors. Limits are about what goes on inside a category.

Whenever you meet a method for taking some objects and arrows in a category and constructing a new object out of them, there is a good chance that you are looking at either a limit or a colimit.

definition. cone [leinster2016basic, 5.1.19] [tt-0028]

Let \({\cal C}\) be a category, \({\cal J}\) a small category, and \(\mathscr {D} : {\cal J} \to {\cal C}\) a diagram in \({\cal C}\) of shape \({\cal J}\).

A cone on \(\mathscr {D}\) is an object \(V \in {\cal C}\) (the vertex of the cone) together with a family \[ \left (V \xrightarrow {\pi _J} \mathscr {D}(J)\right )_{J \in {\cal J}} \] of arrows in \({\cal C}\) such that for all arrows \(J \to J'\) in \({\cal J}\), the diagram commutes.

The family of arrows are components of a natural transformation \(\pi : \Delta _V \to \mathscr {D}\), i.e. from the constant functor ( which assigns the same object \(V\) to any object \(J_i\) in \({\cal J}\)) to diagram functor \(\mathscr {D}\).

For simplicity, we refer to a cone by "a cone \((V, \pi )\) on \(\mathscr {D}\)".

example. a cone on a diagram [kostecki2011introduction, 4.9] [tt-0029]

The cone for a diagram is which indeed looks like a cone with the vertex \(V\).

definition. limit [kostecki2011introduction, 4.10] [tt-002A]

A cone \((V, \pi )\) on \(\mathscr {D} : {\cal C} \to {\cal J}\) is called a limit of \(\mathscr {D}\), denoted \[\lim \mathscr {D}\] if the diagram commutes for every cone \((V, \pi )\) on \(\mathscr {D}\).

The arrows \(\pi _J\) are called the projections of the limit.

Other possible terms of limit are limiting cone, universal cone.

example. limits [kostecki2011introduction, 4.11, example 1-4] [tt-002B]

The basic types of diagrams are actually examples of limits:

binary product [kostecki2011introduction, 2.18]:
pullback (fiber product) [kostecki2011introduction, 2.12]:
equalizer [leinster2016basic, 5.1.11]:
the limit of \(\mathscr {D} : \mathbf {\emptyset } \to {\cal C} \), where \(\mathbf {\emptyset }\) is an empty category: i.e. the terminal object \(\mathrm {1}\) in \({\cal C}\). In particular, for \({\cal C} = \mathbf {Set}\) we have \[\mathrm {-} \xrightarrow {!} V = \lim \mathscr {D} = \{∗\} \]

remark. cocone, colimit [kostecki2011introduction, 4.10] [tt-002E]

A cocone and a colimit are defined by dualization, that is, by reversing the arrows in cone [leinster2016basic, 5.1.19] and limit [kostecki2011introduction, 4.10].

In another word, given \(\mathscr {D}^{op} : {\cal J}^{op} \to {\cal C}^{op}\), a cocone on \(\mathscr {D}\) is a cone on \(\mathscr {D}^{op}\), a colimit of \(\mathscr {D}\) is a limit of \(\mathscr {D}^{op}\) [leinster2016basic, 5.2.1].

The arrows \(\pi _J\) are called the coprojections of the colimit.

In the same say, one can and show that coequaliser, coproduct, pushout and initial object are examples of colimits.

lemma. limits via products and equalizers [stacks2017stacks, 002N, 002P] [tt-0057]

If all products and equalizers exist, all limits exist.

Dually, if all coproducts and coequalizers exist, all colimits exist.

definition. has (finite) limits, (finitely) complete, left exact [kostecki2011introduction, 4.10] [tt-002F]

We say that a category \({\cal C}\) has (finite) limits or is (finitely) complete if every diagram \(\mathscr {D} : {\cal J} \to {\cal C}\), where \({\cal J}\) is a (finite) category, has a limit.

A category \({\cal C}\) is called left exact iff it is finitely complete.

remark. (finitely) cocomplete, right exact [kostecki2011introduction, 4.10] [tt-003C]

Dually to definition [tt-002F], when every diagram \(\mathscr {D} : {\cal J} \to {\cal C}\), where \({\cal J}\) is a (finite) category, has a colimit, it is said that the category \({\cal C}\) has (finite) colimits or is (finitely) cocomplete.

A category is called right exact iff it is finitely cocomplete.

lemma. (finitely) (co)complete category [kostecki2011introduction, 4.14] [tt-002J]

A category \({\cal C}\) is (finitely) complete if it has a terminal object, equalizers and (finite) products, or if it has a terminal object and (finite) pullbacks.

Dually, a category \({\cal C}\) is (finitely) cocomplete if it has an initial object, coequalizers and (finite) coproducts, or if it has an initial object and (finite) pushouts.

lemma. (co)complete functor category [kostecki2011introduction, 4.15] [tt-002I]

If category \({\cal D}\) is complete and category \({\cal C}\) is small, then the functor category \({\cal D}^{{\cal C}}\) is complete.

Dually, if category \({\cal D}\) is cocomplete and category \({\cal C}\) is small, then the functor category \({\cal D}^{{\cal C}}\) is cocomplete.

definition. preorder, partial order, total order [kostecki2011introduction, 1.2, example 9] [tt-002C]

Let \(P\) be a set. The properties

(reflexivity) \(\forall p \in P, p \leq p\)
(transitivity) \(\forall p, q, r \in P, p \leq q \wedge q \leq r \Rightarrow p \leq r\)

define a preorder \((P, \leq )\).

A partially ordered set (called a partial order, or a poset) is defined as a preorder \((P, \leq )\) for which

(antisymmetry) \(\forall p \in P, p \leq q \wedge q \leq p \Rightarrow p=q\)

holds.

A total order (or a linear order) is a partial order \((P, \leq )\) for which

(comparability) \(\forall p, q \in P, p \leq q \vee q \leq p\)

The category \(\mathbf {Preord}\) consists of objects which are preorders and of arrows which are orderpreserving functions.

The category \(\mathbf {Poset}\) consists of objects which are posets and of arrows which are order-preserving functions between posets, that is, the maps \(T: P \to P'\) such that \[ p \leq q \Rightarrow T(p) \leq T(q) \]

Any any preorder \((P, \leq )\) and poset \((P, \leq )\) can be considered as a category consisting of objects which are elements of a set \(P\) and arrows defined by \(p \to q \Longleftrightarrow p \leq q\).

definition. directed poset [rosiak2022sheaf, def. 285] [tt-0051]

A directed poset is a poset that is inhabited (nonempty) and for which every finite subset has an upper bound. Explicitly,

(directedness) \(\forall x,y \in P, \exists z \in P, x \leq z \land y \leq z\)

example. preorder, poset, directed poset [tt-0052]

An example of a preorder category which is not poset is:

An example of a poset category which is not a directed poset is [rosiak2022sheaf, example 3] :

An example that is a directed poset category but not a total order is: where each pair of nodes has a common upper bound (thus satisfying directedness), but there is no path between the two nodes on the center, thus violating comparability.

A more complicated example of a directed poset category which is not a total order is [spivak2013category, example 3.4.1.3]:

One can see immediately that this is a preorder because length=0 paths give reflexivity and concatenation of paths gives transitivity. To see that it is a partial order we only note that there are no loops.

To see that it is a poset, we note that every pair of nodes from one side or both sides has the central node as an upper bound, thus satisfying directedness.

But this partial order is not a total order because there is no path (in either direction) between some nodes, thus violating comparability.

definition. inverse limit, projective limit [kostecki2011introduction, 4.11] [tt-002D]

Let \({\cal J}\) be a directed poset and \(\mathscr {F} : {\cal J} \to {\cal C}\) be a contravariant functor. The limit of \(\mathscr {F}\) is called an inverse limit or projective limit, and is denoted \(\lim \limits _{\leftarrow {\cal J}} \mathscr {F}\) or simply \(\lim \limits _{\longleftarrow } \mathscr {F}\).

definition. direct limit, inductive limit [kostecki2011introduction, 4.12] [tt-002G]

Let \({\cal J}\) be a directed poset and \(\mathscr {F}: {\cal J} \to {\cal C}\) be a contravariant functor. The colimit of \(\mathscr {F}\) is called a direct limit (some called directed limit) or inductive limit, and is denoted \(\lim \limits _{\to {\cal J}} \mathscr {F}\), or simply \(\lim \limits _{\longrightarrow } \mathscr {F}\).

This is dual to inverse limit.

definition. preserves (all) (co)limits, left/right exact [kostecki2011introduction, 4.13] [tt-002H]

A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) preserves (all) limits and is called left exact iff it sends all limits in \({\cal C}\) into limits in \({\cal D}\).

Dually, a functor \(\mathscr {F}: {\cal C} \to {\cal D}\) preserves (all) colimits and is called right exact iff it sends all colimits in \({\cal C}\) into colimits in \({\cal D}\).

remark. directions in (co)limits [tt-004Y]

	Limit	Colimit
diagram
arrows through the vertex	into the diagram	out of the diagram
on (co)shape P	pullback	pushout
categories have finite ...	left exact	right exact
functors preserve all ...	left exact	right exact
on directed poset	inverse/projective limit \(\lim \limits _{\longleftarrow } \mathscr {F}\)	direct/inductive limit \(\lim \limits _{\longrightarrow } \mathscr {F}\)

One can see from the table that, in general, limits have the direction "back" "into" (where "back", "left", "inverse" are directional consistent), and colimits have the opposite: "forward" "out of".

This might help to memorize the directions in these concepts without disorientation.

adjunctions [tt-001T]

definition. adjoint functor [kostecki2011introduction, 5.1] [tt-001Q]

Given functors we say \(\mathscr {L}\) and \(\mathscr {R}\) are a pair of adjoint functors, or together called an adjunction between them, \(\mathscr {L}\) is called left adjoint to \(\mathscr {R}\), and \(\mathscr {R}\) is called right adjoint to \(\mathscr {L}\), denoted \[\mathscr {L} \dashv \mathscr {R} : {\cal C} \rightleftarrows {\cal D}\] or iff there exists a natural isomorphism \(\sigma \) between the following two hom-bifunctors: \[ {\cal D}(\mathscr {L}(-), =) \cong {\cal C}(-, \mathscr {R}(=)) \] diagramatically,

The components of the natural isomorphism \(\sigma \) are isomorphisms \[ \sigma _{XY} : {\cal D}(\mathscr {L}(X), Y) \cong {\cal C}(X, \mathscr {R}(Y)) \]

remark. adjoint functor [kostecki2011introduction, 5.1] [tt-001R]

An adjunction \(\mathscr {L} \dashv \mathscr {R}\) means arrows \(\mathscr {L}(X) \to Y\) are essentially the same thing as arrows \(X \to \mathscr {R}(Y)\) for any \(X \in {\cal C}\) and \(Y \in {\cal D}\).

This means the diagram commutes for any arrows \(f: \mathscr {L}(X) \to Y\) in \({\cal D}\).

The above can also be diagramatically denoted by transposition diagram \[ \begin {array}{ccccccc} X' & \xrightarrow {x} & X & \xrightarrow {\sigma _{X Y}(f)} & \mathscr {R}(Y) & \xrightarrow {\mathscr {R}(y)} & \mathscr {R}\left (Y'\right ) \\ \hline \mathscr {L}\left (X'\right ) & \xrightarrow {\mathscr {L}(x)} & \mathscr {L}(X) & \xrightarrow {f} & Y & \xrightarrow {y} & Y' \end {array} \] or simply, \[ \frac {X \to \mathscr {R}(Y) \quad ({\cal C})}{\mathscr {L}(X) \to Y \quad ({\cal D})} \]

An adjunction is a concept that describes the relationship between two functors that are weakly inverse to each other [nakahira2023diagrammatic, sec. 4].

By "weakly inverse", we don't mean that applying one after the other gives the identity functor, but in a sense similar to eroding (i.e. enhancing holes) and dilating (i.e. filling holes) an image, applying them in different order yeilds upper/lower "bounds" of the original image [rosiak2022sheaf, sec. 7.1].

notation. string diagrams: adjunction [nakahira2023diagrammatic, sec. 3.1] [tt-001U]

Here we follow the string diagram style of [marsden2014category] and [sterling2023models], but with additional string diagram types inspired by [nakahira2023diagrammatic, eq. 3.1, 4.3].

The covariant hom-functor \({\cal C}(X, -)\), denoted \(-^X\), can be represented in string diagrams as where the dotted circle denotes any arrows with the domain \(X\) and codomain \(-\).
The contravariant hom-functor \({\cal C}(-, X)\), denoted \(X^-\), can be represented in a similar manner.
The hom-bifunctor \({\cal C}(-,=)\), also denoted \(=^-\), can be represented as where the dotted circle denotes any arrows with the domain \(-\) and codomain \(=\).
The natural isomorphism \[{\cal D}(\mathscr {L}(-), =) \cong {\cal C}(-, \mathscr {R}(=))\] in adjunction can be represented as

definition. transpose [kostecki2011introduction, 5.1] [tt-001X]

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), there exists \(f^{\sharp }\) and \(g^{\flat }\) such that the diagrams commute for any arrow \(f: X \to \mathscr {R}(Y)\) in \({\cal C}\), \(g: \mathscr {L}(X) \to Y\) in \({\cal D}\).

\(f^{\sharp }\) is called the left transpose of \(f\). \(g^{\flat }\) is called the right transpose of \(g\).

Other possible terms are left/right adjunct of each other, and mates [nlab2023adjunct].

remark. idempotent [zhang2021type, 5.30] [tt-0037]

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), we may obtain two endofunctors \( \mathscr {L} \mathbin {\bullet } \mathscr {R} : {\cal C} \to {\cal C}\) and \( \mathscr {R} \mathbin {\bullet } \mathscr {L} : {\cal D} \to {\cal D}\) that commute the diagram that means they are both idempotent, i.e. applying \(\mathscr {L} \mathbin {\bullet } \mathscr {R}\) any times yields the same result as applying it once, and similarly for \(\mathscr {R} \mathbin {\bullet } \mathscr {L}\).

definition. (co)unit [zhang2021type, 5.30] [tt-001V]

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), the natural transformation \[\eta : \mathit {1}_{{\cal C}} \to \mathscr {L} \mathbin {\bullet } \mathscr {R} \] is called the unit of the adjunction, and \[\epsilon : \mathscr {R} \mathbin {\bullet } \mathscr {L} \to \mathit {1}_{{\cal D}}\] is called the counit.

We call an arrow \[\eta _X: X \to (\mathscr {L} \mathbin {\bullet } \mathscr {R})(X)\] a unit over \(X\), and \[\epsilon _Y: (\mathscr {R} \mathbin {\bullet } \mathscr {L})(Y) \to Y\] a counit over \(Y\). They are components of the natural transformations \(\eta \) and \(\epsilon \), respectively.

Diagramatically, the diagrams commute.

lemma. universality of (co)unit [kostecki2011introduction, 5.3] [tt-001W]

The unit \(\eta \) and counit \(\epsilon \) of an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\) are universal, i.e. the diagram commutes for any \(f \in {\cal C}\), and the diagram commutes for any \(g \in {\cal D}\).

lemma. triangle identities [kostecki2011introduction, 5.4] [tt-001Z]

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), the diagrams commute.

Note that \(\mathscr {L}\) in \(\epsilon _\mathscr {L}\) is a subscript, meaning \(\epsilon _\mathscr {L}: {\cal D} \to {\cal D}, \mathscr {L}(X) \mapsto \epsilon _{\mathscr {L}(X)}\) for \(X \in {\cal C}\). Similar for \(\eta _\mathscr {R}\).

lemma. snake identities [nakahira2023diagrammatic, thm. 4.8] [tt-0030]

Continuing from notation [tt-001U], the triangle identities can be represented in string diagrams as follows, and called the snake identities (or zig-zag identities): where are the unit and counit of the adjunction, respectively.

notation. string diagram: snake identities [nakahira2023diagrammatic, thm. 4.8] [tt-0031]

Following notation [tt-001G], recall that a string diagram is composed from top to bottem, left to right, we can read the left snake in snake identities as \[ \mathscr {L} \xmapsto {(\eta \mathbin {\bullet } \mathscr {L}) \mathbin {\bullet } (\mathscr {L} \mathbin {\bullet } \epsilon )} \mathscr {L}\]

where each pair of parentheses corresponds to an overlay in the string diagram, and this is equivalent to

in triangle identities.

lemma. (co)unit and transposes [leinster2016basic, 2.2.4] [tt-001Y]

Given an adjunction with unit \(\eta \) and counit \(\epsilon \), the diagrams \[h=\eta _X \mathbin {\bullet } \mathscr {R}(h^{\sharp })\] and \[f^{\sharp }=\mathscr {L}(f) \mathbin {\bullet } \epsilon _Y\] commute.

notation. string diagrams: (co)unit and transposes [marsden2014category, lem. 3.6] [tt-0033]

In string diagrams, lemma [tt-001Y] can be represented as:

remark. topologically plausible [leinster2016basic, 2.2.9] [tt-0039]

The string diagrams in lemma [tt-0030] and notation [tt-0033] are topologically plausible equations, i.e. the equality can be obtained by simply pulling the string straight.

lemma. (co)unit and natural isomorphism [kostecki2011introduction, eq. 127] [tt-0020]

The natural transformation \(\sigma _{XY}\) and \(\tau _{XY}\) that are the components of the natural isomorphism in the adjunction \(\mathscr {L} \dashv \mathscr {R} : {\cal C} \rightleftarrows {\cal D}\) are related to the unit and counit of the adjunction: \[\begin {aligned} \sigma _{XY}(f) & = \eta _X \mathbin {\bullet } \mathscr {R}(f^{\sharp })\\ \tau _{XY}(g) & = \mathscr {L}(g^{\flat }) \mathbin {\bullet } \epsilon _Y \end {aligned} \] and they are reverse of each other \[\sigma _{XY} = \tau _{YX}^{-1}\]

proof.

This can be read out from the diagrams in universality of (co)unit [kostecki2011introduction, 5.3] and transpose [kostecki2011introduction, 5.1].

lemma. uniqueness of adjoints [kostecki2011introduction, 5.8] [tt-0021]

A left or right adjoint, if it exists, is unique up to natural isomorphism.

proof.

For the left adjoint, from the university of \(\eta \) it follows that there exists a unique, up to isomorphism, isomorphism between different left adjoints. It remains to show naturality of this isomorphim, which is left as an exercise. The proof for right adjoint follows by duality.

theorem. adjunction via (co)units [leinster2016basic, 2.2.5] [tt-0038]

Given categories and functors there is a one-to-one correspondence between the adjunction \(\mathscr {L} \dashv \mathscr {R}\) and the pairs of natural transformations \(\eta \) and \(\epsilon \) satisfying the the triangle identities.

proof.

From lemma [tt-001Z], it follows that every adjunction between \(\mathscr {L}\) and \(\mathscr {R}\) gives rise to a pair of transformations \(\eta \) and \(\epsilon \) satisfying the triangle identities.

To show that there exists a unique adjunction for \(\eta \) and \(\epsilon \), the uniqueness follows from lemma [tt-001Y], the existence can use the construction in the spirit of definition [tt-001X].

theorem. adjunction via initial objects [leinster2016basic, 2.3.6] [tt-003A]

Given categories and functors there is a one-to-one correspondence between:

the adjunction \(\mathscr {L} \dashv \mathscr {R}\)
natural transformations \(\eta : \mathit {1}_{{\cal C}} \to \mathscr {L} \mathbin {\bullet } \mathscr {R}\) such that \(\eta _X\) is initial in the comma category \(X \Rightarrow \mathscr {R}\) for every \(X \in {\cal C}\)

Diagramatically, where the functor \(X\) is the constant object functor.

interactions [tt-002P]

remark. interactions [leinster2016basic] [tt-0043]

In this section, we will discuss the interactions between

(co)limits
adjunctions
representables

and their relationships with universal properties.

lemma. adjunction preserves (co)limits [leinster2016basic, 6.3.1] [tt-002O]

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), \(\mathscr {L}\) preserves colimits, and \(\mathscr {R}\) preserves limits.

Explictly, given \(\mathscr {D}: {\cal J} \to {\cal C}\), we have \[(\operatorname {colim} \mathscr {D}) \mathbin {\bullet } \mathscr {L} \cong \operatorname {colim}(\mathscr {D} \mathbin {\bullet } \mathscr {L})\] and given \(\mathscr {D}': {\cal J} \to {\cal D}\), we have \[(\lim \mathscr {D}') \mathbin {\bullet } \mathscr {R} \cong \lim (\mathscr {D}' \mathbin {\bullet } \mathscr {R})\]

corollary. a representation is a universal element [leinster2016basic, 4.3.2] [tt-0035]

Let \({\cal C}\) be a locally small category and \(\mathscr {F} : {\cal C}^{op} \to \mathbf {Set}\). Then a representation of \(\mathscr {F}\) consists of a pair \((X, u)\) such that the diagram commutes.

remark. universal element [leinster2016basic, 4.3.2] [tt-0036]

Pairs \((Y, y)\) with \(Y \in {\cal C}\) and \(y \in \mathscr {F}(Y)\) in corollary [tt-0035] are sometimes called elements of the presheaf \(\mathscr {F}\).

Indeed, lemma [tt-002N] (Yoneda) tells us that \(y\) amounts to a generalized element of \(\mathscr {F}\) of shape \(\mathscr {H}_Y\).

An element \(u\) satisfying condition in corollary [tt-0035] is sometimes called a universal element of \(\mathscr {F}\). So, corollary [tt-0035] says that a representation of a presheaf \(\mathscr {F}\) amounts to a universal element of \(\mathscr {F}\).

lemma. adjunction and representable [leinster2016basic, 4.1.11] [tt-003I]

Any set-valued functor with a left adjoint is representable.

definition. cone as a natural transformation [leinster2016basic, eq. 6.1] [tt-0040]

Now, given a diagram \(\mathscr {D}: {\cal J} \to {\cal C}\) and an object \(V \in {\cal C}\), a cone on \(\mathscr {D}\) with vertex \(V\) is simply a natural transformation from the diagonal functor \(\Delta _V\) to the diagram \(\mathscr {D}\).

Writing \(\operatorname {Cone}(V, \mathscr {D})\) for the set of cones on \(\mathscr {D}\) with vertex \(V\), we therefore have \[ \operatorname {Cone}(V, \mathscr {D})=[{\cal J}, {\cal C}] (\Delta _V, \mathscr {D}) . \]

Thus, \(\operatorname {Cone}(V, \mathscr {D})\) is functorial in \(V\) (contravariantly) and \(\mathscr {D}\) (covariantly).

lemma. limit via representation [leinster2016basic, 6.1.1] [tt-003Y]

Let \({\cal J}\) be a small category, \({\cal C}\) a category, and \(\mathscr {D}: {\cal J} \to {\cal C}\) a diagram. Then there is a one-to-one correspondence between

limit cones on \(\mathscr {D}\)
representations of the natural transformation Cone

with the representing objects being the limit objects (i.e. the vertices) of \(\mathscr {D}\).

Briefly put: a limit \((V, \pi )\) of \(\mathscr {D}\) is a representation of \([{\cal J}, {\cal C}] (\Delta _{-}, \mathscr {D})\).

Diagramatically,

It implies that \[\operatorname {Cone}(\mathrm {-}, \mathscr {D}) \cong {\cal C}\left (\mathrm {-}, \lim \limits _{\leftarrow {\cal J}} \mathscr {D} \right )\] for any \(\mathrm {-} \in {\cal C}\).

lemma. representables preserve limits [leinster2016basic, 6.2.2] [tt-0042]

Let \(\mathscr {A}\) be a locally small category and \(X \in {\cal C}\). Then \({\cal C}(X,-): {\cal C} \to \mathbf {Set}\) preserves limits.

proof.

It follows from lemma [tt-003Y] and that [leinster2016basic, 6.2.1] \[\operatorname {Cone}(X, \mathscr {D}) \cong \lim \limits _{\leftarrow {\cal J}} {\cal C}(X, \mathscr {D})\] naturally in \(X\) and \(\mathscr {D}\).

lemma. limits commute with limits [leinster2016basic, 6.2.8] [tt-0047]

Let \({\cal I}\) and \({\cal J}\) be small categories. Let \({\cal C}\) be a locally small category with limits of shape \({\cal I}\) and of shape \({\cal J}\).

Define \[\begin {array}{llll} \mathscr {D}^{\bullet }: & {\cal I} & \to & {[{\cal J}, {\cal C}]} \\ & I & \mapsto & \mathscr {D}(I,-) \end {array}\] and \[\begin {array}{rrrr} \mathscr {D}_{\bullet }: & {\cal J} & \to & {[{\cal I}, {\cal C}]} \\ & J & \mapsto & \mathscr {D}(-, J) \end {array}\]

Then for all \(\mathscr {D}: {\cal I} \times {\cal J} \to {\cal C}\), we have \[ \lim _{\leftarrow {\cal J}} \lim _{\leftarrow {\cal I}} \mathscr {D}^{\bullet } \cong \lim _{\leftarrow {\cal I} {\cal J}} \mathscr {D} \cong \lim _{\leftarrow {\cal I} \leftarrow {\cal J}} \mathscr {D}_{\bullet } \] and all these limits exist. In particular, \({\cal C}\) has limits of shape \({\cal I} \times {\cal J}\).

lemma. colimits commute with colimits [leinster2016basic, 6.2.10] [tt-0049]

Dual to lemma [tt-0047], colimits commute with colimits.

remark. [leinster2016basic, 6.2.10] [tt-004A]

Limits do not in general commute with colimits.

Some special cases where they do:

filtered colimits commute with finite limits [stacks2017stacks, 002W].

lemma. initial and terminal objects via adjunction [leinster2016basic, 2.1.9] [tt-0054]

Initial and terminal objects can be described as adjoints. Let \({\cal C}\) be a category. There exist the unique functor \(! : {\cal C} \to \mathbf {1}\), and a constant object functor \(X : 1 \to {\cal C}\) for each object \(X\).

A left adjoint to \(!\) is exactly an initial object of \({\cal C}\): \[ \mathrm {0} \dashv \ ! : \mathbf {1} \rightleftarrows {\cal C} \]

Similarly, a right adjoint to \(!\) is exactly a terminal object of \({\cal C}\): \[ ! \dashv \mathrm {1} : {\cal C} \rightleftarrows \mathbf {1} \]

proof.

In both cases, being an adjunction gives an isomorphism for each object \(X\), one side of the isomorphism is \(\mathbf {1}(\mathrm {*}, \mathrm {*})\) which is just \(\mathit {1}_{\mathrm {*}}\), and the other side are \({\cal C}(\mathrm {0}, X)\) or \({\cal C}(X, \mathrm {1})\), and the isomorphism establishes the uniqueness of the arrows (from \(\mathrm {0}\) or to \(\mathrm {1}\)) for each object. The initial or terminal object exists if the corresponding adjunction exists.

lemma. (co)limits via adjunction [rosiak2022sheaf, example 200] [tt-005A]

(Co)limits can be phrased entirely in terms of adjunctions:

The advantages of this adjunction perspective is that the (co)limit of every \({\cal J}\)-shaped diagram in \({\cal C}\) can be defined all at once.

cartesian closed categories [tt-004S]

definition. evaluation [leinster2016basic, 6.2.4] [tt-0044]

Let \({\cal S}\) be a small category, \({\cal C}\) a locally small category. For each \(X \in {\cal S}\), there is a functor \[ \begin {array}{lccc} \operatorname {ev}_X: & [{\cal S}, {\cal C}] & \to & {\cal C} \\ & \mathscr {F} & \mapsto & \mathscr {F}(X) \end {array} \] called evaluation at \(X\).

Given a diagram \(\mathscr {D}: {\cal J} \to [{\cal S}, {\cal C}]\), we have for each \(X \in {\cal S}\) a functor \[ \begin {array}{lccc} \mathscr {D} \mathbin {\bullet } \operatorname {ev}_X : & {\cal J} & \to & {\cal C} \\ & J & \mapsto & \mathscr {D}(J)(X) \end {array} \]

We write \(\mathscr {D} \mathbin {\bullet } \operatorname {ev}_X\) as \(\mathscr {D}(-)(X)\).

definition. cartesian product functor [kostecki2011introduction, 5.13] [tt-004F]

If \({\cal C}\) is a category with binary products, we can define for every \(X\) the cartesian product functor \(X \times (-)\) : \({\cal C} \rightarrow {\cal C}\), with the following action: \[ \begin {aligned} & (X \times (-))(Y)=X \times Y \\ & (X \times (-))(f)=\operatorname {id}_X \times f \end {aligned} \]

definition. exponential [kostecki2011introduction, 5.13] [tt-004G]

If for \(X \in {\cal C}\), a cartesian product functor \(X \times (-)\) has a right adjoint, it is called an exponential or the exponential object, denoted \((-)^X\).

Explicitly, \(X \times (-) \dashv (-)^X\) means there is a natural isomorphism of bifunctors \(\operatorname {Hom}(X \times (-),-) \cong \operatorname {Hom}(-, (-)^X)\), i.e. for any arrow \(f: X \times Y \to Z\) there is a unique arrow \(f^b: Y \to Z^X\), which is the transpose of the adjunction, called exponential transpose.

The arrow \(\operatorname {ev} : X \times (-)^X \to (-)\) is called the evaluation arrow of the exponential, and is the counit of the adjunction.

Diagramatically, the diagram commutes.

We say that category \({\cal C}\) has exponentials if for any \(X \in {\cal C}\), there exists an exponential \((-)^X\).

definition. cartesian closed category [kostecki2011introduction, 5.14] [tt-004H]

A category \({\cal C}\) is called cartesian closed iff \({\cal C}\) has exponentials and has finite products.

definition. power object [kostecki2011introduction, 6.8] [tt-004L]

The power object \(P(X)\) of an object \(X\) in a cartesian closed category \({\cal C}\) with subobject classifier \(\Omega \) is defined as the exponential object \(\Omega ^X\).

If \(\Omega ^X\) exists for any \(X\) in \({\cal C}\), we say that \({\cal C}\) has power objects.

lemma. properties of cartesian closed categories [kostecki2011introduction, 5.15] [tt-004N]

For any cartesian closed category \({\cal C}\), and any objects \(X, Y, Z\) of \({\cal C}\), we have

\(\mathrm {0} \times X \cong \mathrm {0}\) if \(\mathrm {0}\) exists in \({\cal C}\)
\(1 \times X \cong X\)
\(X^{\mathrm {0}} \cong \mathrm {1}\) if \(\mathrm {0}\) exists in \({\cal C}\)
\(X^1 \cong X\)
\(\mathrm {1}^X \cong 1\)
\(X \times Y \cong Y \times X\)
\((X \times Y) \times Z \cong X \times (Y \times Z)\)
\(Y^X \times Z^X \cong (Y \times Z)^X\)
\(Z^{X \times Y} \cong \left (Z^X\right )^Y\)
\(X+Y \cong Y+X\)
\((X+Y)+Z \cong X+(Y+Z)\)
\(Z^X \times Z^Y \cong Z^{X+Y}\) if \({\cal C}\) has binary coproducts
\((X \times Y)+(X \times Z) \cong X \times (Y+Z)\) if \({\cal C}\) has binary coproducts

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:

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 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 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)) \]

Topos theory [tt-004U]

definition. topos [kostecki2011introduction, 7.1] [tt-004O]

A topos or elementary topos is a category satisfying one of these equivalent conditions:

it is a complete category with exponentials and subobject classifier
it is a complete category with subobject classifier and its power object
it is a cartesian closed category with equalizers and subobject classifier

Since the completeness of a category with subobject classifier implies its cocompleteness. Thus a topos not only has all finite limits, but also has all finite colimits.

This means that topos is such category which has, in particular,

terminal object
equalizers
pullbacks
all other limits
exponential objects
subobject classifier

remark. topoi, toposes [kostecki2011introduction, 7.1] [tt-004P]

The name "topos" originates from the Greek word "τoπoς", meaning a place, as topos could mean a place of geometry, and at the same time as a place of logic.

Following the ancient Greek naming convention, the plural of topos is topoi, but people also use toposes. We use them interchangeably.

example. topos [tt-004R]

Topos theory unifies, in an extraordinary way, important aspects of geometry and logic.

Grothendieck topos was first introduced by Grothendieck to generalize topological space [kostecki2011introduction, 7.2]:

every space gives rise to a topos (namely, the category of sheaves on it).

Topological properties of the space can be reinterpreted in a useful way as categorical properties of its associated topos.

Elementary topos was introduced by Lawvere and Tierney, to generalize Set. A topos can be regarded as a 'universe of sets' [leinster2016basic, 6.3.20]. \(\mathbf {Set}\) is the most basic example of a topos, and every topos shares enough features with Set that [⧉]

anything you really really needed to do in the category of sets can be done in any topos.

Every presheaf category, is a topos. [leinster2016basic, 6.3.27]

A topos can allow the interpretation of a higher-order logic. In particular, objects can be seen as collections of elements of a given type, subobjects are viewed as propositions. Products and coproducts are interpreted as conjunction and disjunction respectively. For an introduction, see [pitts2001categorical].

definition. geometric morphism, Topoi [kostecki2011introduction, 7.2] [tt-004Q]

If \({\cal E}_1\) and \({\cal E}_2\) are toposes, then a geometric morphism \(\mathscr {G}: {\cal E}_1 \to {\cal E}_2\) is defined as a pair of adjoint functors \(\mathscr {G}^* \dashv \mathscr {G}_*\) between \({\cal E}_1\) and \({\cal E}_2\), such that \(\mathscr {G}^*\) preserves finite limits (i.e. is left exact), which implies \(\mathscr {G}_*\) preserves colimits (i.e. is right exact).

The category of toposes and their geometric morphisms is denoted \(\mathbf {Topoi}\).

Appendix [tt-0006]
✍️source

These are my notes on:

Category theory
Topos theory
Type theory
Sheaf theory
Differential sheaves
SDG (Synthetic Differential Geometry)

The primary references for these notes are:

[kostecki2011introduction]
[leinster2016basic]
[kostecki2009differential]
[rosiak2022sheaf]
[mallios2015differential]
[rosiak2022sheaf]
[zhang2021type]
[chen2016infinitely]
[sterling2023models]

[marsden2014category]

[fauser2004grade]

For draft notes, see drafts for Notes on Topos Theory and Type Theory.

reference. Notes on models of type theory [sterling2023models]

2023
Jon Sterling
https://www.jonmsterling.com/jms-00DJ.xml

@misc{sterling2023models,
 title = {Notes on models of type theory},
 author = {Sterling, Jon},
 year = {2023},
 url = {https://www.jonmsterling.com/jms-00DJ.xml}
}

reference. Sheaf theory through examples [rosiak2022sheaf]

2022
Daniel Rosiak

@book{rosiak2022sheaf,
 title = {Sheaf theory through examples},
 author = {Rosiak, Daniel},
 year = {2022},
 publisher = {MIT Press}
}

reference. Type theories in category theory [zhang2021type]

2021
Tesla Zhang

@article{zhang2021type,
 title = {Type theories in category theory},
 author = {Zhang, Tesla},
 year = {2021},
 journal = {arXiv preprint arXiv:2107.13242}
}

reference. An infinitely large napkin [chen2016infinitely]

2016
Evan Chen

@misc{chen2016infinitely,
 title = {An infinitely large napkin},
 author = {Chen, Evan},
 year = {2016},
 publisher = {Cambridge, Massachusetts: Massachusetts Institute of
Technology}
}

reference. Basic category theory [leinster2016basic]

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

reference. Differential sheaves and connections: A natural approach to physical geometry [mallios2015differential]

2015
Anastasios Mallios, Elias Zafiris

@book{mallios2015differential,
 title = {Differential sheaves and connections: a natural approach to physical geometry},
 author = {Mallios, Anastasios and Zafiris, Elias},
 year = {2015},
 volume = {18},
 publisher = {World Scientific}
}

reference. Category theory using string diagrams [marsden2014category]

2014
Daniel Marsden

@article{marsden2014category,
 title = {Category theory using string diagrams},
 author = {Marsden, Daniel},
 year = {2014},
 journal = {arXiv preprint arXiv:1401.7220}
}

reference. An introduction to topos theory [kostecki2011introduction]

2011
Ryszard Paweł Kostecki
https://www.fuw.edu.pl/~kostecki/ittt.pdf

@article{kostecki2011introduction,
 title = {An Introduction to Topos Theory},
 author = {Kostecki, Ryszard Pawe{\l}},
 year = {2011},
 url = {https://www.fuw.edu.pl/~kostecki/ittt.pdf},
 journal = {Technial Report}
}

reference. Differential geometry in toposes [kostecki2009differential]

2009
Ryszard Paweł Kostecki
https://www.fuw.edu.pl/~kostecki/sdg.pdf

@misc{kostecki2009differential,
 title = {Differential Geometry in Toposes},
 author = {Kostecki, Ryszard Pawe{\l}},
 year = {2009},
 url = {https://www.fuw.edu.pl/~kostecki/sdg.pdf},
 publisher = {Citeseer}
}

reference. Grade free product formulae from graßmann-hopf gebras [fauser2004grade]

@article{fauser2004grade,
 title = {Grade free product formulae from Gra{\ss}mann-Hopf gebras},
 author = {Fauser, Bertfried},
 year = {2004},
 url = {https://arxiv.org/abs/math-ph/0208018},
 journal = {Clifford Algebras: Applications to Mathematics, Physics, and Engineering},
 pages = {279--301},
 publisher = {Springer}
}

drafts for Notes on Topos Theory and Type Theory [tt-000L]

example. (co)limit in Set [leinster2016basic, 5.1.22, 5.2.16] [tt-004W]

In \(\mathbf {Set}\), the limit is constructed as a subset of a product, the colimit is a quotient of a sum.

Add this after definition [tt-002G].

definition. concrete category [riehl2017category, 1.6.17] [tt-0053]

A concrete category is a category \({\cal C}\) equipped with a faithful functor \(\mathscr {F} : {\cal C} \to \mathbf {Set}\).

Add this to where this would be used.

definition. cone [kostecki2011introduction, 4.9] [tt-0027]

Let \({\cal C}^{{\cal J}}\) be a functor category, where \({\cal J}\) is a small category.

Let \(\Delta _O\) be a constant functor, which assigns the same object \(O\) in \({\cal C}\) to any object \(J\) in \({\cal J}\).

Let \(K \in \operatorname {Ob}({\cal J})\) and let \(j \in \operatorname {Arr}({\cal J})\) such that \(j: J \to K\). Let \(\mathscr {F}\) be any functor in \({\cal C}^{{\cal J}}\), i.e. it's a diagram in \({\cal C}\) of shape \({\cal J}\).

A natural transformation \(\pi : \Delta _O \to \mathscr {F}\), defined as a family of arrows \(\pi _J: O \to \mathscr {F}(J)\), such that the diagram commutes, is called a cone on the functor (diagram) \(\mathscr {F}\) with vertex \(O\).

This is the alternative definition of definition [tt-0028], it should be incooporated with definition [tt-0040].

definition. creates limits [leinster2016basic, 5.3.5] [tt-0058]

A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) creates limits (of shape \({\cal J}\)) if whenever \(\mathscr {D}: {\cal J} \to {\cal C}\) is a diagram in \({\cal C}\),

for any limit cone \(\left ( V_{{\cal D}} \xrightarrow {q_J} \mathscr {F} \mathscr {D}(J) \right )_{J \in {\cal J}}\) on the diagram \(\mathscr {D} \mathbin {\bullet } \mathscr {F}\), there is a unique cone \(\left (V_{{\cal C}} \xrightarrow {p_J} \mathscr {D}(J) \right )_{J \in {\cal J}}\) on \(\mathscr {D}\) such that \(\mathscr {F}(V_{{\cal C}})=V_{{\cal D}}\) and \(\mathscr {F}\left (p_J\right )=q_J\) for all \(J \in {\cal J}\)
this cone \(\left (V_{{\cal C}} \xrightarrow {p_J} \mathscr {D}(J)\right )_{J \in {\cal J}}\) is a limit cone on \(\mathscr {D}\).

Simplify wording and put it in § [tt-0023] together with lemma [tt-0059].

example. direct limit [rosiak2022sheaf, example 68] [tt-004X]

Direct limits is the colimit of a diagram indexed by the ordinal category \(\omega \). In other words, for a diagram \[ X_1 \to X_2 \to X_3 \to X_4 \to \cdots \] its colimit is the direct limit \(\lim \limits _{\to } X_n\), defining a diagram of shape \(\omega +1\) :

Observe then that the colimit of a sequence of sets with the inclusions \[ X_0 \hookrightarrow X_1 \hookrightarrow X_2 \hookrightarrow \cdots \] recovers their union \(\bigcup \limits _{n \geq 0} X_n\).

Add this after definition [tt-002G].

corollary. evaluation functor preserves limits of ... [leinster2016basic, 6.2.6] [tt-0046]

An important corollary of theorem [tt-0045].

The Yoneda embedding preserves limits, for any small category [leinster2016basic, 6.2.12]. But it does not preserve colimits in general [leinster2016basic, 6.2.14].

Every presheaf can be expressed as a colimit of representables in a canonical (though not unique) way, this is theorem [tt-004D], and dual to lemma [tt-002N].

fill in details.

definition. filtered category [rosiak2022sheaf, def. 285] [tt-004Z]

A category \({\cal J}\) is filtered (or directed) if

it is not empty
for every pair of objects \(J, J^{\prime } \in {\cal J}\), there exists \(K \in {\cal J}\) and \(f: J \to K\) and \(f': J' \to K\)
for every two parallel arrows \(u, v: i \rightarrow j\) in \({\cal J}\), there exists \(K \in {\cal J}\) and \(w: J \to K\) such that \[u \mathbin {\bullet } w = v \mathbin {\bullet } w\]

This is a generalization of the notion of a (upward) directed poset from order theory.

Add this to where this would be used.

definition. filtered colimit [rosiak2022sheaf, def. 285] [tt-0050]

A filtered colimit is a colimit of a functor \(\mathscr {F}: {\cal J} \to {\cal C}\), where \({\cal J}\) is a filtered category.

In particular, a colimit over a filtered poset \(P\) is the same as the colimit over a cofinal subset \(Q\) of that poset, where \(Q\) as a cofinal subset means that for every element \(p \in P\), there exists an element \(q \in Q\) with \(p \leq q\).

theorem. general adjoint functor theorem [leinster2016basic, 6.3.10] [tt-004E]

Limit-preservation alone does not guarantee the existence of a left adjoint. This theorem specifies the conditions under which a limit-preserving functor has a left adjoint. This theorem requires the definition of weakly initial set.

fill in details.

theorem. limits in a functor category [leinster2016basic, 6.2.5] [tt-0045]

Limits in a functor category are computed pointwise.

fill in details.

This theorem helps proving lemma [tt-0047].

remark. local, global [rosiak2022sheaf, p. 1] [tt-005C]

In a very general and rough way, by local we typically understand that something is being compared to what is around or nearby it; this is as opposed to the global, generally understood to mean compared to everything or across an entire domain of interest. Satisfying a property at a local level does not necessarily entail that the same will obtain at the global level.

lemma. preserves if creates [leinster2016basic, 5.3.6] [tt-0059]

Let \(\mathscr {F}: {\cal C} \rightarrow {\cal D}\) be a functor and \({\cal J}\) a small category. Suppose that \({\cal D}\) has, and \(\mathscr {F}\) creates, limits of shape \({\cal J}\). Then \({\cal C}\) has, and \(\mathscr {F}\) preserves, limits of shape \({\cal J}\).

Same as definition [tt-0058].

lemma. representable functor and adjoint [tt-0022]

Lemma 4.24.2 in The Stacks project.

definition. section, choice [leinster2016basic, sec. 3.1] [tt-003E]

Let \(f: X \to Y\) be an arrow in a category \({\cal C}\). A section (or right inverse) of \(f\) is an arrow \(i: Y \to X\) in \({\cal C}\) such that \(i \mathbin {\bullet } f = \mathit {1}_X\).

In \(\mathbf {Set}\), any arrow with a section is certainly surjective. The converse statement is called the axiom of choice:

Every surjection has a section.

It is called choice because specifying a section of \(f: X \to Y\) amounts to choosing, for each \(y \in Y\), an element of the nonempty set \(\{x \in X \mid f(x)=y\}\).

It's closely related to § [tt-004T], need to figure out how to incooperate.

definition. sequence [leinster2016basic, sec. 3.1] [tt-003D]

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

Related to § [tt-004T].

shaef theory [tt-005B]

definition. slice category [kostecki2011introduction, eq. 12] [tt-0009]

The slice category \({\cal C} \downarrow X\), is the category whose objects are arrows in \({\cal C}\) with fixed codomain \(X\), such that the diagram

commutes, where colored arrows are in \({\cal C} \downarrow X\).

It's also denoted \({\cal C} / X\) or \({\cal C}_{/X}\).

The slice category is a special case of the comma category.

It's also called overcategory, as it's a slice category over \(X\) [zhang2021type, 3.5].

revamp and add co-slice category, maybe following [rosiak2022sheaf, def. 21], or better, follow Basic category theory, to explain how a slice category is a special case of comma category.

definition. sum, coproduct [leinster2016basic, 5.2.2] [tt-003L]

A sum or coproduct is a colimit over a discrete category, i.e. it is a colimit of shape \(J\) for some discrete category \({\cal J}\).

Possibly belong to § [tt-0023].

remark. summary [tt-0055]

This diagram summarizes § [tt-002P].

Add this to § [tt-002P].