TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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 power by a set is the product of that many copies and a copower is the coproduct

Statement

Let $M$ be locally small, let $c$ be an object of $M$ and let $S$ be a set. Write $(c)_{s \in S}$ for the constant $S$ -indexed family at $c$ (An indexed family $(A_{i})_{i \in I}$ is a function with domain $I$ ; ${A_{i} : i \in I}$ is its range).

Then the power $c^{S}$ (The power and the copower of an object by a set) exists exactly when the product $\prod_{s \in S} c$ exists (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations), and they are then the same object with the same counit: a power by a set is the product of that many copies. Dually the copower $S \cdot c$ exists exactly when the coproduct $∐_{s \in S} c$ exists, and a copower is the coproduct.

For $S = \emptyset$ the power is a terminal object and the copower an initial object.

Facts & Assumptions

Given: A locally small category $M$ , an object $c$ and a set $S$ .

[F6]

The covariant hom-assignment $M (m, -)$ sends an object to a set of morphisms, and $S e t$ is the category of sets and functions (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, Sets and functions form the large locally small category $S e t$ ).

[F1]

The power $c^{S}$ is the weighted limit of the one-object diagram at the constant weight $S$ , characterised by a bijection $M (m, c^{S}) ≅ S e t (S, M (m, c))$ natural in $m$ ; the copower is characterised dually by $M (S \cdot c, m) ≅ S e t (S, M (c, m))$ (The power and the copower of an object by a set).

[F4]

An indexed family with index set $I$ is a function $A$ with domain $I$ , written $(A_{i})_{i \in I}$ (An indexed family $(A_{i})_{i \in I}$ is a function with domain $I$ ; ${A_{i} : i \in I}$ is its range).

[F2]

A product of $(A_{i})_{i \in I}$ is an object $P$ with projections $p_{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)$ ; a coproduct is dual (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F3]

The empty product is therefore terminal and the empty coproduct initial. (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[F5]

A limit of a diagram is a terminal cone: explicitly, for every cone $(X, ξ)$ there exists a unique morphism $u : X \to L$ such that $λ_{j} u = ξ_{j}$ for every $j$ ; a product is the limit of a family on a discrete index category (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · direct

1.1

By [F1] the power is characterised by a bijection, natural in $m$ , between morphisms $m \to c^{S}$ and functions $S \to M (m, c)$ .

F1F6

2.1

By [F2], [F4] and [F5] the product of the constant family $(c)_{s \in S}$ is characterised by a bijection, natural in $m$ , between morphisms $m \to \prod_{s \in S} c$ and $S$ -indexed families of morphisms $m \to c$ ; and an $S$ -indexed family of elements of the set $M (m, c)$ is by [F4] exactly a function $S \to M (m, c)$ . So the two universal properties are properties of the same functor of $m$ .

F2F4F5step 1.1

3.1

Hence an object represents one exactly when it represents the other, so the power exists exactly when the product does and any object with either property has both; the counit of the power, indexed by $s \in S$ , is the family of projections of the product, since both are obtained by applying the bijection to the identity. The dual argument, with $M (c, m)$ in place of $M (m, c)$ and copairings in place of pairings, identifies the copower with the coproduct of the same constant family.

F1F5step 2.1

4.1

For $S = \emptyset$ the only function $\emptyset \to M (m, c)$ is the empty one, so the bijection of step 1.1 says that $M (m, c^{\emptyset})$ is a one-element set for every $m$ , that is, $c^{\emptyset}$ is terminal; dually $\emptyset \cdot c$ is initial. This agrees with the published convention that The empty product is therefore terminal and the empty coproduct initial.

F3step 3.1∎

Remarks

This is a seam: the power minted on this page is the product already defined in the library, not a second notion, and the theorem is what says so. Every later use of a power may therefore be read as a product of copies, and the notation is a convenience rather than new mathematics.

The empty case is written out because it is where a plausible-looking alternative convention would go wrong. A power by the empty set is terminal, not initial, and a copower by the empty set is initial: the direction is fixed by which side of the hom-set the exponent sits on, and it is fixed the same way as for the published empty product and coproduct.

Depends on

Used by

Powers and copowers of a set by a set Example

Dependency tree · two levels

17 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

G. M. Kelly, Basic Concepts of Enriched Category Theory (TAC Reprints 10), §3.7 (standard reference, not scraped)
F. Loregian, (Co)end Calculus (arXiv:1501.02503v7), Example 2.2.4 (standard reference, not scraped)