Limits and Colimits

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Constant diagrams, cones, cocones, and their morphisms

Definition

Let $J$ and $C$ be categories and let $c \in C$ . The constant diagram at $c$ is the functor $Δ c : J \to C$ that sends every object to $c$ and every morphism to $1_{c}$ (Covariant functor, identity functor, composite functor, and contravariant functor).

For a diagram $D : J \to C$ (Diagram as a functor from an indexing category), a cone over $D$ with apex $c$ is a natural transformation $λ : Δ c \Rightarrow D$ (Natural transformation and its components). Thus it is a family $λ_{j} : c \to D (j)$ satisfying

$D (u) λ_{j} = λ_{k} (u : j \to k) .$

A morphism of cones $(c, λ) \to (c^{'}, λ^{'})$ is a morphism $h : c \to c^{'}$ such that $λ_{j}^{'} h = λ_{j}$ for every $j$ . Cones and their morphisms form the category $Cone (D)$ .

Dually, a cocone under $D$ with apex $c$ is a natural transformation $ρ : D \Rightarrow Δ c$ , so $ρ_{k} D (u) = ρ_{j}$ . A morphism of cocones $(c, ρ) \to (c^{'}, ρ^{'})$ is a morphism $h : c \to c^{'}$ satisfying $h ρ_{j} = ρ_{j}^{'}$ for every $j$ . These form $Cocone (D)$ .

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties

Definition

Let $D : J \to C$ be a diagram. A limit of $D$ is a terminal object $(L, λ)$ of $Cone (D)$ (Constant diagrams, cones, cocones, and their morphisms, Initial object, terminal object, and zero object). It is written

$L = \lim_{j \in J} D (j), λ_{j} : L \to D (j) .$ Explicitly, for every cone $(X, ξ)$ there exists a unique morphism $u : X \to L$ such that $λ_{j} u = ξ_{j}$ for every $j$ . The diagram has a limit when such a cone exists. A colimit of $D$ is an initial object $(Q, ρ)$ of $Cocone (D)$ , written $Q = {colim}_{j \in J} D (j), ρ_{j} : D (j) \to Q .$

Explicitly, for every cocone $(X, ξ)$ there exists a unique morphism $u : Q \to X$ such that $u ρ_{j} = ξ_{j}$ for every $j$ . The diagram has a colimit when such a cocone exists.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Any two limits, or any two colimits, of one diagram are uniquely isomorphic compatibly with their structure maps

Statement

If $(L, λ)$ and $(L^{'}, λ^{'})$ are limits of one diagram $D$ , there is a unique isomorphism $u : L \to L^{'}$ satisfying $λ_{j}^{'} u = λ_{j}$ for every $j$ . Dually, any two colimits of $D$ are joined by a unique isomorphism that commutes with every cocone leg.

Facts & Assumptions

Given: Two limiting cones $(L, λ)$ and $(L^{'}, λ^{'})$ over $D$ .

[F1]

A limit is a terminal cone: every cone has a unique morphism to it, and a colimit is an initial cocone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[L1]

Any two terminal objects are uniquely isomorphic, as are any two initial objects (Initial and terminal objects are unique up to a unique isomorphism).

[L2]

An isomorphism has a two-sided inverse (Isomorphism, groupoid, and connected category).

Proof

technique · universal property

1.1

By [F1], there are unique cone morphisms $u : L \to L^{'}$ and $v : L^{'} \to L$ ; hence $λ_{j}^{'} u = λ_{j}$ and $λ_{j} v = λ_{j}^{'}$ for every $j$ .

F1

2.1

