Original exposition, written and self-checked with GPT-6.1 Sol (OpenAI), Ultra reasoning effort, with complete retained arguments and linked free primary proofs. A separate scoped model check covers the specified arguments, their complete prerequisite interfaces and four exercise solutions. It adds no whole-lesson or whole-course review. Model source and locus reading; no Lean build or human endorsement. Original exposition uses CC0 1.0; linked complete proofs retain their stated terms.

Comma functors, iterated cocones and arrow categories

A stage chosen in one diagram may have to be compared with a stage chosen in another. Keeping only the two stages loses the comparison arrow. A comma category keeps all three pieces. Its projections then answer two different questions: whether these linked stages can replace the original index, and whether assembly over the linked stages can be performed one fibre at a time.

The same construction organizes commuting squares. An arrow between two source objects, together with a square to a fixed target arrow, is a comma object between two ordinary outgoing comma categories. This observation lets us transfer filteredness, cofinality and size bounds to arrow categories.

1. Retain the arrow between the two stages

Fix ambient set-categories and functors

Composition is written from right to left. The category

has objects \((i,j,u)\), where \(u:\phi(i)\to\psi(j)\). An arrow

consists of \(v:i\to i'\) and \(w:j\to j'\), subject to

The arrows are the actual pairs in \(I,J\), even when their images in \(K\) coincide.

Identities are \((1_i,1_j)\); successive pairs compose componentwise. The equation survives composition because

The units and associativity are those in \(I,J\). These laws give three functors

Equation (1.3) also says that the arrows \(u\) form a natural transformation \(\phi p_I\Rightarrow\psi p_J\).

The complete existing construction is A category whose objects carry an arrow, together with the general two-functor interface in A map between two different functor images. The later ind-object result in that second section has different hypotheses; we use its general comma definition here.

Let \(\mathrm{Pt}\) be the one-object category with only its identity. A functor \(\mathrm{Pt}\to K\) chooses an object \(a\). Then

The first has arrows \(v\) satisfying \(u'\phi(v)=u\); the second has arrows \(w\) satisfying \(\psi(w)u=u'\). The inverse assignments insert the unique object and identity of \(\mathrm{Pt}\). When the middle category itself is \(\mathrm{Pt}\), the comma is \(I\times J\): insert the unique connecting arrow and retain each arrow pair.

We use the native size convention: a category is locally \(\mathcal U\)-small unless a larger universe is stated. Each Hom set of \(M\) is a subset of

Thus \(M\) is locally small. Smallness of its whole object set is a separate question: its objects include choices from the sets \(K(\phi(i),\psi(j))\). The complete bounds used below are Building sets inside a universe, Transporting the size bound, and Two distinct size conditions on a category.

For a simple picture, take ordered sets as categories. If \(\phi,\psi\) are increasing maps, an object of \(M\) is a pair \((i,j)\) for which \(\phi(i)\leq\psi(j)\). Its arrows increase both coordinates. The condition on an object still matters, even though every admissible square commutes automatically.

2. Specify the comparisons before changing the comma

Consider two rows \(I_\nu\xrightarrow{\phi_\nu}K_\nu\xleftarrow{\psi_\nu}J_\nu\), and functors

The comparison data are specified natural isomorphisms

They determine a functor \(\theta:M_1\to M_2\):

The connecting arrow starts at \(\phi_2(Fi)\) and ends at \(\psi_2(Gj)\). In particular, the inverse on \(B_j\) cannot be omitted.

The component equations for naturality are

For a source arrow satisfying (1.3), they give

This is the target comma equation. The identity and composition laws follow from those of \(F,G\).

Theorem 2.1. With the specified invertible comparisons (2.1):

1. If \(F,G\) are faithful, then \(\theta\) is faithful.
2. If \(F,G\) are fully faithful and \(H\) is faithful, then \(\theta\) is fully faithful.
3. If \(F,G\) are equivalences and \(H\) is fully faithful, then \(\theta\) is an equivalence.

