Draft lesson.

Bounded colimits, accessible sets and cardinal ind-objects

Written by GPT-6.1 Sol (OpenAI), October 2026. Original exposition: CC0. Reused proof interfaces retain their stated terms.

A map out of a colimit is a compatible family of maps out of its pieces. This turns a question about preservation by a Hom functor into a question about exchanging two Set constructions. We identify the resulting comparison on every coprojection, use it to receive diagrams of maps into a fixed object, and then distinguish accessible sets from cardinal restrictions on ordinary ind-objects.

1. Size conventions and the actual preservation map

Fix ambient Choice and a Grothendieck universe \(\mathcal U\). Small means bijective to a member of \(\mathcal U\). Let \(\pi\) be an infinite cardinal represented in \(\mathcal U\). Until Section 4 explicitly adds regularity, \(\pi\) is arbitrary. Categories have ambient sets of data; \(C\) is locally small, and its object set need not be small. The complete universe transport and category encoding retains all original labels and arrows. An enlargement permits ambient calculations, while working-universe smallness continues to govern the indices and values below.

We use two companion lessons: cardinal foundations and common arrows and bounded Set comparisons. The latter proves the criterion and exchange theorem for every infinite \(\pi\). Its criterion says that an index is \(\pi\)-filtered precisely when every diagram with fewer than \(\pi\) total morphisms has a cocone. Equivalently, bounded object families have receivers and bounded parallel-arrow families have one equalizing postarrow. Empty object families require nonemptiness. At \(\aleph_0\) this is ordinary filteredness.

The cardinal companion proves the infinite square and finite-union bounds; regularity is unnecessary for those bounds. Identities inject the objects of a category into its total morphism set. Thus a total-arrow bound below \(\pi\) also bounds the objects and makes the whole category small up to its complete encoding. It counts identities and composites, rather than only a chosen generating graph.

For Sections 1–3 suppose \(C\) admits all small \(\pi\)-filtered colimits. For a small \(\pi\)-filtered diagram \(D:I\to C\), choose its colimit \(L\), with coprojections \(a_i:D(i)\to L\). The complete Hom bifunctor supplies both variances and the natural encodings of its values. The filtered quotient construction supplies classes and their equality test. Define

The transition along \(s:i\to i'\) sends \(f\) to \(D(s)f\). Since \(a_{i'}D(s)=a_i\), the formula respects every generating identification and descends by the retained quotient factor property. It uses arrows of \(C\), not underlying elements of its objects. Encoded Hom values give the same function by decoding, composing, and encoding.

Here \(\pi\)-accessible means that (1.1) is bijective for every such \(I,D\). Write \(C_\pi\) for the full subcategory on these objects: its arrows, identities and compositions are exactly the corresponding ones in \(C\). This is the definition used throughout this lesson.

For \(u:X'\to X\), the source map is \([i,f]\mapsto[i,fu]\), and the target map is \(g\mapsto gu\). Both routes give \(a_i f u\). For a natural transformation \(\eta:D\to D'\), let \(\ell:L\to L'\) be the unique map with \(\ell a_i=a_i'\eta_i\), from the complete cocone factor and induced-map proof. The source map is \([i,f]\mapsto[i,\eta_i f]\), and

These equations prove contravariant naturality in \(X\) and naturality in the whole diagram \(D\). The Hom and quotient laws give identities and composition. Replacing the chosen colimit by an isomorphic cocone composes (1.1) with the corresponding Hom bijection, so bijectivity is independent of that choice. Surjectivity asks for a stage factor of every actual map \(X\to L\). Injectivity asks for a common later-stage equality of two representatives. No choice from an empty Hom set is made.

2. An existing bounded colimit is accessible

Theorem 2.1. Let \(\beta:J\to C_\pi\) be a functor with \(|\operatorname{Mor}J|<\pi\). Suppose its particular colimit \(B\) exists in \(C\), with coprojections \(c_j:\beta(j)\to B\). Then \(B\in C_\pi\).

The existence of this \(J\)-colimit is part of the hypothesis. The assumed existence of \(\pi\)-filtered colimits does not create it. Neither regularity nor existence of all bounded-shape colimits is added.

