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].

Lemma. Representable functor and adjoint [tt-0022]

Lemma 4.24.2 in The Stacks project.

Shaef theory [tt-005B]

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

See also .

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}\).

Definition [tt-002F]Definition [tt-0058]Same as Definition [tt-0058].

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].

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].