LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

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∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 13 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

E. Riehl, Category Theory in Context, Exercise 3.1.iv (standard reference, not scraped)