ExampleConstruction: Literature-sourcedVerification: 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.

In a poset regarded as a category, products are infima, coproducts are suprema, and equalizers are automatic

Example

In a poset category, a product of a family is its infimum, a coproduct is its supremum, and for any parallel pair the identity of its domain is an equalizer while the identity of its codomain is a coequalizer.

Facts & Assumptions

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

[F1]

An arrow $x \to y$ means $x \leq y$ , and at most one such arrow exists (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 represent cones and cocones over discrete families (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F3]

Equalizers and coequalizers have their parallel-pair universal properties (Equalizers and coequalizers as limits and colimits of a parallel pair).

Verification

technique · translate arrows into inequalities

1.1

A cone from $x$ to $(p_{i})$ is exactly the assertion $x \leq p_{i}$ for all $i$ . Its unique factor through $p$ says $x \leq p$ for every lower bound $x$ . Thus [F2] is exactly the greatest-lower-bound property.

F1F2

1.2

Reversing all inequalities turns the coproduct property into the least-upper-bound property. The empty cases give the greatest and least elements, respectively.

F1F2

2.1

If $f, g : x ⇉ y$ exist, [F1] gives $f = g$ . Then $1_{x}$ equalizes them and every arrow into $x$ factors through $1_{x}$ uniquely. Dually, $1_{y}$ is a coequalizer.

F1F3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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, Example 3.1.24 (standard reference, not scraped)