Proof. Fix a small \(\pi\)-filtered \(I\), a functor \(D:I\to C\), and its specified colimit \((L,a_i)\). Put

This is a Set functor on \(J^{\mathrm{op}}\times I\). An arrow \(s:j\to j'\) acts by precomposition with \(\beta(s)\), from the \(j'\) value to the \(j\) value. An arrow \(t:i\to i'\) acts by postcomposition with \(D(t)\). Associativity makes these actions commute and proves their identity and composite laws. All values and the Set constructions are small by the retained Hom encodings and universe operations.

For every \(T\), the complete cocone universal property identifies

The tuple satisfies \((f c_{j'})\beta(s)=f c_j\) for every actual \(s\). Its inverse is the unique cocone factor. Postcomposition by \(v:T\to T'\) sends every leg to \(v f c_j\), so (2.2) is natural in \(T\); in particular \((R_{D(i)})_i\) is an isomorphism of the stage diagrams.

The bounded Set exchange of the companion lesson, with its entire-arrow bound and empty-shape case, gives the middle bijection in

Each \(\chi_{\beta(j),D}\) is bijective by the hypothesis \(\beta(j)\in C_\pi\). Its naturality under \(\beta(s)\) is the precomposition square of Section 1. The inverse functions also commute with these maps, by composing that square with the two inverses. They therefore give an isomorphism of the \(J^{\mathrm{op}}\)-diagrams and hence a bijection on compatible tuples. Every arrow in (2.3) is thus justified for arbitrary infinite \(\pi\).

The composite is the specific comparison \(\chi_{B,D}\). Indeed, a representative \([i,f]\), with \(f:B\to D(i)\), follows the routes

The final equality uses every original coprojection \(c_j\). Representatives cover the source quotient, so (2.4) proves equality of functions, not merely existence of some bijection. It proves accessibility of \(B\).

The whole comparison is natural in \(D\): a transformation \(\eta\) replaces \(f\) by \(\eta_i f\) and its final value by \(\ell a_i f\), as in (1.2). It is also compatible with a transformation \(\theta:\beta\to\beta'\) between two diagrams satisfying the hypotheses. Their induced map \(b:B\to B'\) satisfies \(b c_j=c_j'\theta_j\); precomposing at each stage by \(b\) corresponds under (2.2) to precomposing the \(j\) leg by \(\theta_j\). The two final values are \(a_i(f b)=(a_i f)b\). These identities verify both naturalities with the actual structural maps. Identities and composites follow from their same leg equations and uniqueness.

If \(J\) is empty, the specified \(B\) is initial. Every Hom out of it is a singleton, and the target tuple set is the singleton empty tuple. A \(\pi\)-filtered \(I\) is nonempty and connected: two objects have a receiver. Its colimit of singleton sets is consequently a singleton by the quotient test. Thus the empty case of (2.3) and (2.4) is included. Arbitrary object and arrow labels are transported using the complete category encoding, not changed by a small skeleton without its maps. \(\square\)

Worked instance. At \(\pi=\aleph_0\), an existing colimit of a finite-total-arrow diagram of accessible objects is accessible. In particular a pushout that already exists has this property. The walking span has three objects, their three identities and its two nonidentity arrows. This verifies the entire-arrow bound. The theorem does not assert that a category with filtered colimits has pushouts.

3. Receive maps into a fixed target

Now strengthen the existence hypothesis: suppose \(C\) admits every small colimit. Let \(\iota:C_\pi\hookrightarrow C\) be the full inclusion, and fix any \(X\in C\). The costructured-arrow category \((\iota\downarrow X)\) has objects \((Y,u)\), where \(Y\in C_\pi\) and \(u:Y\to X\). Its arrows are

Identities satisfy the equation, and \(u''g=u'\), \(u'f=u\) imply \(u''gf=u\). Composition, associativity and units are the original ones in \(C\). The direction is from an accessible object to \(X\). No accessibility of \(X\) is assumed.

Theorem 3.1. Both \(C_\pi\) and \((\iota\downarrow X)\) are \(\pi\)-filtered.

Proof for \(C_\pi\). For any whole functor \(\beta:J\to C_\pi\) with fewer than \(\pi\) total arrows, cocompleteness supplies its colimit \(B\) in \(C\). Theorem 2.1 puts \(B\) in \(C_\pi\). Fullness retains every \(c_j\), and \(c_{j'}\beta(s)=c_j\) verifies every cocone equation in that full subcategory. The arbitrary-cardinal criterion of the companion proves the claim. For empty \(J\) the receiver is the initial object \(0\), which is accessible by the empty case of Theorem 2.1.

Proof for the costructured-arrow category. Given \(\Phi:J\to(\iota\downarrow X)\), write \(\Phi(j)=(Y_j,u_j)\). Its underlying functor is \(\beta:J\to C_\pi\), and its whole-arrow equations say

Form the specified underlying colimit \((B,c_j)\). By Theorem 2.1, \(B\) is accessible. Equation (3.2) gives its unique factor \(u:B\to X\) with \(u c_j=u_j\). Therefore each \(c_j\) is an actual arrow from \((Y_j,u_j)\) to \((B,u)\) in (3.1), and the original colimit equations make them a cocone on all of \(\Phi\).

In fact this is a colimit in the costructured-arrow category. For a cocone with legs \(s_j:(Y_j,u_j)\to(Z,v)\), the underlying factor \(w:B\to Z\) satisfies \(w c_j=s_j\). Then \(v w c_j=v s_j=u_j=u c_j\) for all \(j\), so uniqueness of the underlying factor to \(X\) gives \(v w=u\). Hence \(w\) is a costructured-arrow morphism. Its uniqueness is the same underlying uniqueness; fullness retains it. For empty \(J\), use \((0,0\to X)\). Applying the same bounded-diagram criterion proves \(\pi\)-filteredness, without regularity. \(\square\)

Worked instance. In sets, \((\iota\downarrow X)\) records small accessible sets whose elements are labelled by points of \(X\). When \(\pi\) is regular, Section 4 identifies its domains as the sets of cardinal below \(\pi\). If \(|X|\geq\pi\), this category is still \(\pi\)-filtered, but has no terminal object. A terminal \((Y,u)\) would give, for each singleton labelled by \(x\in X\), exactly one arrow to \((Y,u)\). Thus each fibre \(u^{-1}(x)\) would contain exactly one element. The map \(u\) would be bijective, contrary to \(|Y|<\pi\). Filtered receiving witnesses do not require \(X\) itself as an accessible receiver.

4. The exact accessible sets at a regular cardinal

For this section add the hypothesis that \(\pi\) is regular. We use its tagged-union form from the cardinal companion: a family indexed by fewer than \(\pi\) points, with every summand of cardinal below \(\pi\), has tagged union of cardinal below \(\pi\). The ordinary union inherits this bound, by sending each element to its least occurrence in a well-order of the index. Empty summands and an empty index are included. This is an explicit regularity condition, stronger than the finite-union bound used earlier.

Theorem 4.1. For every object \(A\) of \(\mathsf{Set}_{\mathcal U}\),

Joël Riou (2025), Mathlib's type classification proves the regular-cardinal classification using element lifting, equality synchronization, the subset diagram and factorization of the identity. The linked source retains Apache-2.0 terms. The following Set formulas identify all those maps and the fixed-universe interpretation.

Small cardinal implies accessibility. This direction needs only that \(\pi\) is infinite. Let \(|A|<\pi\) and let \(D:I\to\mathsf{Set}_{\mathcal U}\) be small and \(\pi\)-filtered, with colimit \((Q,a_i)\). Its comparison sends \([i,f:A\to D(i)]\) to \(a_i f\).

Given a function \(g:A\to Q\), select a representative \([i_a,x_a]\) for each existing value \(g(a)\). Receive the fewer-than-\(\pi\) stages at \(i_0\), with arrows \(r_a:i_a\to i_0\), and set \(f(a)=D(r_a)x_a\). Then \(a_{i_0}f=g\). If \(A\) is empty, choose any \(i_0\in I\) and the empty function. This proves surjectivity for arbitrary \(A\) of that cardinal, rather than just finite \(A\).

For injectivity, first receive two representative stages at one \(i_0\). Their functions \(f,g:A\to D(i_0)\) have equal images in \(Q\). For each \(a\), the same-stage equality test gives \(t_a:i_0\to i_a\) making \(D(t_a)f(a)=D(t_a)g(a)\). The companion's common-arrow lemma gives one \(h:i_0\to i_1\) factoring through all \(t_a\). Thus \(D(h)f=D(h)g\) as functions. The representatives have equal quotient classes. For empty \(A\) use \(h=1_{i_0}\). This proves bijectivity of the specific comparison; its naturalities are (1.2) and precomposition. In particular the empty set and singleton are accessible for every infinite \(\pi\).

Accessibility implies small cardinal. Define the inclusion poset

Its objects form a subset of \(\mathcal P(A)\), and its total arrow set is the subset of their square consisting of pairs \((B,B')\) with \(B\subseteq B'\). The identity at \(B\) is \((B,B)\), and composition is \((B',B'')\circ(B,B')=(B,B'')\). Their graphs are small by the universe bounds. External labels transport through \(B\mapsto e(B)\) for a bijection \(e:A\to A_0\in\mathcal U\), and through the same map on both coordinates of every arrow. Thus the whole category is small. It need not have fewer than \(\pi\) total arrows.

For a family \((B_t)_{t\in T}\) with \(|T|<\pi\), regularity puts \(W=\bigcup_t B_t\) below \(\pi\). The actual inclusions \(B_t\to W\) receive it. An empty family is received by \(\varnothing\). The category is thin, so every parallel-arrow family is already equal; the target identity equalizes it, including an empty family. Hence \(P_{<\pi}(A)\) is \(\pi\)-filtered.

Its diagram \(B\mapsto B\), with every inclusion, has colimit \(A\) with its actual inclusions \(b_B:B\hookrightarrow A\). To verify the full factor property, let \(v_B:B\to T\) be a compatible cocone. For \(a\in A\), define \(v(a)=v_{\{a\}}(a)\); singletons are stages because \(\pi\) is infinite. Whenever \(a\in B\), compatibility with \(\{a\}\subseteq B\) gives \(v(a)=v_B(a)\). Thus \(v b_B=v_B\). These equations on singleton stages force uniqueness, and postcomposition of a target cocone gives postcomposition of \(v\). For \(A=\varnothing\) the empty stage gives the unique empty factor. This specified colimit uses no regularity; regularity was needed for its stronger filteredness.

If \(A\) is accessible, its comparison for this small \(\pi\)-filtered diagram is onto. In particular \(1_A\) has a stage representative \([B,f:A\to B]\), satisfying

For each \(a\in A\), (4.3) puts \(a\) in \(B\). Hence \(A=B\), and \(|A|<\pi\). Conversely, when \(|A|\geq\pi\), the identity is an explicit map outside this comparison's image. The equality (4.1) describes the full object property in the fixed universe; both full subcategories retain all functions between the selected sets. No finite, countable or nonempty restriction on \(A\) was made. \(\square\)

5. Cardinal conditions on ordinary ind-objects

For this section return to an arbitrary locally small \(C\), with ambient set data. No colimits in \(C\) are assumed. Let a presheaf be a functor \(A:C^{\mathrm{op}}\to\mathsf{Set}_{\mathcal U}\). The existing complete formal pointwise colimit interface constructs small colimits of such presheaves with every class map and natural factor. Its indices remain small even if the objects of \(C\) are large.

An ordinary ind-object is a presheaf admitting a small nonempty filtered presentation \(A\simeq\operatorname{colim}_{i\in I}h_{X_i}\), where \(h_X=\operatorname{Hom}_C(-,X)\). This colimit is in presheaves. The complete recognition theorem and its proof identifies this condition with a filtered, cofinally small category of elements. In its proof every element is represented at a stage; two element objects are received at a common stage; parallel element arrows are equalized by the same-stage equality test. The full subcategory on the structural element objects is a small receiving family. These are the exact reused interfaces; local smallness alone does not replace their cofinal-smallness hypothesis.

Explicitly, the category \(E_A\) has objects \((T,x)\) with \(x\in A(T)\), and an arrow is

The complete element-category law proof gives identities and composition: \(A(1_T)x=x\), and if \(A(f)x'=x\), \(A(g)x''=x'\), then \(A(gf)x''=A(f)A(g)x''=x\). Associativity and units are inherited. Each element Hom is a subset of the corresponding \(C\)-Hom, hence small. The retained Yoneda bijection sends \(x\) to \(\alpha_x:h_T\to A\) with \((\alpha_x)_S(u)=A(u)x\); its naturality is the presheaf equation \(A(v)A(u)x=A(uv)x\), and its inverse evaluates at \(1_T\). For \(f:T\to T'\), postcomposition gives \(h_f:h_T\to h_{T'}\). The equation \(\alpha_{x'}h_f=\alpha_x\) holds on every \(u:S\to T\) precisely when \(A(fu)x'=A(u)x\); (5.1) implies all these equations, and evaluation at \(u=1_T\) recovers (5.1). Thus this is the entire costructured-arrow category of maps \(h_T\to A\), with the same arrows, identities and composites. Its direction retains the actual Yoneda map into \(A\).

Here cofinally small means that a small full subcategory receives an arrow from every element object. Its entire arrow set is small: over its small set of object pairs, take the tagged union of subsets of the small \(C\)-Hom sets. The recognition theorem supplies this witness for an already ordinary ind-object. The full category \(E_A\) itself may still be large.

Define

as a full subcategory. An arrow between two selected objects is the same natural transformation as in ordinary \(\operatorname{Ind}(C)\); identities and composition are the existing componentwise ones. Both requirements in (5.2) are present: being an ordinary ind-object, with its cofinally small elements, and the additional cardinal-filteredness condition. It is not a definition involving all presheaves with locally small elements. It adds no small object set of \(C\), no colimits in \(C\), and no ordinary realization of the formal presentation. Natural-transformation sets can be handled in the chosen ambient universe without asserting that arbitrary presheaf Hom sets are working-universe small.

Proposition 5.1. For arbitrary infinite cardinals \(\pi'\leq\pi\),

Proof. Every ordinary ind-object has filtered elements by the complete recognition theorem. The ordinary-filteredness criterion is exactly the \(\aleph_0\) criterion, including nonemptiness, so every such object satisfies the first condition in (5.3). The reverse object inclusion is part of (5.2).

For the second assertion, any object-family or parallel-arrow test of cardinal below \(\pi'\) is below \(\pi\). Every receiver and equalizing postarrow supplied by \(\pi\)-filteredness therefore satisfies that same test for \(\pi'\). Empty tests are unchanged. Apply this elementary restriction to the same \(E_A\), retaining its ordinary ind-object and cofinal-smallness conditions. Both subcategories are full, so the inclusion acts identically on every actual natural transformation and preserves its identities and composites. No regularity or new existence theorem is involved. \(\square\)

Worked instance. A representable \(h_T\) has the one-object filtered presentation, so is an ordinary ind-object. Its elements form \(C/T\): an object is \(u:S\to T\), and an arrow \(f:S\to S'\) satisfies \(u'f=u\). The object \((T,1_T)\) is terminal. Its unique incoming legs receive any family; for parallel arrows, postcompose to it and uniqueness equalizes them. The empty family is also received by it. Thus \(h_T\) belongs to \(\operatorname{Ind}^{\pi}(C)\) for every infinite \(\pi\), even if \(C\) has no small colimits.

If \(C\) is empty, there is a unique empty-domain presheaf, but it has no small nonempty filtered presentation by objects of \(C\). Its elements are empty, hence not filtered. Therefore \(\operatorname{Ind}(C)\) and every \(\operatorname{Ind}^{\pi}(C)\) are empty, and the full equalities and inclusions above still hold. No representable is invented in this case.

6. Four original exercises with complete solutions

Exercise 1. (intermediate) A given pushout without general cocompleteness

Let \(C\) admit small \(\pi\)-filtered colimits. Suppose \(A_0,A_1,A_2\in C_\pi\), and a particular span \(A_1\leftarrow A_0\to A_2\) has a pushout \(P\). Prove accessibility of \(P\) directly on the comparison, identifying all lifts and equalities. Do not assume any other pushout exists.

Solution. Write the span arrows \(s:A_0\to A_1\), \(t:A_0\to A_2\), and the specified pushout legs \(p_1:A_1\to P\), \(p_2:A_2\to P\), with \(p_1s=p_2t\). Fix \((L,a_i)=\operatorname{colim}_I D\).

Given \(q:P\to L\), accessibility of \(A_1,A_2\) factors \(q p_1\) and \(q p_2\) at stages. Receive the two stages at \(i_0\), obtaining \(f_1:A_1\to D(i_0)\), \(f_2:A_2\to D(i_0)\) with \(a_{i_0}f_r=q p_r\). The two maps \(f_1s,f_2t:A_0\to D(i_0)\) have equal composites into \(L\). Injectivity of \(\chi_{A_0,D}\), followed by the same-stage test in its Hom diagram, gives one \(h:i_0\to i_1\) such that \(D(h)f_1s=D(h)f_2t\). The given pushout supplies a unique \(f:P\to D(i_1)\) with \(f p_r=D(h)f_r\). Its composite into \(L\) agrees with \(q\) on both pushout legs, hence equals \(q\). This proves surjectivity.

For injectivity, receive two representative stages at \(i_0\), so the representatives are \(v,w:P\to D(i_0)\) with \(a_{i_0}v=a_{i_0}w\). Accessibility of \(A_1,A_2\) gives outgoing witnesses making \(v p_r,w p_r\) equal. The common-arrow lemma combines these two witnesses into one \(h:i_0\to i_1\). Then \(D(h)v\) and \(D(h)w\) agree on both \(p_r\), so the pushout factor uniqueness makes them equal. Their quotient classes agree. The canonical comparison is bijective. Only the specified pushout was used; the theorem applies for arbitrary infinite \(\pi\). Empty Hom sets cause no extra choice because every selected lift belongs to an actual given map or class.

Exercise 2. (intermediate) Labelled sets and every slice arrow

Let \(\pi\) be infinite regular and let \(X\) be any small set. Construct receiving objects and equalizing arrows in the category of maps \(Y\to X\) with \(|Y|<\pi\). Treat bounded object families, bounded parallel-arrow families and both empty cases explicitly.

Solution. For \((u_a:Y_a\to X)_{a\in A}\), with \(|A|<\pi\), take \(Y=\coprod_aY_a\). Regularity gives \(|Y|<\pi\). Define \(u(a,y)=u_a(y)\). Each tagged inclusion \(e_a:Y_a\to Y\) has \(u e_a=u_a\), hence is an actual costructured-arrow leg. For empty \(A\), take \(\varnothing\to X\).

For parallel arrows \(f_b:(Y,u)\to(Z,v)\), generate on \(Z\) the equivalence relation identifying \(f_b(y)\) with \(f_{b'}(y)\) for every \(b,b',y\). Let \(q:Z\to Q\) be its quotient. Each generating pair has the same value under \(v\), because \(v f_b=u=v f_{b'}\). Thus \(v\) is constant on the generated relation and descends to \(\bar v:Q\to X\), with \(\bar v q=v\). Since a quotient of \(Z\) has cardinal at most \(|Z|<\pi\), the target is an object. The actual arrow \(q:(Z,v)\to(Q,\bar v)\) equalizes every \(f_b\). If the parallel family is empty, choose \(q=1_Z\); no equivalence generators are needed. These are the two cardinal-filteredness axioms with their full triangle equations. No bound on \(|X|\) below \(\pi\) was assumed.

Exercise 3. (advanced) Locate the use of regularity

Let \(\lambda\in\mathcal U\) be an infinite cardinal failing the tagged-union regularity condition. Construct a small set \(T\) such that \(P_{<\lambda}(T)\) is ordinarily filtered but not \(\lambda\)-filtered. Explain exactly which step of the converse proof in Section 4 cannot use this diagram.

Solution. Failure of regularity gives a set \(A\) with \(|A|<\lambda\) and sets \(B_a\) with \(|B_a|<\lambda\), whose tagged union has cardinal at least \(\lambda\). Transport the index and summands to universe members using the complete encodings; the same cardinal bounds and tagged-union cardinal are preserved. Put \(T=\coprod_a B_a\), a universe-member set by indexed-union closure. Each tagged block \(T_a=\{a\}\times B_a\) belongs to \(P_{<\lambda}(T)\).

The empty subset is a stage, and the finite union of any two stages has cardinal below arbitrary infinite \(\lambda\), by the retained finite-union bound. Thus finite families have a receiver, while thinness equalizes parallel arrows. This proves ordinary filteredness. But the fewer-than-\(\lambda\) family \((T_a)_a\) has no receiver in that poset: a receiving subset must contain their union \(T\), whose cardinal is at least \(\lambda\). It is not \(\lambda\)-filtered.

The inclusions of these small subsets still have colimit \(T\) by the singleton-stage factor argument. What fails is permission to apply \(\lambda\)-accessibility to that particular index. The exercise does not infer an accessibility classification for singular cardinals. It identifies the exact missing hypothesis in the regular-cardinal converse.

Exercise 4. (advanced) A strict decrease of cardinal ind-objects

Let \(C\) be the inclusion poset of finite subsets of \(\mathbb N\), and let \(A:C^{\mathrm{op}}\to\mathsf{Set}\) be the singleton-valued constant presheaf. Prove that \(A\in\operatorname{Ind}^{\aleph_0}(C)\) but \(A\notin\operatorname{Ind}^{\aleph_1}(C)\). Give its actual ordinary ind-presentation and every relevant arrow direction.

Solution. The category \(C\) is small: its object set is a subset of \(\mathcal P(\mathbb N)\), and its whole arrow set is a subset of that object's square. It is nonempty, finite unions receive finite families, and thinness equalizes parallel arrows. Thus \(C\) is ordinarily filtered.

Use the diagram \(F\mapsto h_F\), indexed by that same \(C\). At a finite test subset \(S\), \(h_F(S)\) is a singleton if \(S\subseteq F\), and is empty otherwise. A transition \(F\subseteq G\) is induced by postcomposition with the inclusion. There is a representative at \(F=S\). Any two representatives become the same singleton point at \(F\cup G\). Hence the pointwise colimit is a singleton. Restriction along \(S\subseteq S'\) sends the unique represented point at \(S'\) to the unique point at \(S\), so the pointwise bijections are natural and give \(A\simeq\operatorname{colim}_{F\in C}h_F\). This is a small nonempty filtered presentation in presheaves; no colimit of the whole diagram of finite sets inside \(C\) is invoked.

Each \(A(S)\) has one point. Its category of elements therefore has exactly the objects \((S,\ast)\) and exactly the arrows \(S\subseteq S'\), because \(A(S\subseteq S')\ast=\ast\). Thus \(E_A\simeq C\), ordinarily filtered, giving membership in \(\operatorname{Ind}^{\aleph_0}(C)\).

The countable family \(F_n=\{0,\ldots,n\}\) has cardinal below \(\aleph_1\) but has no finite-set receiver: any receiver must contain every natural number. Consequently \(E_A\) is not \(\aleph_1\)-filtered. This proves the strict inclusion in this example. The full-subcategory arrows remain natural transformations throughout; the obstruction concerns an object family's receivers.

7. Prerequisites

The linked universe, Hom, compatible-family, quotient, pointwise presheaf and ordinary Ind constructions supply the prerequisite interfaces. The cardinal and bounded-exchange companion lessons supply the stated prerequisite results. The pinned Mathlib type proof corroborates and supplies the exact regular-cardinal Set classification interface; its regularity typeclass is retained, and no general arbitrary-cardinal result is inferred from it. The new arguments identify the arbitrary-cardinal closure comparison on all legs, lift entire diagrams in the costructured-arrow category, and restrict cardinal tests on already ordinary ind-objects. The proof interfaces keep their original attribution and terms.