The complete primary proofs are retained at the pinned Mathlib commit in Comma/Basic, lines 233–298. Its left comparison is \(A\), its right comparison is \(B^{-1}\), its two endpoint functors are \(F,G\), and its middle functor is \(H\). Its faithful-map proof uses only faithfulness of the endpoints. Its full-map proof requires full endpoints, faithful middle and invertible comparisons; adding faithful endpoints gives part 2. Its essential-image proof uses essentially surjective endpoints and full middle; together with part 2 and Recognizing a reversible change of category, it gives part 3. This checks the complete hypotheses without adding essential surjectivity of \(H\).

There is also an exact composition rule for these comparison data. For successive changes \(1\to2\to3\), write the comparisons as \(A_{12},B_{12}\) and \(A_{23},B_{23}\). The composite comparisons have components

Their domains and codomains are those for \(F_{23}F_{12},G_{23}G_{12},H_{23}H_{12}\). Substitution in (2.2) gives the composite induced comma functor, with the usual functor-associativity identifications. The complete whiskering and interchange laws are Compose comparisons along successive functors.

This rule concerns compatible, specified data. It does not imply independence from arbitrary choices of \(A,B\). For example, with all endpoint categories equal to \(\mathrm{Pt}\) and the middle category a one-object group, the comma is discrete on the group elements. Changing a comparison can permute those elements; distinct such permutations need not be naturally isomorphic. Exercise 2 calculates this effect.

We will use natural-isomorphism invariance of cofinality in its actual comma form. If \(\rho:P\Rightarrow Q\) is invertible, then

is an isomorphism, with inverse using \(\rho^{-1}\) and the same underlying source arrows. Naturality verifies its triangles. On outgoing commas the corresponding arrow is \(s\rho_x^{-1}\). Thus the direction of the comparison is fixed before transporting a cofinality assertion.

3. Assemble a cocone one fibre at a time

Return to (1.1), and let \(\alpha:M\to C\). For \(j\in J\), put

An arrow \(v\) in \(E_j\) acts by \(\alpha(v,1_j)\).

Proposition 3.1. Suppose every inner actual colimit

exists in \(C\), with chosen coprojections \(\lambda^j_{i,u}\). These objects have a canonical \(J\)-diagram structure. Its colimit exists if and only if the actual colimit of \(\alpha\) exists. When they exist, the comparison

is characterized by every original leg:

Here \(b\) and \(\ell\) are the respective colimit coprojections.

We now bind the pointwise universal maps and total assembly from Build the left extension and Total assembly and total compatibility to these fibres. Only the displayed actual inner colimits are assumed; no general cocompleteness assumption is added to \(C\).