Both $v u$ and $1_{L}$ are cone morphisms from $(L, λ)$ to itself, so terminal uniqueness gives $v u = 1_{L}$ . Similarly $u v = 1_{L^{'}}$ .

F1step 1.1

3.1

Thus $u$ is an isomorphism with inverse $v$ . Any compatible isomorphism is a cone morphism $L \to L^{'}$ , so it equals $u$ by uniqueness.

L2step 1.1step 2.1

4.1

The same argument in $Cocone (D)$ uses initial rather than terminal uniqueness [L1]: the unique morphisms between the two initial cocones are inverse and commute with all cocone legs.

F1L1∎

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category

Statement

For $D : J \to C$ , let $D^{o p} : J^{o p} \to C^{o p}$ be the same object and arrow assignment with directions reversed. A cone $λ : Δ L \Rightarrow D$ is limiting in $C$ if and only if the reversed family is a colimiting cocone under $D^{o p}$ in $C^{o p}$ . The dual assertion exchanges colimits and limits.

Facts & Assumptions

Given: A diagram $D : J \to C$ .

[F1]

Limits are terminal cones and colimits are initial cocones (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F2]

The opposite category has the same objects and reverses all morphisms and composites (Opposite category $C^{o p}$ ).

[L1]

A formally dual theorem follows by reversing every morphism and the order of every composite (Every theorem about categories has a formal dual obtained by reversing morphisms and composition).

Proof

technique · duality

1.1

Reversing $λ_{j} : L \to D (j)$ gives $λ_{j}^{o p} : D (j) \to L$ . The cone equation $D (u) λ_{j} = λ_{k}$ reverses to the cocone equation $λ_{j}^{o p} D (u)^{o p} = λ_{k}^{o p}$ .

F2

1.2

A cone morphism $h : (X, ξ) \to (L, λ)$ reverses to a cocone morphism from $(L, λ^{o p})$ to $(X, ξ^{o p})$ , and this operation is bijective on morphisms.

F2algebra

2.1

Consequently terminality of $(L, λ)$ among cones is exactly initiality of $(L, λ^{o p})$ among cocones. By [F1], this proves both directions of the asserted equivalence.

F1step 1.1step 1.2

3.1

Applying the same translation a second time gives the colimit-to-limit statement. Any later appeal to duality uses this exact reversal of objects, arrows, hypotheses, and conclusion, as required by [L1].

L1step 2.1∎

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Limits of empty diagrams are terminal objects, and colimits of empty diagrams are initial objects

Statement

For the unique diagram $D : \emptyset \to C$ , an object is the apex of a limiting cone exactly when it is terminal in $C$ . It is the apex of a colimiting cocone exactly when it is initial in $C$ .

Facts & Assumptions

Given: The empty diagram $D : \emptyset \to C$ .

[F1]

A limit is a terminal cone and a colimit is an initial cocone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F2]

An object is terminal when every object has exactly one morphism to it, and initial when it has exactly one morphism to every object (Initial object, terminal object, and zero object).

[L1]

Limits in a category are colimits of the dual diagram in the opposite category (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · universal property

1.1

A cone over $D$ with apex $X$ has no legs, and every morphism $X \to Y$ is a cone morphism because there are no compatibility equations.

given

2.1

Hence a cone with apex $T$ is terminal in the cone category if and only if for every $X$ there is exactly one morphism $X \to T$ . By [F1] and [F2], this is equivalent to $T$ being both a limit apex and a terminal object.

F1F2step 1.1

3.1

The empty category is its own opposite. Applying [L1] to step 2.1 turns the limiting assertion into the assertion that an empty-diagram colimit is an initial object, in both directions.

L1step 2.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations

Definition

Let $(A_{i})_{i \in I}$ be an indexed family of objects (An indexed family $(A_{i})_{i \in I}$ is a function with domain $I$ ; ${A_{i} : i \in I}$ is its range), regarded as a diagram on the discrete category $I$ . Its product is its limit (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties): an object $P = \prod_{i \in I} A_{i}$ with projections $p_{i} : P \to A_{i}$ such that every family $f_{i} : X \to A_{i}$ has a unique pairing

$⟨ f_{i} ⟩_{i \in I} : X \to P, p_{i} ⟨ f_{i} ⟩ = f_{i} (i \in I) .$

Its coproduct is its colimit: an object $Q = ∐_{i \in I} A_{i}$ with injections $ι_{i} : A_{i} \to Q$ such that every family $f_{i} : A_{i} \to X$ has a unique copairing

$[f_{i}]_{i \in I} : Q \to X, [f_{i}]_{i \in I} ι_{i} = f_{i} (i \in I) .$

The empty product is therefore terminal and the empty coproduct initial. A one-object product or coproduct is canonically the object itself. A product or coproduct need not exist.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Equalizers and coequalizers as limits and colimits of a parallel pair

Definition

For parallel morphisms $f, g : A ⇉ B$ , an equalizer is a limit of that parallel-pair diagram (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties). It is a morphism $e : E \to A$ satisfying $f e = g e$ such that, whenever $h : X \to A$ satisfies $f h = g h$ , there is a unique $u : X \to E$ with $e u = h$ .

A coequalizer is a colimit of the parallel pair. It is a morphism $q : B \to Q$ satisfying $q f = q g$ such that, whenever $h : B \to X$ satisfies $h f = h g$ , there is a unique $u : Q \to X$ with $u q = h$ .

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Pullbacks and pushouts as limits and colimits of cospans and spans

Definition

For a cospan $X \overset{f}{\to} Z \overset{g}{\leftarrow} Y$ , a pullback is its limit (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties). It consists of an object $X \times_{Z} Y$ and morphisms $p : X \times_{Z} Y \to X$ , $q : X \times_{Z} Y \to Y$ with $f p = g q$ , such that every $a : W \to X$ , $b : W \to Y$ satisfying $f a = g b$ admit a unique $u : W \to X \times_{Z} Y$ with $p u = a$ and $q u = b$ .

For a span $X \overset{f}{\leftarrow} Z \overset{g}{\to} Y$ , a pushout is its colimit. It consists of $X ⨿_{Z} Y$ and morphisms $i : X \to X ⨿_{Z} Y$ , $j : Y \to X ⨿_{Z} Y$ with $i f = j g$ , such that every compatible pair $a : X \to W$ , $b : Y \to W$ has a unique $u : X ⨿_{Z} Y \to W$ satisfying $u i = a$ and $u j = b$ .

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers

Definition

Let $C$ be a category with specified zero morphisms (Category with zero morphisms), and let $f : A \to B$ .

The kernel of $f$ is an equalizer

$\ker (f) \overset{k}{\to} A \begin{array}{c} \overset{f}{\to} \\ \to_{0_{A, B}}^{} \end{array} B .$

The cokernel of $f$ is a coequalizer

$A \begin{array}{c} \overset{f}{\to} \\ \to_{0_{A, B}}^{} \end{array} B \overset{q}{\to} coker (f) .$

in the sense of Equalizers and coequalizers as limits and colimits of a parallel pair. Thus $f k = 0$ and every $h$ with $f h = 0$ factors uniquely through $k$ ; dually, $q f = 0$ and every $h$ with $h f = 0$ factors uniquely through $q$ .

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic

Statement

If $(L, λ_{j})$ is a limiting cone and $r, s : X \to L$ satisfy $λ_{j} r = λ_{j} s$ for every $j$ , then $r = s$ . Dually, if $(Q, ρ_{j})$ is colimiting and $r, s : Q \to X$ satisfy $r ρ_{j} = s ρ_{j}$ for every $j$ , then $r = s$ .

Facts & Assumptions

Given: A limiting cone $(L, λ)$ and morphisms $r, s : X \to L$ with equal composites through every leg.

[F1]

A limiting cone admits exactly one cone morphism from each cone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F2]

Monomorphisms and epimorphisms are defined by left and right cancellation, respectively (Monomorphism and epimorphism by left and right cancellation).

[L1]

The formal dual of a limiting cone is a colimiting cocone (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · universal property

1.1

The common family $ξ_{j} : = λ_{j} r = λ_{j} s$ is a cone, since both families arise by composing the cone $λ$ with an apex morphism.

given

2.1

Both $r$ and $s$ are cone morphisms $(X, ξ) \to (L, λ)$ . The uniqueness clause in [F1] therefore gives $r = s$ .

F1step 1.1

3.1

Reverse every arrow in steps 1.1 and 2.1. By [L1] this says that equal composites after all legs of a colimiting cocone force equality of the two arrows out of its apex.

L1step 1.1step 2.1

4.1

These two cancellation properties are precisely joint monicity and joint epicity; for a one-legged family they reduce to the notions in [F2].

F2step 2.1step 3.1∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Every equalizer is a monomorphism, and every coequalizer is an epimorphism

Statement

Every equalizer morphism is monic, and every coequalizer morphism is epic.

Facts & Assumptions

Given: An equalizer $e : E \to A$ and a coequalizer $q : B \to Q$ .

[F1]

An equalizer is the single nonidentity leg of a limiting cone, and a coequalizer is the single nonidentity leg of a colimiting cocone (Equalizers and coequalizers as limits and colimits of a parallel pair).

[L1]

Limit legs are jointly monic and colimit legs are jointly epic (The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic).

Proof

technique · direct corollary

1.1

If $e r = e s$ , [F1] and the limiting clause of [L1] give $r = s$ ; hence $e$ is monic.

F1L1

2.1

If $r q = s q$ , [F1] and the colimiting clause of [L1] give $r = s$ ; hence $q$ is epic.

F1L1∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

A pullback of a monomorphism is a monomorphism, and a pushout of an epimorphism is an epimorphism

Statement

In a pullback square

if $m$ is monic, then $p$ is monic. Dually, in a pushout square, the pushout of an epimorphism is an epimorphism.

Facts & Assumptions

Given: The displayed pullback and a monomorphism $m$ .

[F1]

The pullback legs satisfy $f p = m q$ and have the stated universal property (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L1]

Pullback legs are jointly monic (The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic).

[F2]

A monomorphism cancels on the left and an epimorphism cancels on the right (Monomorphism and epimorphism by left and right cancellation).

[L2]

Pullbacks dualize to pushouts (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · cancellation

1.1

Let $r, s : W \to P$ satisfy $p r = p s$ . Then $m q r = f p r = f p s = m q s$ by the pullback equation.

F1givenalgebra

2.1

Since $m$ is monic, [F2] gives $q r = q s$ . The two pullback legs now have equal composites with $r$ and $s$ , so [L1] gives $r = s$ . Thus $p$ is monic.

F2L1step 1.1

3.1

Reversing the displayed square changes the pullback into a pushout, $m$ into an epimorphism, and the conclusion into epicity of its pushout. Applying [L2] to steps 1.1 and 2.1 proves the dual assertion.

L2step 1.1step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Pullback and pushout pasting, with cancellation of the square adjacent to the outer edge

Statement

Consider a commutative diagram of two adjacent squares

If both small squares are pullbacks, then the outer rectangle is a pullback. If the right square and the outer rectangle are pullbacks, then the left square is a pullback. Reversing all arrows gives the corresponding composition and cancellation laws for pushouts.

Facts & Assumptions

Given: The displayed commutative diagram.

[F1]

A pullback supplies a unique factor for each compatible pair (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L1]

Pullbacks and pushouts are exact formal duals (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · universal property

1.1

Suppose first that both small squares are pullbacks. Given $r : W \to D$ and $s : W \to C$ with $e d r = z s$ , the right pullback gives a unique $t : W \to B$ with $y t = d r$ and $b t = s$ . The left pullback then gives a unique $u : W \to A$ with $x u = r$ and $a u = t$ .

F1given

1.2

For the cancellation law, assume the right square and outer rectangle are pullbacks. A compatible pair $r : W \to D$ , $t : W \to B$ for the left square gives $b t : W \to C$ and $e d r = z b t$ . The outer property yields a unique $u : W \to A$ with $x u = r$ and $b a u = b t$ . Since $y a u = d x u = d r = y t$ , right-pullback uniqueness gives $a u = t$ . Outer uniqueness gives uniqueness of $u$ .

F1

2.1

This $u$ satisfies $b a u = s$ . If $u^{'}$ has $x u^{'} = r$ and $b a u^{'} = s$ , then the right pullback gives $a u^{'} = t$ , and the left pullback gives $u^{'} = u$ . Hence the outer rectangle is a pullback.

F1step 1.1

3.1

Reversing steps 1.1, 1.2, and 2.1 by [L1] proves the corresponding composition and cancellation laws for pushouts.

L1step 1.1step 2.1step 1.2∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Assuming Choice, cardinality of a small category and κ-small diagrams

Definition

Assume the Axiom of Choice (The Axiom of Choice), so every set has a cardinality (A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used, Cardinal sum $κ \oplus λ$ , product $κ \otimes λ$ and exponentiation $κ^{λ}$ , and why they are written apart from the ordinal operations). For a small category $J$ (Small, locally small, and large categories), define

$∣ J ∣ : = ∣ Mor (J) ∣ .$

Every object contributes an identity morphism, so this convention also bounds the number of objects. The cardinality of a small diagram $D : J \to C$ (Diagram as a functor from an indexing category) is $∣ J ∣$ . For a cardinal $κ$ , the diagram is $κ$ -small when $∣ J ∣ < κ$ .

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Finite, small, and large limits and colimits; complete and cocomplete categories

Definition

A diagram is finite when its indexing category has finitely many morphisms, small when its indexing category is small, and large otherwise (Assuming Choice, cardinality of a small category and κ-small diagrams, Small, locally small, and large categories).

A category has finite limits, small limits, or a specified class of limits when every diagram of the corresponding class has a limit in the sense of Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties. It is complete when it has all small limits. The dual terms are finite colimits, small colimits, and cocomplete. Completeness and cocompleteness do not assert the existence of limits or colimits of large diagrams.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A cone over an identity diagram is weakly initial, and the identity diagram has a limit exactly when the category has an initial object

Statement

A cone $λ : Δ L \Rightarrow 1_{C}$ supplies a morphism from $L$ to every object of $C$ , so $L$ is weakly initial. The possibly large identity diagram $1_{C} : C \to C$ has a limit if and only if $C$ has an initial object; in that event every limiting apex is initial.

Facts & Assumptions

Given: A category $C$ and its identity diagram.

[F1]

Completeness concerns all small diagrams and makes no assertion about a large identity diagram (Finite, small, and large limits and colimits; complete and cocomplete categories).

[F2]

An initial object $I$ has exactly one morphism $I \to C$ for every object $C$ (Initial object, terminal object, and zero object).

Proof

technique · universal property

1.1

A cone $λ$ has a leg $λ_{C} : L \to C$ for every object $C$ , so its apex is weakly initial.

given

1.2

Suppose $λ$ is limiting. Both $1_{L}$ and $λ_{L}$ are morphisms from the cone $λ$ to itself, because naturality gives $λ_{C} λ_{L} = λ_{C}$ . Limit uniqueness yields $λ_{L} = 1_{L}$ .

given

1.3

Conversely, let $I$ be initial. The unique maps $i_{C} : I \to C$ form a cone: for $f : C \to C^{'}$ , both $f i_{C}$ and $i_{C^{'}}$ are maps $I \to C^{'}$ , hence equal by [F2].

F2

2.1

For any $f : L \to C$ , cone naturality for $f$ says $f λ_{L} = λ_{C}$ . By step 1.2, $f = λ_{C}$ . Thus exactly one morphism $L \to C$ exists, and [F2] makes $L$ initial.

F2step 1.2

2.2

For any cone $ξ : Δ X \Rightarrow 1_{C}$ , take $u : = ξ_{I} : X \to I$ . Naturality along $i_{C} : I \to C$ gives $i_{C} u = ξ_{C}$ . If $v : X \to I$ is another cone morphism, its equation at $I$ is $i_{I} v = ξ_{I}$ ; since $i_{I} = 1_{I}$ , $v = u$ . The cone of step 1.3 is limiting.

F2step 1.3

3.1

Steps 1.2, 2.1, 1.3, and 2.2 prove both directions. If $C$ is large, [F1] explains why this conclusion is not supplied merely by completeness.

F1step 2.1step 2.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Set has all small limits, realized as compatible tuples in a set-indexed product

Statement

Every small diagram $D : J \to S e t$ has a limit. It is the set

$L = {(x_{j})_{j \in Ob J} \in \prod_{j} D (j) : D (u) (x_{j}) = x_{k} for every u : j \to k}$

with its coordinate projections.

Facts & Assumptions

Given: A small category $J$ and a diagram $D : J \to S e t$ .

[F1]

A small category has sets of objects and morphisms, and completeness means existence of limits for all small diagrams (Finite, small, and large limits and colimits; complete and cocomplete categories).

[F2]

Sets and functions form $S e t$ (Sets and functions form the large locally small category $S e t$ ).

[F3]

The product of a set-indexed family consists of functions choosing one element from each member (The product $\prod_{i \in I} A_{i} : = {f : I \to ⋃_{i \in I} A_{i} ∣ f (i) \in A_{i} for every i \in I}$ ).

[F4]

A limit requires a unique mediating morphism from every cone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · construction

1.1

By [F1] and [F3], the displayed product and its subset $L$ are sets. For each $j$ , let $p_{j} : L \to D (j)$ be the coordinate function. The defining equalities give $D (u) p_{j} = p_{k}$ , so $(L, p)$ is a cone.

F1F2F3

1.2

If $Ob J$ is empty, the product is the singleton containing the empty function and all compatibility conditions are vacuous. Thus the construction still gives the terminal set.

F3

1.3

Let $(X, ξ_{j})$ be any cone. Define $h : X \to \prod_{j} D (j)$ by $h (x)_{j} = ξ_{j} (x)$ . The cone equations imply $h (x) \in L$ , so $h$ corestricts to a function $\overset{ˉ}{h} : X \to L$ satisfying $p_{j} \overset{ˉ}{h} = ξ_{j}$ .

F2given

2.1

If $g : X \to L$ has the same composites, then for every $x$ and $j$ , $g (x)_{j} = p_{j} g (x) = ξ_{j} (x) = p_{j} \overset{ˉ}{h} (x)$ . Equality of functions gives $g = \overset{ˉ}{h}$ . This remains true for the empty index, where there is one function to the singleton.

step 1.2step 1.3

3.1

By [F4], steps 1.1, 1.3, and 2.1 prove that $(L, p)$ is a limit, with step 1.2 covering the empty boundary. Since $D$ was an arbitrary small diagram, $S e t$ is complete.

F1F4step 1.1step 1.3step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Set has all small colimits, realized as a quotient of a set-indexed disjoint union

Statement

Every small diagram $D : J \to S e t$ has a colimit. It is the quotient of the tagged union $S = {(j, x) : x \in D (j)}$ by the least equivalence relation containing

$(j, x) \sim (k, D (u) (x)) (u : j \to k) .$

Facts & Assumptions

Given: A small diagram $D : J \to S e t$ .

[F1]

Smallness makes the object and morphism collections sets, and cocompleteness means existence of all small colimits (Finite, small, and large limits and colimits; complete and cocomplete categories).

[F2]

Sets and functions form $S e t$ (Sets and functions form the large locally small category $S e t$ ).

[F3]

An equivalence relation is reflexive, symmetric, and transitive (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ).

[L1]

A function on a set factors uniquely through its quotient precisely when it is constant on equivalence classes (Let $\sim$ be an equivalence relation on $A$ with quotient map $π : A \to A / \sim$ , and let $f : A \to B$ . There is a function $g : A / \sim \to B$ with $g \circ π = f$ if and only if $a \sim a^{'}$ implies $f (a) = f (a^{'})$ ; and such a $g$ is then unique).

[F4]

A colimit has a unique mediating morphism to every cocone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · construction

1.1

By [F1], $S$ is a set. Intersecting all equivalence relations on $S$ that contain the displayed pairs gives the least such relation $\sim$ ; let $Q = S / \sim$ .

F1F3

2.1

Define $ρ_{j} : D (j) \to Q$ by $ρ_{j} (x) = [j, x]$ . Each generating relation gives $ρ_{k} D (u) = ρ_{j}$ , so $ρ$ is a cocone.

step 1.1

2.2

For a cocone $ξ_{j} : D (j) \to X$ , define $h : S \to X$ by $h (j, x) = ξ_{j} (x)$ . The cocone equations make $h$ equal on every generating pair, hence on the equivalence relation they generate.

givenstep 1.1

2.3

If $J$ is empty, then $S = Q = \emptyset$ ; the empty set has one function to every set, so the same construction is the initial-set colimit.

F2step 1.1

3.1

By [L1], there is a unique $\overset{ˉ}{h} : Q \to X$ with $\overset{ˉ}{h} [j, x] = ξ_{j} (x)$ , equivalently $\overset{ˉ}{h} ρ_{j} = ξ_{j}$ for every $j$ . Any map with these equations has the same composite with the quotient map and therefore equals $\overset{ˉ}{h}$ .

L1step 2.2

4.1

By [F4], the cocone is colimiting. Since $D$ was arbitrary, $S e t$ is cocomplete.

F1F4step 2.1step 3.1step 2.3∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category

Statement

Let $D : J \to C$ be small. If the products

$P = \prod_{j \in Ob J} D (j), Q = \prod_{u : j \to k} D (k)$

and the equalizer of the maps $s, t : P ⇉ Q$ defined by $q_{u} s = D (u) p_{j}$ and $q_{u} t = p_{k}$ exist, then that equalizer is a limit of $D$ .

Facts & Assumptions

Given: The displayed products and an equalizer $e : L \to P$ of $s, t$ .

[F1]

A product represents families of arrows into its factors (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F2]

An equalizer represents arrows on which its parallel pair agrees (Equalizers and coequalizers as limits and colimits of a parallel pair).

[F3]

A small diagram has sets of objects and arrows (Finite, small, and large limits and colimits; complete and cocomplete categories).

[F4]

A limit represents cones by unique mediating arrows (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · construction

1.1

By [F3] the two displayed families are set-indexed. By [F1], the stated coordinate equations define unique maps $s, t : P \to Q$ .

F1F3

2.1

Put $λ_{j} = p_{j} e$ . Since $s e = t e$ , equality of the $u$ -coordinates says $D (u) λ_{j} = λ_{k}$ for every $u : j \to k$ . Thus $λ$ is a cone.

F2step 1.1

2.2

Given a cone $ξ_{j} : X \to D (j)$ , [F1] supplies a unique $a : X \to P$ with $p_{j} a = ξ_{j}$ . Its cone equations imply $q_{u} s a = D (u) ξ_{j} = ξ_{k} = q_{u} t a$ for all $u$ , so product uniqueness gives $s a = t a$ .

F1givenstep 1.1

3.1

By [F2], $a$ factors uniquely as $a = e h$ with $h : X \to L$ . Then $λ_{j} h = p_{j} e h = ξ_{j}$ , so $h$ is a cone morphism.

F2step 2.1step 2.2

4.1

If $h^{'}$ has the same leg equations, product uniqueness gives $e h^{'} = a = e h$ ; equalizer uniqueness gives $h^{'} = h$ .

F1F2step 3.1

5.1

Steps 2.1, 2.2, 3.1, and 4.1 are exactly [F4], so $(L, λ)$ is a limit. If $J$ is empty, both products are terminal objects, $s = t$ , and their equalizer is isomorphic to the terminal object, so the construction still applies.

F1F2F4step 2.1step 3.1step 4.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Every small colimit can be constructed as a coequalizer between coproducts over the arrows and objects of the index category

Statement

Let $D : J \to C$ be small. If the coproducts

$R = ∐_{u : j \to k} D (j), S = ∐_{j} D (j)$

and the coequalizer of $d, c : R ⇉ S$ , where on the $u$ -summand $d ι_{u} = ι_{j}$ and $c ι_{u} = ι_{k} D (u)$ , exist, then that coequalizer is a colimit of $D$ .

Facts & Assumptions

Given: The displayed coproducts and coequalizer.

[L1]

The product-equalizer construction yields every small limit when its constituent limits exist (Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category).

[L2]

Formal duality exchanges limits with colimits, products with coproducts, and equalizers with coequalizers (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

[F1]

Coproducts give unique maps out of families of summands (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F2]

A coequalizer gives a unique factor for each arrow that equalizes its pair (Equalizers and coequalizers as limits and colimits of a parallel pair).

Proof

technique · duality

1.1

Apply [L1] to $D^{o p} : J^{o p} \to C^{o p}$ . By [L2], its object-indexed product becomes $S$ , its arrow-indexed product becomes $R$ , and the two coordinate maps become $d$ and $c$ with exactly the displayed summand equations.

L1L2F1

2.1

The equalizer universal property in $C^{o p}$ becomes the coequalizer property [F2] in $C$ . The limiting cone equations become $q ι_{j} = q ι_{k} D (u)$ , and existence and uniqueness of mediating arrows both reverse to the colimit clauses.

L2F2step 1.1

3.1

Thus the coequalizer is a colimit. When $J$ is empty, both coproducts are initial and the construction returns the initial-object colimit, exactly dual to the boundary case in [L1].

L1L2step 2.1∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers

Statement

A category is complete if and only if it has products indexed by every set and has equalizers of all parallel pairs. Dually, it is cocomplete if and only if it has all small coproducts and all coequalizers.

Facts & Assumptions

Given: A category $C$ .

[L1]

Existing object-indexed products and equalizers construct the limit of every small diagram (Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category).

[L2]

Existing object-indexed coproducts and coequalizers construct the colimit of every small diagram (Every small colimit can be constructed as a coequalizer between coproducts over the arrows and objects of the index category).

[F1]

Complete means having all small limits and cocomplete means having all small colimits (Finite, small, and large limits and colimits; complete and cocomplete categories).

Proof

technique · biconditional

1.1

If $C$ is complete, specialize [F1] to every small discrete category and to the finite parallel-pair category. These limits are all set-indexed products, including the empty product, and all equalizers.

F1

1.2

Conversely, if those products and equalizers exist, [L1] constructs a limit for every small diagram, so [F1] says that $C$ is complete.

L1F1

1.3

If $C$ is cocomplete, specialization gives all set-indexed coproducts, including the empty one, and all coequalizers. Conversely those colimits construct every small colimit by [L2].

L2F1

2.1

Steps 1.1 and 1.2 prove both directions of the completeness equivalence; step 1.3 proves both directions of its cocomplete dual.

step 1.1step 1.2step 1.3∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Finite, nonempty finite, and connected finite (co)limit criteria in terms of products, equalizers, pullbacks, terminal objects, and their duals

Statement

For a category $C$ :

all finite limits exist if and only if finite products and equalizers exist, equivalently if and only if a terminal object and pullbacks exist;
all nonempty finite limits exist if and only if binary products and equalizers exist, equivalently if and only if binary products and pullbacks exist;
all finite connected limits exist if and only if pullbacks and equalizers exist.

Reversing arrows gives the three colimit criteria, with coproducts, coequalizers, an initial object, and pushouts.

Facts & Assumptions

Given: A category $C$ .

[F1]

Empty limits are terminal objects, and empty colimits are initial objects (Limits of empty diagrams are terminal objects, and colimits of empty diagrams are initial objects).

[F2]

Products, equalizers, pullbacks, and their duals have their stated universal properties (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations, Equalizers and coequalizers as limits and colimits of a parallel pair, Pullbacks and pushouts as limits and colimits of cospans and spans).

[L1]

A limit is constructed from products over the objects and arrows of its index category and an equalizer (Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category).

[L2]

The dual coproduct-coequalizer construction gives colimits (Every small colimit can be constructed as a coequalizer between coproducts over the arrows and objects of the index category).

[L3]

Formal duality reverses every hypothesis and conclusion (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · equivalence of constructions

1.1

For a finite index category, both products in [L1] are finite, so finite products and equalizers give all finite limits. Conversely, discrete finite diagrams and parallel pairs show that all finite limits give finite products and equalizers.

L1F2

1.2

If the finite index category is nonempty, its object and arrow sets are nonempty, so the two products in [L1] can be built by iterated binary products without a terminal object. This proves sufficiency from binary products and equalizers; those constructions themselves have nonempty finite shapes, proving necessity. If binary products and pullbacks exist, the equalizer of $f, g : A ⇉ B$ is obtained by pulling $(f, g) : A \to B \times B$ back along the diagonal $B \to B \times B$ . Conversely, nonempty finite limits include binary products and pullbacks. This proves every equivalence in clause 2.

L1F2

1.3

For a finite connected diagram, choose a spanning tree in its finite underlying undirected graph and root it at one object. Start with the root object. When a leaf is attached by an arrow directed from the leaf toward the constructed subtree, pull back the current apex along that arrow; when the arrow points toward the leaf, its required leg is the composite of the existing leg with that arrow and the apex does not change. Induction constructs the universal cone for the tree. For each remaining diagram arrow, take the equalizer of the two maps from the current apex to its codomain, and repeat finitely many times. The result represents exactly the cones over the whole diagram. Conversely, pullbacks and equalizers have finite connected indexing categories. This proves both directions of clause 3, including the one-object case, where loops are imposed by equalizers.

F2

2.1

A terminal object and binary products give every finite product by iteration, including the zero-factor product. An equalizer of $f, g : A ⇉ B$ is the pullback of $(f, g) : A \to B \times B$ along the diagonal $B \to B \times B$ . Hence a terminal object and pullbacks give all finite limits by step 1.1.

F1F2step 1.1

3.1

Conversely, finite limits include the terminal object and every pullback. Thus both formulations in clause 1 are equivalent in both directions.

F1F2step 1.1step 2.1

4.1

Applying [L3] to steps 1.1, 1.2, 1.3, 2.1, and 3.1 exchanges every construction with the one in [L2] and proves all three colimit equivalences, including the empty boundary through [F1].

F1L2L3step 1.1step 2.1step 3.1step 1.2step 1.3∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors

Definition

Let $F : C \to D$ be a functor (Covariant functor, identity functor, composite functor, and contravariant functor) and fix an indexing category $J$ .

$F$ preserves $J$ -limits if the image under $F$ of every limiting cone over $D : J \to C$ is limiting over $F D$ .
$F$ reflects $J$ -limits if a cone over $D$ is limiting whenever its image is limiting.
In the ordinary isomorphism-invariant sense used here, $F$ creates $J$ -limits if every limiting cone over $F D$ is isomorphic as a cone (Natural isomorphism) to the image of a cone over $D$ , that source cone is limiting, and any source cone whose image is limiting is limiting. This does not require an on-the-nose lift of the target apex.
The functor strictly creates $J$ -limits if every limiting cone over $F D$ has a unique lift with exactly the same apex and legs under $F$ , and that lifted cone is limiting. Strict creation therefore contains data not demanded by ordinary isomorphism-invariant creation.

The terms preserves, reflects, and creates colimits use cocones and colimits (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties). A functor is continuous if it preserves all small limits and cocontinuous if it preserves all small colimits.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

A functor preserves a chosen limit exactly when its canonical comparison to the chosen target limit is an isomorphism, and dually for colimits

Statement

Let $(L, λ)$ be a chosen limit of $D : J \to C$ , and let $(M, μ)$ be a chosen limit of $F D$ in $D$ . There is a unique canonical comparison $c : F (L) \to M$ satisfying $μ_{j} c = F (λ_{j})$ . The functor $F$ preserves this limit if and only if $c$ is an isomorphism. Dually, the canonical map from a chosen colimit of $F D$ to the image of a chosen colimit of $D$ is an isomorphism exactly when that colimit is preserved.

Facts & Assumptions

Given: The two chosen limiting cones in the statement.

[F1]

Preservation means that the image of the source limiting cone is limiting (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

[L1]

Two limits of one diagram have a unique compatible isomorphism (Any two limits, or any two colimits, of one diagram are uniquely isomorphic compatibly with their structure maps).

[L2]

Limits and colimits are formal duals (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · biconditional

1.1

The family $F (λ_{j})$ is a cone over $F D$ , so the universal property of $(M, μ)$ gives a unique $c : F (L) \to M$ with $μ_{j} c = F (λ_{j})$ .

given

2.1

If $F$ preserves the limit, [F1] makes $(F (L), F λ)$ another limit of $F D$ . By [L1], its unique compatible map $c$ to $(M, μ)$ is an isomorphism.

F1L1step 1.1

2.2

Conversely, suppose $c$ is an isomorphism. For any cone $ξ$ over $F D$ , its unique factor $h : X \to M$ through $μ$ yields $c^{- 1} h : X \to F (L)$ , and $F (λ_{j}) c^{- 1} h = μ_{j} h = ξ_{j}$ .

givenstep 1.1

3.1

If $r : X \to F (L)$ has these equations, then $c r$ factors $ξ$ through $μ$ , so $c r = h$ and $r = c^{- 1} h$ . Thus $F λ$ is limiting, and [F1] says that $F$ preserves this limit.

F1step 2.2

4.1

Reversing arrows in steps 1.1, 2.1, 2.2, and 3.1 by [L2] gives the colimit comparison and proves both directions of its criterion.

L2step 1.1step 2.1step 2.2step 3.1∎

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Fully faithful functors reflect limits and colimits

Statement

Every fully faithful functor reflects every limit and every colimit, without a smallness restriction on the diagram for which the relevant cone is defined.

Facts & Assumptions

Given: A fully faithful functor $F : C \to D$ , a diagram $D : J \to C$ , and a cone $λ$ whose image is limiting.

[F1]

Reflection means that a source cone is limiting whenever its image is limiting (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

[F2]

Full faithfulness means every hom-map is bijective (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).

[L1]

Colimit reflection is the formal dual of limit reflection (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · universal property

1.1

For a cone $ξ$ over $D$ , the limiting property of $F λ$ gives a unique $h : F (X) \to F (L)$ satisfying $F (λ_{j}) h = F (ξ_{j})$ . Fullness in [F2] gives $u : X \to L$ with $F (u) = h$ .

F2given

2.1

Faithfulness applied to $F (λ_{j} u) = F (λ_{j}) h = F (ξ_{j})$ gives $λ_{j} u = ξ_{j}$ , so $u$ is a cone morphism.

F2step 1.1

3.1

If $v$ is another factor, then $F (v)$ is a factor through the limiting cone $F λ$ , hence $F (v) = h = F (u)$ ; faithfulness gives $v = u$ . Thus $λ$ is limiting, which is reflection in [F1].

F1F2step 1.1step 2.1

4.1

Apply the identical argument in opposite categories. By [L1], full faithfulness remains hom-set bijectivity and the conclusion is reflection of colimits.

F2L1step 1.1step 2.1step 3.1∎

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Equivalences preserve, reflect, and create limits and colimits in the isomorphism-invariant sense

Statement

An equivalence of categories preserves and reflects every existing limit and colimit and creates them in the ordinary isomorphism-invariant sense fixed in Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors. This does not assert strict creation with an unchanged target apex.

Facts & Assumptions

Given: An equivalence $F : C \to D$ .

[F1]

An equivalence has a quasi-inverse $G$ and unit and counit natural isomorphisms (Equivalence, quasi-inverse, and adjoint equivalence of categories, Natural isomorphism).

[L1]

Fully faithful functors reflect limits and colimits (Fully faithful functors reflect limits and colimits).

[F2]

Isomorphism-invariant creation asks for a limiting source lift whose image is isomorphic as a cone to the target limit, together with reflection (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

[L2]

Limits and colimits are formal duals (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · transport of structure

1.1

Since an equivalence is fully faithful, [L1] proves reflection of limits. The quasi-inverse $G$ is also fully faithful and therefore reflects limits.

F1L1

2.1

If $λ$ is a limit cone in $C$ , apply $F$ . If a cone over $F D$ is given, transport it along the unit and counit of [F1], apply $G$ , and factor uniquely through $λ$ . Transporting the factor back gives existence through $F λ$ ; reflection by $G$ gives uniqueness. Hence $F$ preserves limits.

F1step 1.1

3.1

Let $μ$ be a limiting cone over $F D$ . Applying $G$ and using step 2.1 for $G$ gives a limiting cone over $G F D$ . Transport it along the unit $D ≅ G F D$ to a limiting cone $\overset{ˉ}{μ}$ over $D$ . Its image is isomorphic as a cone to $μ$ by the counit and its naturality. Together with reflection from step 1.1, this is creation in [F2].

F1F2step 1.1step 2.1

4.1

Applying [L2] to steps 1.1, 2.1, and 3.1 proves preservation, reflection, and isomorphism-invariant creation of colimits. The construction uses the unit and counit isomorphisms, so it supplies no on-the-nose strict lift.

L2step 1.1step 2.1step 3.1∎

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

A functor that creates limits of a given shape lifts their existence and preserves the created limits, and dually for colimits

Statement

If $F : C \to D$ creates limits of shape $J$ , then for every $D : J \to C$ whose image has a limit, $D$ has a limit and $F$ preserves it. The dual assertion holds for created colimits.

Facts & Assumptions

Given: A functor $F$ creating $J$ -limits and a diagram $D$ such that $F D$ has a limit.

[F1]

Creation lifts a target limiting cone, up to a cone isomorphism, to a limiting source cone and includes reflection (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

[L1]

Preservation of a chosen limit is equivalent to invertibility of its canonical comparison (A functor preserves a chosen limit exactly when its canonical comparison to the chosen target limit is an isomorphism, and dually for colimits).

[L2]

Creation and preservation of colimits are dual to their limit forms (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · unpacking the definition

1.1

Choose a limiting cone $μ$ over $F D$ . By the existence clause of [F1], there is a limiting cone $λ$ over $D$ and a cone isomorphism $F λ ≅ μ$ . Hence $D$ has a limit.

F1given

2.1

The cone isomorphism in step 1.1 is precisely an invertible canonical comparison after identifying its direction by the target universal property. By [L1], $F$ preserves $λ$ .

L1step 1.1

3.1

Because any limiting source cone is uniquely compatibly isomorphic to $λ$ , its image is also limiting. Thus preservation does not depend on the chosen source limit.

F1step 1.1step 2.1

4.1

Reverse every arrow. By [L2], steps 1.1, 2.1, and 3.1 prove existence and preservation for created colimits.

L2step 1.1step 2.1step 3.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Chosen limits and colimits of a fixed small shape assemble into limit and colimit functors

Statement

Let $J$ be small. If a particular limiting cone is chosen for every $D : J \to C$ , these choices define a functor

$\lim_{J} : [J, C] \to C .$

Chosen colimiting cocones similarly define ${colim}_{J} : [J, C] \to C$ .

Facts & Assumptions

Given: A small $J$ and, for every $D$ , a chosen limit $(L_{D}, λ^{D})$ .

[F1]

Objects and arrows of a functor category are functors and natural transformations (Functor category $[C, D]$ , Natural transformation and its components).

[F2]

A chosen limit supplies a unique factor from every cone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F3]

Smallness is cardinality of the indexing category (Assuming Choice, cardinality of a small category and κ-small diagrams).

[L1]

Limit legs are jointly monic (The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic).

[L2]

The colimit construction is the formal dual (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · universal property

1.1

For $α : D \Rightarrow E$ , the family $α_{j} λ_{j}^{D} : L_{D} \to E (j)$ is a cone: for $u : j \to k$ , naturality of $α$ and the cone equation give $E (u) α_{j} λ_{j}^{D} = α_{k} D (u) λ_{j}^{D} = α_{k} λ_{k}^{D}$ .

F1F2

2.1

By [F2], there is a unique morphism $\lim α : L_{D} \to L_{E}$ satisfying $λ_{j}^{E} \lim α = α_{j} λ_{j}^{D}$ for every $j$ .

F2step 1.1

3.1

For $1_{D}$ , both $\lim (1_{D})$ and $1_{L_{D}}$ have the same composites with all $λ_{j}^{D}$ ; [L1] gives $\lim (1_{D}) = 1_{L_{D}}$ .

L1step 2.1

3.2

For $D \overset{α}{\Rightarrow} E \overset{β}{\Rightarrow} H$ , the maps $\lim (β α)$ and $(\lim β) (\lim α)$ have composite $β_{j} α_{j} λ_{j}^{D}$ with every $λ_{j}^{H}$ . By [L1] they are equal. Thus the assignments satisfy the functor laws.

L1step 2.1

4.1

The smallness in [F3] ensures that the functor category is used under the library's set-based indexing convention. Reversing every arrow in steps 1.1, 2.1, 3.1, and 3.2 by [L2] gives the chosen-colimit functor.

F3L2step 1.1step 2.1step 3.1step 3.2∎

RemarkRemark: Literature-sourcedProof: Not applicableaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A limit for each diagram need not provide a chosen limit functor without a simultaneous choice of representatives

Remark

Existence of a limit for each diagram does not itself specify one limiting cone for every diagram. The functors in Chosen limits and colimits of a fixed small shape assemble into limit and colimit functors require simultaneous choices of such cones, an application of an appropriate Axiom of Choice (The Axiom of Choice) when the diagrams and available cones form sets.

Once choices are made, no further arbitrary choices define the action on natural transformations: the universal property forces it. Different systems of chosen limits give naturally isomorphic limit functors because any two limits have unique compatible isomorphisms (Any two limits, or any two colimits, of one diagram are uniquely isomorphic compatibly with their structure maps). For a proper class of diagrams, the needed selection is a separate global or universe-level convention, not a consequence of the set-sized Axiom of Choice.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Every covariantly representable functor to Set preserves all existing small limits

Statement

Let $C$ be locally small and let $R : C \to S e t$ be covariantly representable. For every small diagram in $C$ whose limit exists, its image under $R$ is a limit in $S e t$ .

Facts & Assumptions

Given: A small $D : J \to C$ , a limit $(L, λ)$ , and a representation $R ≅ C (X, -)$ .

[F1]

Covariant and contravariant hom-assignments have their stated actions on morphisms and are functors (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, The assignments $C (a, -)$ and $C (-, a)$ are functors to $S e t$ ).

[F2]

A covariantly representable functor is naturally isomorphic to $C (X, -)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F3]

A limit represents compatible cones by unique arrows (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[L1]

Every small set-valued diagram has a compatible-tuple limit (Set has all small limits, realized as compatible tuples in a set-indexed product).

[L2]

Yoneda's bijection and its inverse are natural in both variables (The Yoneda bijection $Nat (C (a, -), F) ≅ F (a)$ is natural in both $a$ and $F$ ).

Proof

technique · universal property

1.1

For the hom-functor, define $Φ : C (X, L) \to \prod_{j} C (X, D (j))$ by $Φ (f)_{j} = λ_{j} f$ . The cone equations put its image in the compatible subset that [L1] identifies as $\lim_{j} C (X, D (j))$ .

F1F3L1

1.2

Conversely, a compatible family $(f_{j} : X \to D (j))_{j}$ is a cone over $D$ . By [F3] there is a unique $f : X \to L$ with $λ_{j} f = f_{j}$ . This defines an inverse $Ψ$ to $Φ$ .

F3

2.1

The equations in steps 1.1 and 1.2 give $Ψ Φ (f) = f$ by limit uniqueness and $Φ Ψ (f_{j}) = (f_{j})$ coordinatewise. Thus the image cone under $C (X, -)$ is a Set-limit.

F3step 1.1step 1.2

3.1

The natural isomorphism in [F2] transports this limiting cone to the image under $R$ ; its compatibility follows from naturality, equivalently from [L2]. Hence $R$ preserves the limit. Smallness is needed so the limit in [L1] is a set.

F2L1L2step 2.1∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Hom(X,−) is continuous, while Hom(−,X) sends every existing small colimit to a limit of sets

Statement

For every object $X$ of a locally small category $C$ , $C (X, -) : C \to S e t$ preserves all small limits that exist. Moreover, for every small diagram $D$ with a colimit, there is a natural bijection

$C (colim D, X) ≅ \lim_{j \in J^{o p}} C (D (j), X) .$

Facts & Assumptions

Given: An object $X$ and the indicated existing limits or colimits.

[L1]

Every covariantly representable functor preserves small limits (Every covariantly representable functor to Set preserves all existing small limits).

[F1]

$C (X, -)$ and $C (-, X)$ are the covariant and contravariant hom-functors (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[L2]

A colimit in $C$ is a limit in $C^{o p}$ (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

[F2]

Continuous means preserving all small limits (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

Proof

technique · direct corollary

1.1

The functor $C (X, -)$ is represented by $X$ , so [L1] says that it preserves every small existing limit. By [F2], it is continuous whenever the term is applied to the available small limits of its domain.

L1F1F2

1.2

Regard a colimit cocone $D (j) \to Q$ as a limiting cone in $C^{o p}$ by [L2]. Applying [L1] there to the representable $C^{o p} (X, -) = C (-, X)$ gives the displayed limit of hom-sets.

L1F1L2

2.1

Explicitly, the bijection sends $f : Q \to X$ to the compatible family of composites $D (j) \to Q \to X$ ; the colimit existence and uniqueness clauses give its inverse and prove uniqueness.

step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

For small source and index categories, chosen target limits and colimits compute the corresponding functor-category limits and colimits pointwise

Statement

Let $A$ and $J$ be small and let $D : J \to [A, C]$ . If each diagram $j \mapsto D (j) (a)$ has a chosen limit, these limits form a limit of $D$ in the functor category. The dual statement holds pointwise for chosen colimits.

Facts & Assumptions

Given: The two small categories, the diagram $D$ , and a chosen limiting cone $(L (a), λ_{j}^{a})$ at every $a \in A$ .

[F1]

The functor category has functors as objects and natural transformations as morphisms; the small-source hypotheses ensure the stated size control (Functor category $[C, D]$ , If $C$ is small and $D$ is locally small then $[C, D]$ is locally small; if both are small it is small).

[F2]

A limit is characterized by existence and uniqueness of cone factors (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[L1]

Chosen limits act functorially on natural transformations (Chosen limits and colimits of a fixed small shape assemble into limit and colimit functors).

[L2]

Limit legs are jointly monic (The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic).

[L3]

Colimits are the formal dual (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

[F3]

Choice selects an element from every set in a family of nonempty sets (The Axiom of Choice).

Proof

technique · pointwise construction

1.1

For $h : a \to b$ , the maps $D (j) (h) : D (j) (a) \to D (j) (b)$ form a natural transformation of $J$ -diagrams. By [L1] they induce $L (h) : L (a) \to L (b)$ with $λ_{j}^{b} L (h) = D (j) (h) λ_{j}^{a}$ .

F1L1

1.2

Given a cone $ξ : X \Rightarrow D$ in the functor category, pointwise universality gives a unique $u_{a} : X (a) \to L (a)$ with $λ_{j}^{a} u_{a} = ξ_{j, a}$ . For $h : a \to b$ , naturality of $ξ_{j}$ makes $L (h) u_{a}$ and $u_{b} X (h)$ equal after every $λ_{j}^{b}$ ; [L2] makes them equal. Thus the $u_{a}$ form a natural transformation $u : X \Rightarrow L$ .

F1F2L2

2.1

Identity and composition for $L$ follow either from [L1] or by composing with every $λ_{j}^{a}$ and applying [L2]. Thus $L : A \to C$ is a functor, and the displayed equations say each $λ_{j} : L \Rightarrow D (j)$ is natural.

F1L1L2step 1.1

2.2

The transformation $u$ factors the cone componentwise. Any other factor has the same component at every $a$ by pointwise uniqueness, hence equals $u$ . By [F2], $(L, λ)$ is a limit in the functor category.

F1F2step 1.2

3.1

If only existence, rather than chosen limits, is assumed, [F3] selects the pointwise cones over the set of objects of the small category $A$ . Reversing the whole construction by [L3] proves the colimit assertion.

F3L3step 1.1step 2.1step 1.2step 2.2∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

If A is small, then [A,C] is complete or cocomplete whenever C is respectively complete or cocomplete

Statement

Assume Choice. If $A$ is small and $C$ is complete, then $[A, C]$ is complete. If $C$ is cocomplete, then $[A, C]$ is cocomplete.

Facts & Assumptions

Given: A small $A$ and the indicated completeness or cocompleteness of $C$ .

[L1]

Functor-category limits and colimits are computed pointwise when the pointwise choices exist (For small source and index categories, chosen target limits and colimits compute the corresponding functor-category limits and colimits pointwise).

[F1]

Completeness and cocompleteness mean existence of every small limit and colimit (Finite, small, and large limits and colimits; complete and cocomplete categories).

[F2]

Choice permits simultaneous selections from a set-indexed family of nonempty sets (The Axiom of Choice).

Proof

technique · direct corollary

1.1

Let $D : J \to [A, C]$ be small. If $C$ is complete, [F1] supplies a limit of $j \mapsto D (j) (a)$ for every $a$ . Since $A$ is small, [F2] selects these pointwise limits simultaneously.

F1F2

2.1

By [L1], the selected objects form a limit of $D$ . Since $D$ was arbitrary, [F1] says the functor category is complete.

L1F1step 1.1

3.1

If $C$ is cocomplete, make the same set-indexed choices of pointwise colimits and apply the colimit clause of [L1]. This proves cocompleteness, with no assertion for a large source $A$ .

L1F1F2∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

For a small category, the Yoneda functor preserves and reflects all existing small limits

Statement

For a small category $C$ , its Yoneda embedding $y : C \to [C^{o p}, S e t]$ preserves and reflects every small limit that is defined in $C$ .

Facts & Assumptions

Given: A small category $C$ and a small diagram in it.

[F1]

The Yoneda embedding sends $a$ to $C (-, a)$ (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding).

[L1]

Covariant representable functors preserve small limits (Every covariantly representable functor to Set preserves all existing small limits).

[L2]

Limits in functor categories are computed pointwise (For small source and index categories, chosen target limits and colimits compute the corresponding functor-category limits and colimits pointwise).

[L3]

Fully faithful functors reflect limits (Fully faithful functors reflect limits and colimits).

[L4]

The Yoneda embedding is fully faithful (The Yoneda functor is fully faithful, and it is a full embedding when its object map is injective).

Proof

technique · pointwise

1.1

At $c \in C$ , evaluation of the Yoneda image of a limiting cone is its image under $C (c, -)$ by [F1]. This is a limiting cone of sets by [L1].

F1L1

2.1

Since every evaluation is limiting, [L2] says the Yoneda-image cone is a limit in the presheaf category. Thus Yoneda preserves the small limit.

L2step 1.1

3.1

By [L4], Yoneda is fully faithful, so [L3] makes it reflect every limit. The smallness of $C$ ensures that the stated presheaf category and embedding are formed under the library convention.

L3L4∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Iterated small limits commute: either order is canonically isomorphic to the limit over the product category

Statement

Let $J$ and $K$ be small and let $D : J \times K \to C$ . Whenever the displayed limits exist, there are canonical compatible isomorphisms

$\lim_{j} \lim_{k} D (j, k) ≅ \lim_{(j, k)} D (j, k) ≅ \lim_{k} \lim_{j} D (j, k) .$

Facts & Assumptions

Given: Small $J, K$ , the diagram $D$ , and the limits in the statement.

[F1]

A limit represents cones by unique arrows (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[L1]

Two limits of one diagram have a unique compatible isomorphism (Any two limits, or any two colimits, of one diagram are uniquely isomorphic compatibly with their structure maps).

[F2]

The product category has objects $(j, k)$ and componentwise morphisms (Product category and its projection functors).

[F3]

The cardinality of a small category is the cardinality of its morphism set, and a small diagram is one with a small indexing category (Assuming Choice, cardinality of a small category and κ-small diagrams).

Proof

technique · universal property

1.1

By [F2], a cone from $X$ to $D$ is exactly a family of arrows $X \to D (j, k)$ compatible separately with every $J$ -arrow and every $K$ -arrow.

F2

2.1

For each $j$ , the $K$ -limit turns such a compatible $k$ -family into one unique arrow $X \to \lim_{k} D (j, k)$ . Compatibility in $j$ turns these into a cone over the resulting $J$ -diagram, and its limit turns the family into one unique arrow $X \to \lim_{j} \lim_{k} D (j, k)$ . Both constructions reverse by the two universal properties.

F1step 1.1

3.1

Hence the first iterated limit has the universal property of the $J \times K$ -limit. By [L1] it is uniquely compatibly isomorphic to that limit. Interchanging $j$ and $k$ proves the second isomorphism.

F1L1step 2.1

4.1

If either index category is empty, step 1.1 describes an empty family, so each existing expression is a terminal object and [L1] gives the same canonical isomorphisms. The morphisms of $J \times K$ form a subset of the Cartesian product of the two morphism sets, so [F3] makes the product category small and no large diagram has been introduced.

L1F3step 1.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Filtered categories and filtered colimits

Definition

A category $J$ is filtered when every finite diagram in $J$ admits a cocone. Equivalently:

$J$ is nonempty;
for every $j, k$ there are an object $ℓ$ and arrows $j \to ℓ \leftarrow k$ ;
for every parallel pair $f, g : j ⇉ k$ , there is $h : k \to ℓ$ with $h f = h g$ .

The equivalence uses finite diagrams as in Finite, small, and large limits and colimits; complete and cocomplete categories; the nonempty and zigzag language agrees with the connectedness convention in Isomorphism, groupoid, and connected category. A filtered colimit is a colimit (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties) of a diagram indexed by a small filtered category. Smallness is included so the colimit is among the ordinary small colimits.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Two representatives in a filtered colimit of sets are equal exactly when they become equal at one common later stage

Statement

Let $D : J \to S e t$ be a small filtered diagram. For $x \in D (j)$ and $y \in D (k)$ , their images in $colim D$ are equal if and only if there are arrows $a : j \to ℓ$ and $b : k \to ℓ$ such that $D (a) (x) = D (b) (y)$ .

Facts & Assumptions

Given: The filtered diagram and the two elements in the statement.

[F1]

Filteredness supplies common target objects and coequalizers of parallel arrows (Filtered categories and filtered colimits).

[L1]

A Set-colimit is the tagged union modulo the equivalence relation generated by the diagram arrows (Set has all small colimits, realized as a quotient of a set-indexed disjoint union).

[F2]

An equivalence relation is reflexive, symmetric, and transitive (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ).

Proof

technique · identify the generated equivalence relation

1.1

On tagged elements define $(j, x) \approx (k, y)$ when some $j \overset{a}{\to} ℓ \overset{b}{\leftarrow} k$ satisfies $D (a) x = D (b) y$ . Identity arrows prove reflexivity, and exchanging $a, b$ proves symmetry.

F1F2

1.2

For transitivity, suppose the first equality is witnessed in $ℓ$ by $a : j \to ℓ$ , $b : k \to ℓ$ , and the second in $m$ by $c : k \to m$ , $d : n \to m$ . Choose $r : ℓ \to p$ and $s : m \to p$ by [F1]. Then $r b, s c : k ⇉ p$ are parallel, so choose $t : p \to q$ with $t r b = t s c$ . Applying $D$ shows $t r a (x) = t s d (z)$ , proving $(j, x) \approx (n, z)$ .

F1given

2.1

Thus $\approx$ is an equivalence relation. It contains every generating pair $(j, x)$ and $(k, D (u) x)$ by choosing $ℓ = k$ , $a = u$ , and $b = 1_{k}$ . Conversely, a witness $a, b$ gives a chain of two generating identifications from $(j, x)$ and $(k, y)$ to their equal tagged element in $D (ℓ)$ . Hence $\approx$ is exactly the equivalence relation in [L1].

F2L1step 1.1step 1.2

3.1

By [L1], equality of the two colimit classes is equivalence under that relation. Step 2.1 identifies this with the existence of the displayed common stage, proving both directions of the biconditional.

L1step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Filtered colimits commute with finite limits in Set

Statement

For every small filtered category $J$ and finite category $K$ , and every $D : J \times K \to S e t$ , the canonical comparison

${colim}_{j} \lim_{k} D (j, k) ⟶ \lim_{k} {colim}_{j} D (j, k)$

is a bijection. This includes the empty finite limit.

Facts & Assumptions

Given: The categories and diagram in the statement.

[F1]

Filteredness combines finitely many objects at a common later stage and coequalizes finitely many parallel arrows (Filtered categories and filtered colimits).

[L1]

Equality of two elements in a filtered Set-colimit occurs at one common later stage (Two representatives in a filtered colimit of sets are equal exactly when they become equal at one common later stage).

[L2]

Set-limits are compatible tuples and Set-colimits are tagged quotients (Set has all small limits, realized as compatible tuples in a set-indexed product, Set has all small colimits, realized as a quotient of a set-indexed disjoint union).

[L3]

Finite limits can be tested using finite products and equalizers (Finite, nonempty finite, and connected finite (co)limit criteria in terms of products, equalizers, pullbacks, terminal objects, and their duals).

[L4]

A canonical comparison is invertible exactly when the limit is preserved (A functor preserves a chosen limit exactly when its canonical comparison to the chosen target limit is an isomorphism, and dually for colimits).

Proof

technique · representatives

1.1

By [L3], it suffices to prove that a filtered colimit preserves finite products and equalizers. For a finite product, a tuple on the right has finitely many coordinates, each represented at some stage. Repeated use of [F1] moves all representatives to one common stage, producing a tuple there. Thus the comparison is surjective.

F1L2L3

1.2

If two common-stage tuples have the same image, [L1] makes each coordinate equal at some later stage. There are finitely many coordinates, so repeated use of [F1] moves all those equalities to one stage. The tuples then agree, which proves injectivity.

F1L1L2

1.3

For an equalizer, an element on the right is represented by $x$ at some stage and its two images become equal in the filtered colimit. By [L1], after moving $x$ to one later stage its two images are equal there, so it is represented by a stagewise equalizer element. This proves surjectivity.

L1L2

1.4

If two stagewise equalizer elements become equal in the ambient filtered colimit, [L1] makes them equal at a common later stage; functoriality keeps them inside the later equalizer. This proves injectivity.

L1L2

1.5

For the empty product, each stage and the target are singletons. The filtered category is nonempty by [F1], so the colimit of the constant singleton diagram is a singleton, not empty.

F1L2

2.1

Steps 1.1 to 1.5 make every finite-limit comparison bijective. By [L4], filtered colimits preserve finite limits, proving the displayed assertion.

L3L4step 1.1step 1.2step 1.3step 1.4step 1.5∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Final and initial functors via nonempty connected comma categories

Definition

Let $u : A \to B$ be a functor (Covariant functor, identity functor, composite functor, and contravariant functor). It is final when, for every $b \in B$ , the comma category $(b ↓ u)$ (Comma category, slice category, and coslice category) is nonempty and connected in the finite-zigzag sense of Isomorphism, groupoid, and connected category. Its objects are pairs $(a, β : b \to u (a))$ .

The functor $u$ is initial when $u^{o p} : A^{o p} \to B^{o p}$ is final (Opposite category $C^{o p}$ ). Equivalently, every $(u ↓ b)$ is nonempty and connected. Some sources call a final functor cofinal.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Assuming Choice, precomposition with a final functor does not change colimits, and precomposition with an initial functor does not change limits

Statement

Assume Choice. Let $u : A \to B$ be final between small categories and let $F : B \to C$ . Then $F$ has a colimit if and only if $F u$ has a colimit, and in that event the canonical map

${colim}_{a \in A} F (u (a)) ⟶ {colim}_{b \in B} F (b)$

is an isomorphism. Dually, restriction along an initial functor does not change limits.

Facts & Assumptions

Given: The final functor $u$ and diagram $F$ in the statement.

[F1]

Finality means every $(b ↓ u)$ is nonempty and connected (Final and initial functors via nonempty connected comma categories).

[F2]

A colimit is an initial cocone, characterized by a unique map to every cocone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[L1]

Two colimits are uniquely compatibly isomorphic (Any two limits, or any two colimits, of one diagram are uniquely isomorphic compatibly with their structure maps).

[F3]

Choice selects one object from every member of a set-indexed family of nonempty sets (The Axiom of Choice).

[L2]

Initiality and limits are dual to finality and colimits (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · identify cocones

1.1

Restriction sends a cocone $ρ_{b} : F (b) \to X$ to $ρ_{u (a)} : F (u (a)) \to X$ . Conversely, from a cocone $λ$ over $F u$ , use [F1] and [F3] to choose for each $b$ an object $(a_{b}, β_{b} : b \to u (a_{b}))$ and put ${\overset{ˉ}{λ}}_{b} = λ_{a_{b}} F (β_{b})$ .

F1F3

1.2

If $h : (a, β) \to (a^{'}, β^{'})$ is a comma morphism, then $u (h) β = β^{'}$ and the cocone equation gives $λ_{a^{'}} F (β^{'}) = λ_{a} F (β)$ . A finite zigzag therefore proves that ${\overset{ˉ}{λ}}_{b}$ is independent of the chosen comma object.

F1given

2.1

For $r : b \to b^{'}$ , choose a comma object $(a, β : b^{'} \to u (a))$ for $b^{'}$ . Then $(a, β r)$ is one for $b$ , so step 1.2 gives ${\overset{ˉ}{λ}}_{b} = {\overset{ˉ}{λ}}_{b^{'}} F (r)$ . Thus $\overset{ˉ}{λ}$ is a cocone over $F$ .

step 1.2

3.1

Restricting $\overset{ˉ}{λ}$ at $u (a)$ and using $(a, 1_{u (a)})$ returns $λ_{a}$ . Extending the restriction of $ρ$ returns $ρ_{b}$ by its cocone equation. Hence restriction is a bijection between cocones over $F$ and over $F u$ , natural in their apex.

step 1.1step 1.2step 2.1

4.1

By [F2], an initial object represents either naturally identical cocone assignment exactly when it represents the other. Thus either colimit exists if and only if the other does. When both are chosen, [L1] identifies the induced canonical map as their unique compatible isomorphism.

F2L1step 3.1

5.1

Applying [L2] to steps 1.1 to 2.1 replaces $(b ↓ u)$ by the comma categories for an initial functor and proves the limit assertion, including both directions of existence.

L2step 1.1step 1.2step 2.1step 3.1step 4.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Grp is complete and cocomplete

Statement

The category $G r p$ of groups and group homomorphisms has all small limits and all small colimits.

Facts & Assumptions

Given: A set-indexed family of groups or a parallel pair of group homomorphisms.

[L1]

A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers (A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers).

[F1]

Groups and homomorphisms form $G r p$ , and homomorphisms preserve the group operation and identity (Groups and group homomorphisms form the large locally small category $G r p$ , Monoid homomorphism and group homomorphism).

[F2]

The free group on a set has the unique homomorphic extension property (Free group on a set of generators).

[F3]

The normal closure is the least normal subgroup containing a subset (The normal closure of a subset of a group).

[L2]

A homomorphism out of $G / N$ exists uniquely precisely when the original homomorphism kills $N$ (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

Proof

technique · explicit constructions and the criteria

1.1

For groups $(G_{i})_{i \in I}$ , the Cartesian product with componentwise multiplication and inverse is a group. Coordinate projections are homomorphisms, and the unique set-theoretic pairing of a family of homomorphisms is componentwise a homomorphism. This gives every small product, including the one-element group for $I = \emptyset$ .

F1algebra

1.2

For $f, g : G ⇉ H$ , the subset $E = {x \in G : f (x) = g (x)}$ is a subgroup. Its inclusion is an equalizer because an equalizing homomorphism has image in $E$ and corestricts uniquely. Thus [L1] gives completeness.

F1L1

1.3

For a family $(G_{i})$ , let $S = ∐_{i} {i} \times ∣ G_{i} ∣$ , take the free group $F (S)$ , and quotient by the normal closure $N$ of the elements imposing $[i, 1] = 1$ and $[i, x y] = [i, x] [i, y]$ . The maps $G_{i} \to F (S) / N$ , $x \mapsto [i, x] N$ , are homomorphisms.

F2F3algebra

1.4

For $f, g : G ⇉ H$ , let $N$ be the normal closure of ${f (x) g (x)^{- 1} : x \in G}$ . The quotient $q : H \to H / N$ satisfies $q f = q g$ . If $h : H \to K$ equalizes $f, g$ , it kills those generators and their normal closure, so [L2] gives a unique factor through $q$ . Thus $q$ is a coequalizer.

F3L2algebra

2.1

Given homomorphisms $h_{i} : G_{i} \to H$ , [F2] extends the tagged function to a unique $F (S) \to H$ . It kills every defining relation, hence $N$ , so [L2] factors it uniquely through $F (S) / N$ . Conversely any factor restricts to the $h_{i}$ . This proves the coproduct existence and uniqueness clauses, including the empty family, where the free group is trivial.

F2F3L2step 1.3

3.1

Steps 1.3, 2.1, and 1.4 give all small coproducts and coequalizers. The dual half of [L1] therefore gives cocompleteness.

L1step 2.1step 1.4∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Top is complete and cocomplete, and its underlying-set functor preserves all small limits and colimits

Statement

The category $T o p$ has all small limits and colimits. The underlying set functor $U : T o p \to S e t$ preserves every small limit and every small colimit.

Facts & Assumptions

Given: A small diagram $D : J \to T o p$ .

[L1]

The underlying Set-diagram has a limit and a colimit (Set has all small limits, realized as compatible tuples in a set-indexed product, Set has all small colimits, realized as a quotient of a set-indexed disjoint union).

[F1]

Topological spaces and continuous maps form $T o p$ (Topological spaces and continuous maps form the large locally small category $T o p$ ).

[F2]

For the initial topology of a family $(f_{i} : X \to Y_{i})$ , a function $h : Z \to X$ is continuous exactly when every $f_{i} \circ h$ is continuous; dually, for the final topology of a family $(g_{i} : Y_{i} \to X)$ , a function $h : X \to Z$ is continuous exactly when every $h \circ g_{i}$ is continuous (Characteristic properties: a map into a space with the initial topology is continuous iff every composite with the defining family is, a map out of a space with the final topology is continuous iff every composite with the defining family is, and the two topologies are respectively the coarsest and the finest making that family continuous, claims 2 and 4). The topologies themselves are constructed in The initial topology of a family of maps into spaces and the final topology of a family of maps out of spaces, and the subspace topology as the model initial topology, which states these characteristic properties are proved separately.

[F3]

Continuity means inverse images of open sets are open (Continuity of a map of topological spaces at a point and globally).

[F4]

Preservation means that the image of a limiting or colimiting cone is again limiting or colimiting (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

Proof

technique · lift the Set constructions by universal topologies

1.1

Let $(L, p_{j})$ be the Set-limit of $U D$ from [L1]. Give $L$ the initial topology induced by all $p_{j} : L \to U (D (j))$ . Then every $p_{j}$ is continuous and the Set cone equations make it a cone in $T o p$ .

L1F1F2

1.2

Let $(Q, i_{j})$ be the Set-colimit of $U D$ and give $Q$ the final topology induced by all $i_{j} : U (D (j)) \to Q$ . A function $f : Q \to X$ is continuous exactly when every $f i_{j}$ is continuous. Set-universality therefore proves existence and uniqueness of the continuous factor for every Top-cocone. Thus $Q$ is a Top-colimit.

L1F2F3

2.1

For a cone of continuous maps $f_{j} : X \to D (j)$ , Set-universality gives a unique function $f : X \to L$ with $p_{j} f = f_{j}$ . By the characteristic property in [F2], $f$ is continuous exactly because all $p_{j} f$ are continuous. Its uniqueness as a continuous map follows from uniqueness as a function. Hence this is a Top-limit.

L1F2F3step 1.1

3.1

In steps 1.1 and 1.2 the underlying sets, legs, and mediating functions are exactly the Set-limit and Set-colimit data. Applying $U$ removes only the topologies, so both canonical comparisons are identity bijections. By [F4], $U$ preserves all the small limits and colimits.

F4step 1.1step 2.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

For every ring R, the category R-Mod is complete and cocomplete

Statement

For every ring $R$ , the category $R - M o d$ of left $R$ -modules and $R$ -linear maps has all small limits and all small colimits.

Facts & Assumptions

Given: A fixed ring $R$ .

[L1]

Small products and equalizers characterize completeness, and small coproducts and coequalizers characterize cocompleteness (A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers).

[F1]

Left modules and their homomorphisms form $R - M o d$ and obey the module and linearity axioms (Left modules over a fixed ring and module homomorphisms form the large locally small category $R - M o d$ , Unital left and right modules over a ring; unqualified module means left module, Module homomorphism and isomorphism, kernel, image and cokernel).

[F2]

Submodules are closed under addition, inverses, and scalar multiplication (Submodule of a module).

[F3]

A subset $B \subseteq M$ is a basis when every element of $M$ has a unique expression as a finite $R$ -linear combination of elements of $B$ , and a module possessing a basis is free (Generated submodule, cyclic and finitely generated modules, module basis and free module). This supplies the definition only; the free module on a set and its extension property are constructed in step 1.4 below.

[F4]

Quotients by submodules are modules, and a linear map factors uniquely through the quotient precisely when it kills that submodule (Quotient module $M / N$ with scalar multiplication on additive cosets, A module homomorphism vanishing on $N$ factors uniquely through $M / N$ ).

Proof

technique · explicit constructions and the criteria

1.1

A set-indexed Cartesian product of left $R$ -modules, with componentwise addition and scalar multiplication, is a module. Coordinatewise pairing gives its product universal property. The empty product is the zero module.

F1algebra

1.2

For parallel linear maps $f, g : M ⇉ N$ , their agreement set is $\ker (f - g)$ and is a submodule by [F1] and [F2]. Corestriction through its inclusion gives the equalizer universal property. Hence [L1] gives completeness.

F1F2L1

1.3

For $f, g : M ⇉ N$ , quotient $N$ by the submodule generated by ${f (m) - g (m) : m \in M}$ . The quotient map equalizes $f, g$ , and [F4] says every equalizing linear map factors through it uniquely. Thus this is a coequalizer.

F2F4

1.4

For a set $S$ , let $R^{(S)}$ be the set of functions $λ : S \to R$ vanishing outside some finite subset, with pointwise addition and scalar multiplication; these are again finitely supported, so [F1] makes $R^{(S)}$ a left $R$ -module. For $s \in S$ let $e_{s}$ take the value $1$ at $s$ and $0$ elsewhere. Each $λ$ is the finite sum $\sum_{s} λ (s) e_{s}$ over its support, and evaluating any such expression at a point of $S$ returns its coefficient there, so the expression is unique; hence ${e_{s} : s \in S}$ is a basis and $R^{(S)}$ is free in the sense of [F3]. Given a left $R$ -module $P$ and any function $g : S \to P$ , the assignment $λ \mapsto \sum_{s} λ (s) g (s)$ , summed over the finite support, is $R$ -linear by [F1] and sends $e_{s}$ to $g (s)$ ; and any linear map agreeing with $g$ on every $e_{s}$ agrees with it on every finite $R$ -combination of the $e_{s}$ , hence everywhere. So a linear map out of $R^{(S)}$ may be prescribed arbitrarily on the basis and is determined by that prescription.

F1F2F3algebra

2.1

For modules $(M_{i})$ , let $S = ∐_{i} {i} \times ∣ M_{i} ∣$ . In the free module $R^{(S)}$ of step 1.4, quotient by the submodule generated by $[i, 0]$ , $[i, x + y] - [i, x] - [i, y]$ , and $[i, r x] - r [i, x]$ . The maps $M_{i} \to R^{(S)} / N$ induced by $x \mapsto [i, x] + N$ are linear.

F2F4step 1.4

3.1

A family of linear maps $M_{i} \to P$ extends uniquely from $S$ to the free module by step 1.4, kills the displayed generators, and therefore factors uniquely through the quotient by [F4]. This is the coproduct universal property. For an empty family, it returns the zero module.

F4step 1.4step 2.1

4.1

Steps 2.1, 3.1, and 1.3 give all small coproducts and coequalizers, so [L1] gives cocompleteness.

L1step 2.1step 3.1step 1.3∎

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A poset category is complete exactly when every small family has an infimum, and cocomplete exactly when every small family has a supremum

Statement

A poset regarded as a category is complete if and only if every set-indexed family has an infimum, including the empty family. It is cocomplete if and only if every set-indexed family has a supremum, including the empty family. Hence it is both complete and cocomplete exactly when it is a complete lattice.

Facts & Assumptions

Given: A poset $P$ regarded as a category.

[F1]

In the associated category, $x \to y$ exists exactly when $x \leq y$ , and there is at most one such arrow (A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps).

[F2]

Products and coproducts have their family-of-arrows universal properties (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[L1]

Products plus equalizers characterize completeness, and coproducts plus coequalizers characterize cocompleteness (A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers).

Proof

technique · translate universal properties into inequalities

1.1

A cone from $x$ to a discrete family $(p_{i})$ is precisely the collection of inequalities $x \leq p_{i}$ . By [F1] and [F2], a product is therefore a lower bound above every lower bound, namely $\inf_{i} p_{i}$ . For the empty family this is a greatest element.

F1F2

1.2

Reversing inequalities, a coproduct is $\sup_{i} p_{i}$ , with the empty coproduct a least element. Coequalizers are identities for the same at-most-one-arrow reason. The dual half of [L1] proves both directions of the cocompleteness equivalence.

F1F2L1

2.1

Parallel arrows in a poset category are equal whenever they exist. The identity of their common domain is consequently an equalizer, since every factor is unique by [F1]. Hence [L1] and step 1.1 prove both directions of the completeness equivalence.

F1L1step 1.1

3.1

Having all set-indexed infima and suprema, including empty ones, is exactly the complete-lattice condition, which proves the last assertion.

step 2.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Assuming Choice, a small category with products or coproducts indexed by the cardinality of its morphism set is a preorder

Statement

Assume Choice. Let $C$ be small and put $κ = ∣ Mor (C) ∣$ . If every constant $κ$ -indexed family has a product, then $C$ is a preorder. The same conclusion follows if every constant $κ$ -indexed family has a coproduct.

Facts & Assumptions

Given: The small category, its morphism cardinal $κ$ , and one of the two product or coproduct hypotheses.

[F1]

A product represents every family of arrows into its factors (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F2]

The cardinality of a small category is the cardinality of its morphism set (Assuming Choice, cardinality of a small category and κ-small diagrams).

[L1]

Cantor's theorem gives $κ < 2^{κ} = ∣ P (κ) ∣$ (Assuming the Axiom of Choice, $2^{κ} = ∣ P (κ) ∣$ , and Cantor's theorem in cardinal form: $κ < 2^{κ}$ ).

[F3]

A preorder is reflexive and transitive, and its associated category has at most one arrow between any two objects (Preorder and monotone map, A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps).

[L2]

Products and coproducts are formal duals (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · cardinality contradiction

1.1

Suppose distinct parallel arrows $f, g : A ⇉ B$ exist, and let $P = B^{κ}$ be a product of the constant $κ$ -family. For each subset $S \subseteq κ$ , [F1] gives a unique $h_{S} : A \to P$ whose $i$ th projection is $f$ when $i \in S$ and $g$ when $i \notin S$ .

F1given

2.1

If $S \neq T$ , choose $i$ in their symmetric difference. The $i$ th composites of $h_{S}$ and $h_{T}$ are $f$ and $g$ in some order, so $h_{S} \neq h_{T}$ . Thus $S \mapsto h_{S}$ injects $P (κ)$ into $Mor (C)$ .

step 1.1given

3.1

By [F2], the codomain has cardinality $κ$ , whereas [L1] says the domain has strictly larger cardinality. This contradiction proves that no distinct parallel arrows exist. Identities and composition already make the object relation reflexive and transitive, so [F3] makes $C$ a preorder.

F2L1F3step 2.1

4.1

Apply [L2] to $C^{o p}$ . Its morphism set has the same cardinality, a $κ$ -indexed coproduct in $C$ is a product there, and being a preorder is unchanged by reversal. This proves the coproduct clause.

F2F3L2step 3.1∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Assuming Choice, every small complete category and every small cocomplete category is a preorder

Statement

Assume Choice. Every small complete category is a preorder, and every small cocomplete category is a preorder.

Facts & Assumptions

Given: A small category $C$ that is complete or cocomplete.

[L1]

If a small category has constant products or coproducts indexed by the cardinality of its morphism set, it is a preorder (Assuming Choice, a small category with products or coproducts indexed by the cardinality of its morphism set is a preorder).

[F1]

Complete categories have every small limit, and cocomplete categories have every small colimit (Finite, small, and large limits and colimits; complete and cocomplete categories).

Proof

technique · direct corollary

1.1

Let $κ = ∣ Mor (C) ∣$ . Since $C$ is small, a discrete category on the set $κ$ is a small indexing category.

given

2.1

If $C$ is complete, [F1] supplies the product of every constant $κ$ -family. The product clause of [L1] makes $C$ a preorder.

F1L1step 1.1

3.1

If $C$ is cocomplete, [F1] instead supplies every constant $κ$ -coproduct, and the coproduct clause of [L1] gives the same conclusion.

F1L1step 1.1∎

Limits and Colimits

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Constant diagrams, cones, cocones, and their morphisms

Definition

Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties

Definition

Any two limits, or any two colimits, of one diagram are uniquely isomorphic compatibly with their structure maps

Statement

Facts & Assumptions

Proof

A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category

Statement

Facts & Assumptions

Proof

Limits of empty diagrams are terminal objects, and colimits of empty diagrams are initial objects

Statement

Facts & Assumptions

Proof

Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations

Definition

Equalizers and coequalizers as limits and colimits of a parallel pair

Definition

Pullbacks and pushouts as limits and colimits of cospans and spans

Definition

Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers

Definition

The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic

Statement

Facts & Assumptions

Proof

Every equalizer is a monomorphism, and every coequalizer is an epimorphism

Statement

Facts & Assumptions

Proof

A pullback of a monomorphism is a monomorphism, and a pushout of an epimorphism is an epimorphism

Statement

Facts & Assumptions

Proof

Pullback and pushout pasting, with cancellation of the square adjacent to the outer edge

Statement

Facts & Assumptions

Proof

Assuming Choice, cardinality of a small category and κ-small diagrams

Definition

Finite, small, and large limits and colimits; complete and cocomplete categories

Definition

A cone over an identity diagram is weakly initial, and the identity diagram has a limit exactly when the category has an initial object

Statement

Facts & Assumptions

Proof

Set has all small limits, realized as compatible tuples in a set-indexed product

Statement

Facts & Assumptions

Proof

Set has all small colimits, realized as a quotient of a set-indexed disjoint union

Statement

Facts & Assumptions

Proof

Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category

Statement

Facts & Assumptions

Proof

Every small colimit can be constructed as a coequalizer between coproducts over the arrows and objects of the index category

Statement

Facts & Assumptions

Proof

A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers

Statement

Facts & Assumptions

Proof

Finite, nonempty finite, and connected finite (co)limit criteria in terms of products, equalizers, pullbacks, terminal objects, and their duals

Statement

Facts & Assumptions

Proof

Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors

Definition

A functor preserves a chosen limit exactly when its canonical comparison to the chosen target limit is an isomorphism, and dually for colimits