TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

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∎

Depends on

Used by

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

E. Riehl, Category Theory in Context, Proposition 3.7.3 (standard reference, not scraped)