For \(w:j\to j'\), postcomposition sends \((i,u)\) to \((i,\psi(w)u)\). There is an actual \(M\)-arrow

Define \(L(w)\) by

For a fibre arrow \(v\), the two ways through its square with \((1,w)\) are the same \(M\)-arrow. Applying \(\alpha\) and the \(j'\)-cocone equation proves that the right side of (3.4) is a cocone on \(\alpha_j\). Hence the universal factor exists and is unique. Testing every \(\lambda\) gives \(L(1)=1\) and \(L(w'w)=L(w')L(w)\).

An \(M\)-cocone \(a_{i,j,u}:\alpha(i,j,u)\to T\) uniquely factors on each fibre:

Its equations on the arrows \((1_i,w)\), together with (3.4), give \(a_{j'}L(w)=a_j\). Conversely a \(J\)-cocone \(a_j:L_j\to T\) gives the family \(a_j\lambda^j_{i,u}\). An arbitrary \(M\)-arrow \((v,w)\) factors as

The outer equation handles the first arrow; the fibre equation handles the second. Thus the family is an \(M\)-cocone. The constructions (3.5) and this last family are inverse, and postcomposition with \(T\to T'\) commutes with them.

This natural bijection of cocone families proves both directions of actual existence in Proposition 3.1. If the total colimit is given, factor its \(b\)-legs on each fibre to obtain \(d_j:L_j\to\operatorname{colim}_M\alpha\). They form an outer cocone, and its universal property follows from the same bijection. If the outer colimit is given, its legs \(\ell_j\lambda^j_{i,u}\) supply the total colimit.

When both are chosen, \(d\), the inverse of (3.2), has

Equations (3.3) and (3.7) give \(dc=1\) on every \(b\)-leg. They give \(cd=1\) first on every \(\ell_j\lambda^j\), then on every \(\ell_j\), and finally on the outer colimit. This identifies the actual comparison, rather than only an isomorphism class.

For a transformation \(z: \alpha\Rightarrow\alpha'\), the inner transformation is defined by

Naturality of \(z\) on \((1_i,w)\) verifies naturality in \(j\). Identity and composition laws again hold on every leg. If the total and outer colimits exist, their induced maps satisfy

because both sides have the same value on each \(b_{i,j,u}\). This supplies naturality in the original diagram.

There is a formal version when the inner objects are not represented in \(C\). Write

For each \(j\), let \(Q_j(T)\) be the set of cocones from \(\alpha_j\) to \(T\). The map \(w:j\to j'\) gives \(Q_{j'}(T)\to Q_j(T)\) by precomposition with the arrows \(\alpha(1_i,w)\). Thus these value functors form a \(J^{\mathrm{op}}\)-diagram in \(\operatorname{Fun}(C,\mathsf{Set})\), or a \(J\)-diagram in \(C^\vee\). The same inverse cocone constructions give

naturally in \(T,\alpha\). In \(C^\vee\), this is the formal iterated-colimit formula.

The formal inner leg at \((i,u)\) reverses evaluation \(Q_j(T)\to C(\alpha(i,j,u),T)\). The formal outer leg reverses restriction \(\operatorname{Cocone}_M(\alpha,T)\to Q_j(T)\). Their composite reverses the evaluation \(a\mapsto a_{i,j,u}\), which is the original formal \(M\)-coprojection. Thus (3.10) retains the same leg identity as (3.3). A transformation \(z: \alpha\Rightarrow\alpha'\) sends a cocone \(a'\) to \(a'z\), giving \(Q_{\alpha'}\Rightarrow Q_\alpha\); reversing this arrow gives the formal colimit map in the usual direction. Restriction and evaluation commute with this operation, proving the two naturality squares for the formal comparison.

The complete formal interface is Universal functors before universal objects, with Size changes and opposite categories. The value functors in (3.10) are covariant in \(T\); the opposite on \(C^\vee\) reverses arrows. Small indices in the chosen universe, or an adequate enlargement, bound the products defining those values. A large index has no automatic \(\mathcal U\)-small cocone set, and transformation sets on a large base may need a further enlargement. A formal colimit need not be represented by an actual \(C\)-object.

In particular, an existing total actual colimit does not supply missing inner actual colimits. Exercise 3 gives a finite example. For empty \(J\), also \(M\) is empty: the actual assertion asks for an initial object of \(C\), while the formal cocone-value functor is the constant singleton.

4. Two different commas around a projection

Fix \(j_0\in J\). Put

A \(Q\)-object is \((i,j,u,s:j\to j_0)\). An arrow \((v,w)\) satisfies both the \(M\)-square and \(s'w=s\). The fibre inclusion is

Define

Indeed, the two source equations give \(\psi(s')u'\phi(v)=\psi(s'w)u=\psi(s)u\), the required target equation.

The full primary adjunction is Costructured-arrow projection and inclusion, lines 1292–1318. Its specialization has

For \(q=(i,j,u,s)\) and \(e=(a,t)\), the natural Hom bijection sends \(v:i\to a\) satisfying \(t\phi(v)=\psi(s)u\) to the \(Q\)-arrow \((v,s):q\to\xi(e)\). The inverse forgets the forced second component \(s\). The unit at \(q\) is \((1_i,s)\); the counit is identity because \(\eta\xi=1_E\). Applying \(\eta\) to the unit gives identity, and the unit at \(\xi(e)\) is identity, verifying both triangles. The arrow equations verify naturality.

Consequently \(\xi\), the right adjoint, is cofinal. We use the full right-adjoint cofinality proof. Calling \(\eta\) a left adjoint does not give this cofinality conclusion for \(\eta\).

Recall that a functor \(P:A\to B\) is cofinal when every incoming comma \((b\downarrow P)\) is nonempty and connected. The complete cocone extension, canonical comparison and conditional existence theorem are Connected comma categories and Extend every cocone.

Proposition 4.1. If \(\psi:J\to K\) is cofinal, then \(p_I:M\to I\) is cofinal. If \(I\) is connected as well, then \(M\) is connected.

These are the full primary first-projection and connected-comma results, lines 99–131. Here is their concrete incoming-comma interface. For \(i_0\in I\), objects of

are \((i,j,u,r:i_0\to i)\). The category \(E_0=(\phi(i_0)\downarrow\psi)\) is nonempty connected. The functors

send an arrow respectively to \((1_{i_0},w)\) and \(w\). The incoming triangle \(vr=r'\), together with the \(M\)-square, verifies the second functor. We have \(ts=1\), and \((r,1_j)\) gives a natural arrow \(st(q)\to q\). Hence every \(R\)-object is connected to the image of the nonempty connected \(E_0\). This proves the required incoming connectedness. It does not assert that \(s\) is cofinal.

The full canonical component bijection for a cofinal functor, proved in Compose and cancel index changes, now gives \(\pi_0(M)\cong\pi_0(I)\). Connected includes nonempty, so connected \(I\) gives connected \(M\).

No filteredness hypothesis was used in Proposition 4.1. For empty \(I\), \(M\) is empty and \(p_I:\varnothing\to\varnothing\) is cofinal vacuously. This does not make \(M\) connected. The comma \(Q\) in (4.1) is outgoing; \(R\) in (4.4) is incoming, and their arrow directions are different.

5. Check an induced comma functor by two cofinal maps

Keep the specified data (2.1).

Theorem 5.1. Suppose \(J_1\) is filtered, and \(\psi_1,\psi_2,F,G\) are cofinal. Then \(\theta:M_1\to M_2\) is cofinal. In particular this applies when both \(J_1,J_2\) are assumed filtered.

The complete primary theorem and proof are Comma.map_final, lines 153–174. We identify its entire incoming comma and both induced cofinal maps, using the complete current Four functors between incoming commas.

First the hypotheses make \(J_2,K_1,K_2\) filtered: apply the full local cofinal-arrow theorem to \(G,\psi_1,\psi_2\). Also

Composition, the transport (2.6), and cancellation of cofinal functors show that \(H\) is cofinal. Neither fullness nor faithfulness of \(H,F,G\) is needed here.

Fix \(a=(i_2,j_2,u_2)\in M_2\), and set

There are functors \(P:D\to T\) and \(Q:E\to T\):

An object of \((a\downarrow\theta)\) consists of \((i,j,u)\in M_1\) and \(x:i_2\to Fi,\ y:j_2\to Gj\), with

Equivalently,

This says exactly that \(u\) is a \(T\)-arrow \(P(i,x)\to Q(j,y)\). On arrows, both descriptions retain \((v,w)\) and all three equations

The assignments are inverse on objects and Hom sets, with unchanged identities and compositions. Thus

is an isomorphism of whole categories. The full primary inverse functors and comparison isomorphisms are StructuredArrow/CommaMap, lines 36–87.

To see the exact cofinal factors of \(Q\), first use the chain

and \(u_2:\phi_2(i_2)\to\psi_2(j_2)\). Part 4 of the retained incoming-comma theorem gives

Transport by \(B\) sends this object to \((j,B_j\psi_2(y)u_2)\) in \((\phi_2(i_2)\downarrow H\psi_1)\). Second, part 3 for

gives

Both chains have filtered categories and cofinal functors, as checked above. Both functors are therefore cofinal, and their literal composite, including the specified \(B\)-transport, is \(Q\).

Since \(F\) is cofinal, \(D\) is nonempty connected. Proposition 4.1 applied to \(P: D\to T\leftarrow Q: E\) makes \((P\downarrow Q)\) connected. By (5.5), every incoming comma of \(\theta\) is connected, proving Theorem 5.1 with the exact maps of the retained primary proof.

The incoming-comma provider's part 2 uses the chain \(I\xrightarrow{1_I}I\xrightarrow{\phi}J\), with \(u=1_{\phi(i)}\). That corrected specialization is the current provider; no full-embedding hypothesis is inserted into any of these four comma functors.

6. Filtered linked stages and all three projections

Theorem 6.1. Suppose \(I,J\) are filtered and \(\psi:J\to K\) is cofinal, while \(\phi:I\to K\) is arbitrary. Then \(M\) is filtered, and each of

is cofinal. If \(I,J\) are cofinally \(\mathcal U\)-small, then \(M\) is cofinally \(\mathcal U\)-small.

Filtered means nonempty, admits common receivers for two objects, and post-equalizes every parallel pair. The complete finite-graph criterion and empty-diagram case are Bring a finite diagram to one object.

For every \(i\), cofinal \(\psi\) with filtered source makes \((\phi(i)\downarrow\psi)\) filtered by the retained local-arrow theorem. The full primary relative comma proof Comma/Final, lines 46–118, specialized with \(A=I,B=J,L=\phi,R=\psi\), supplies all three filtered axioms of \(M\). Its filtered form uses the explicit opposite equivalence

which swaps endpoints and sends each arrow pair to its reversed opposite pair; the full inverse functors and projection comparisons are Comma/Basic, lines 509–547. This is the direct proof retained here; it requires no finite colimits in \(I,J,K\). Its final specialization is isFiltered_of_final, lines 180–182.

The outgoing comma of this first projection also has a complete concrete description. For \(i\in I\), let \(q:(1_I\downarrow i)\to I\) forget the arrow to \(i\). Then

The object \(((a,j,u),v:a\to i)\) maps to \(((a,v),j,u)\). An arrow \((h,w)\) has exactly the two equations \(v'h=v\) and \(\psi(w)u=u'\phi(h)\) on both sides. The inverse retains these same objects and arrow pairs, so the identification respects identities and every composite.

The object \((i,1_i)\) is terminal in \((1_I\downarrow i)\); its one-object inclusion is cofinal because each incoming comma has the unique arrow to that terminal object. Apply Theorem 5.1 with this inclusion, \(1_J\), \(1_K\) and identity comparisons. It gives a cofinal functor

Its source is filtered by the retained local-arrow theorem for the cofinal functor \(\psi\) with filtered source \(J\). A cofinal image of a filtered category is filtered, by that same complete theorem. Hence every outgoing \((p_I\downarrow i)\) is filtered: \(p_I\) is right exact in the outgoing convention. This proof binds the terminal-stage specialization on whole arrows without requiring finite colimits in \(I,J,K\).

Proposition 4.1 gives cofinal \(p_I\). The full second-projection proof is the relative result at lines 110–118 of the same primary source, applied to these filtered incoming commas; final_snd, lines 193–195 makes the specialization explicit. Its incoming comma at \(j_0\) has objects \((i,j,u,s:j_0\to j)\), and arrows \((v,w)\) satisfying (1.3) and \(ws=s'\). Thus this theorem concerns the actual \(p_J\); it is different from the outgoing comma and right-adjoint fibre inclusion in Section 4.

The paired projection needs its own argument. Apply Theorem 5.1 to the source row \(I\to K\leftarrow J\) and target row

with endpoint functors \(1_I,1_J\) and middle functor \(K\to\mathrm{Pt}\). The target right functor \(J\to\mathrm{Pt}\) is cofinal: its sole incoming comma is \(J\), which is nonempty connected because it is filtered. Both comparisons are the unique ones. The target comma is \(I\times J\), by (1.6), and the induced map sends \((i,j,u)\) to \((i,j)\), \((v,w)\) to \((v,w)\). It is exactly \(p\). Theorem 5.1 therefore proves the third assertion; separate cofinality of the two component projections was not used as a substitute for this proof.

For the size assertion, Replace a large index by a small full one produces \(\mathcal U\)-small full cofinal subcategories \(I'\subseteq I,\ J'\subseteq J\). Each inclusion receives an arrow from every object of its ambient category. The full receiving-subcategory criterion makes \(I',J'\) filtered. It uses fullness to lift receiving maps and faithfulness to reflect their equalities; both hold for the full inclusions.

Set

The restricted \(\psi|_{J'}\) is cofinal by composition. Theorem 5.1, with the two inclusions, middle identity and identity comparisons, makes \(M'\to M\) cofinal. To check that \(M'\) itself is small, its objects are the tagged union

The index is small, and every summand is small by the default local \(\mathcal U\)-smallness of \(K\). Each Hom set is a subset of \(I'(i,i')\times J'(j,j')\); the set of all arrows is the small tagged union of these Hom sets over the square of the small object set. The retained universe proofs transport these bounds when the original labels are small only up to bijection. Smallness of the entire object set of \(K\) is unnecessary. Removing its local Hom bound would remove the bound on (6.5).

The nonemptiness assumptions are essential: for empty \(I\) and nonempty \(J\), \(p_J\) need not be cofinal. Theorem 6.1 excludes that case by filteredness.

7. A square to one arrow is a comma object

For a category \(C\), let \(\operatorname{Mor}(C)\) have arrows \(t:X\to X'\) as objects. An arrow from \(t\) to \(t':Z\to Z'\) is a square \((s,s')\) with

Its identity and composition are componentwise, as in Section 1. A functor \(F:C\to D\) gives

Functoriality of \(F\) carries (7.1) to the target square and preserves the category laws.

Here right exact means that every outgoing comma \((F\downarrow Y)\) is filtered. Right small means that every such outgoing comma is cofinally \(\mathcal U\)-small. These are comma conditions; we do not assume that \(C\) has finite colimits.

Corollary 7.1. Let \(F:C\to D\) be right exact. Then \(\operatorname{Mor}(F)\) is right exact. For each target arrow \(f:Y\to Y'\), the two endpoint projections and their pair

are cofinal. If both endpoint commas are cofinally \(\mathcal U\)-small, so is the source comma in (7.3). Consequently, if this right exact \(F\) is also right small, then \(\operatorname{Mor}(F)\) is right small.

To bind every map in this application, put \(C_Y=(F\downarrow Y)\) and \(C_{Y'}=(F\downarrow Y')\). There is a functor

Its arrow equation is \(a_{\rm new}F(s)=a\); postcomposition with \(f\) preserves it.

An object of \((f_*\downarrow1_{C_{Y'}})\) is

This is exactly the outgoing \(\operatorname{Mor}(F)\)-comma object given by \(t\) and the square \((a,b):F(t)\to f\). An arrow to \((t_{\rm new},a_{\rm new},b_{\rm new})\) has

These are both the two-functor comma equations and the outgoing arrow-category triangle. The inverse assignments retain \(t,a,b\) and the actual pair \((s,s')\), hence identities and all composites. We obtain the exact category isomorphism

Right exactness makes \(C_Y,C_{Y'}\) filtered; their identity functor is cofinal. Theorem 6.1 applied to (7.7) makes this comma filtered and gives all three projections in (7.3). On objects they are \((X,a)\), \((X',b)\), and their ordered pair; on arrows they are \(s,s'\), and \((s,s')\). The target categories are the structured outgoing commas, rather than only \(C,C\times C\).

The same theorem proves cofinal smallness. Local Hom sets of \(C_{Y'}\) are subsets of Hom sets of \(C\), so the needed local bound is present. If \(F\) is right small, the two endpoint hypotheses hold for every \(f\); quantifying over these arrows proves the final assertion. Its right exactness hypothesis remains in force.

Only the endpoint commas must be filtered; \(C\) itself need not be filtered. If \(D\) is empty, a functor to it forces \(C\) empty, and these assertions are vacuous for the empty arrow categories.

8. Four graded exercises with full solutions

Exercise 1 — introductory: five linked stages

Let \(I=\{0<1\}\), \(J=K=\{0<1<2\}\), with \(\phi\) the inclusion and \(\psi=1_J\). List the objects and arrows of \(M\). For an arbitrary \(\alpha:M\to C\), compute all three inner colimits, the outer transition arrows, and the total colimit. Identify comparison (3.3).

Solution. The objects are

There is an arrow \((i,j)\to(i',j')\) exactly when \(i\leq i'\) and \(j\leq j'\). The connecting arrow in \(K\) is unique, so (1.3) imposes no further condition on such a pair. The final object is \((1,2)\).

The fibres at \(0,1,2\) have final objects \((0,0),(1,1),(1,2)\), respectively. Therefore choose

Their coprojections are the images of the unique arrows to those final objects. Formula (3.4) gives

The \(0\leq2\) map is their composite by functoriality of \(\alpha\). The outer and total colimits are both \(\alpha(1,2)\), with legs the images of the arrows to \((1,2)\). On every original object the composite \(\ell_j\lambda^j_{i,u}\) is that same image arrow. Thus (3.3) is the identity for these chosen objects. No completeness assumption on \(C\) was required: a diagram with a final indexing object has that actual colimit by its cocone universal property.

Exercise 2 — intermediate: a comparison can move an object

Let every endpoint category be \(\mathrm{Pt}\). Let both middle categories be the one-object category of a \(\mathcal U\)-small group \(\Gamma\), and take \(H=1_\Gamma\). A specified comparison (2.1) is a pair of group elements \(a,b\). Describe its induced comma functor, and compute the composite for two choices \((a_1,b_1)\), \((a_2,b_2)\). For \(\Gamma=\{1,g\}\) with \(g^2=1\), compare the choices \((1,1)\), \((g,1)\).

Solution. The comma objects are \(u\in\Gamma\). Its only endpoint arrow pair is the identity pair, and its equation is \(u=u'\), so the comma category is discrete. Formula (2.2) sends

This is a bijection, with inverse \(v\mapsto bva^{-1}\), and hence an equivalence of the discrete categories. The composite sends

which agrees with the specified composite comparisons (2.5).

In the two-element group, \((1,1)\) induces the identity and \((g,1)\) interchanges the two objects. A natural transformation between those functors would need, at \(1\), an arrow \(1\to g\) in a discrete category. There is no such arrow. Thus these two choices do not give naturally isomorphic induced functors, although each is an equivalence. The correct composition rule preserves the specified comparisons; it gives no arbitrary-choice independence.

Exercise 3 — advanced: total assembly can exist before a fibre object

Let \(I\) be the three-object ordered category with \(a<t,\ b<t\), while \(a,b\) are incomparable. Let \(J=K=\{0<1\}\), take \(\psi=1_J\), and set \(\phi(a)=\phi(b)=0,\ \phi(t)=1\).

Let \(C\) be the four-object ordered category with objects \(A,B,T,S\), relations \(A<T,\ B<T,\ A<S,\ B<S\), and no other nonidentity relations. Define \(\alpha:M\to C\) by sending both occurrences of \(a\) to \(A\), both occurrences of \(b\) to \(B\), and the occurrence of \(t\) to \(T\). Show that the total actual colimit exists but the inner actual colimit at \(0\) does not. Calculate the formal comparison between the two fibre values.

Solution. The comma objects are

Their arrows increase the \(I\)- and \(J\)-coordinates. In particular, \((t,1)\) is final. The stated assignment is a functor: its only nonidentity values are identities on \(A,B\) or the arrows \(A\to T,B\to T\). Thus its actual total colimit is \(T\), with precisely those terminal-stage legs.

The fibre at \(0\) is the discrete diagram \(A,B\). Its actual colimit would be their least upper bound in \(C\). Both \(T,S\) are upper bounds, and they are incomparable; neither \(A\) nor \(B\) is an upper bound. Hence no least upper bound exists. This does not contradict Proposition 3.1, whose actual assertion assumes every inner colimit.

The fibre at \(1\) has final object \(t\), so its actual colimit is \(T\). Formally, the two covariant value functors are

The outer transition in \(C^\vee\) is the reversal of

At \(X=S\), this is the unique map from the empty set to a singleton; at \(X=T\), it is the unique map between singletons; at \(A,B\), both sets are empty. These components are natural by associativity. Since \(1\) is final in \(J\), the formal outer colimit is \(k_C(T)\). The total is represented while the first fibre is not. This calculates the formal arrow with its correct reversed variance.

Exercise 4 — expert: all three arrow projections and their actual comparison

Let \(S\) be a \(\mathcal U\)-small set and \(C\) its finite-subset ordered category. Let \(F:C\to\mathrm{Pt}\) be the unique functor. Identify \((\operatorname{Mor}(F)\downarrow1_*)\). Prove filteredness, cofinality of its three projections, and right smallness directly in this example.

For \(\beta:C\times C\to\mathsf{Set}\), \(\beta(A,B)=A\times B\), identify the canonical cofinal-colimit comparison along the paired projection and its inverse.

Solution. Finite subsets form a nonempty filtered poset: \(\varnothing\) is an object, unions give common receivers, and parallel arrows are equal. The outgoing comma \((F\downarrow *)\) is exactly \(C\), so \(F\) is right exact. An object of the arrow comma is an inclusion \(X\subseteq Y\); its square to \(1_*\) is unique. An arrow to \(X'\subseteq Y'\) exists exactly when \(X\subseteq X'\) and \(Y\subseteq Y'\). Thus this comma is \(\operatorname{Mor}(C)\), also filtered: a common receiver of two inclusions is

It contains \(\varnothing\subseteq\varnothing\), and has no unequal parallel arrows.

For the first projection, its incoming comma at \(A\) has an initial object \(A\subseteq A\). For the second projection, its incoming comma at \(B\) has an initial object \(\varnothing\subseteq B\). For the paired projection, an incoming object at \((A,B)\) is \(X\subseteq Y\) with \(A\subseteq X,\ B\subseteq Y\). Its initial object is

The unique arrows from these displayed objects obey all incoming triangles. Each incoming comma is therefore nonempty connected, so all three projections are cofinal, with exactly the structured endpoints of (7.3). The set of finite subsets of \(S\) is \(\mathcal U\)-small, as are its relation and the object/arrow sets of \(\operatorname{Mor}(C)\). Thus the relevant commas are small, hence cofinally small; both \(F\) and \(\operatorname{Mor}(F)\) are right small.

The two colimits in the final question are \(S\times S\). For the product index, the class of \((s,t)\in A\times B\) maps to \((s,t)\). For the arrow index, the class of \((s,t)\in X\times Y\), \(X\subseteq Y\), has the same image. Surjectivity of the second map follows by taking \(X=\{s\}\), \(Y=\{s,t\}\). If two representatives have the same pair, the common receiver given by unions identifies them; the same argument applies to the product index.

The canonical cofinal comparison sends

Its inverse sends a target class with pair \((s,t)\) to

The union receiver proves independence from every chosen representative and both inverse identities. This comparison agrees with each original coprojection. More generally, for a transformation \(\beta\Rightarrow\beta'\), the two comparison routes agree on every pair-stage leg; the complete cofinal universal-property theorem then gives naturality. If \(S\) is empty, all value sets are empty, the index still contains its empty stage, and the same maps are the unique inverse maps of empty sets.

9. Retained primary proofs and licence

The primary Mathlib references above are pinned to commit 389347a7c1cfa76f6bd5be2ca35d4cb621610ad3. They contain the complete proofs of the faithful/full/equivalence, cofinality, filteredness and adjunction assertions used here. Mathlib is distributed under its Apache-2.0 licence. The links identify the exact proof interfaces specialized in this lesson.

The prerequisite proofs linked in the lesson supply universal factors, naturality, incoming-comma cofinality, composition and cancellation, filtered finite witnesses, and the exact universe bounds. Actual colimit statements retain their existence hypotheses, and all three projection statements retain their stated filteredness hypotheses.