LemmaStatement: 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.

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].

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∎

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, Lemma 3.7.1 (standard reference, not scraped)