ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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 canonical group solution set on a two-element set

Example

For the two-element set $S = {x, y}$ , the canonical solution set for the underlying-set functor on groups consists of the maps $S ⟶ U (F (S) / N)$ as $N$ ranges over the normal subgroups of the free group $F (S)$ . For example, the map sending both $x$ and $y$ to the nonidentity element of $Z / 2 Z$ occurs through the quotient by its induced kernel.

Facts & Assumptions

Given: The set $S = {x, y}$ .

[L1]

For every set $S$ , the quotient maps $S \to U (F (S) / N)$ indexed by normal subgroups $N ⊴ F (S)$ form a solution set for the underlying-set functor on groups (Normal-subgroup quotients of a fixed free group give a canonical solution set for the underlying-set functor on groups).

[L2]

For a group homomorphism, the image is a subgroup of the codomain and the kernel is a normal subgroup of the domain (The image of a group homomorphism is a subgroup and its kernel is a normal subgroup).

[L3]

If a homomorphism kills a normal subgroup $N$ , it factors uniquely through the quotient by $N$ (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

Verification

technique · direct

1.1

Apply [L1] to the two-element set $S$ . The normal subgroups of the set-sized group $F (S)$ form a set, so the displayed family is the promised solution set.

2.1

Let $C = Z / 2 Z$ and map both $x$ and $y$ to its nonidentity element. Freeness extends this function uniquely to a homomorphism $\hat{f} : F (S) \to C$ . Its kernel $N = \ker \hat{f}$ is a normal subgroup of $F (S)$ by [L2], so $N$ indexes a member of the family in step 1.1. Since $N \subseteq \ker \hat{f}$ , [L3] gives a unique $\overset{ˉ}{f} : F (S) / N \to C$ with $\hat{f} = \overset{ˉ}{f} q_{N}$ , and $\overset{ˉ}{f}$ is injective because $\overset{ˉ}{f} (g N) = 0$ forces $g \in \ker \hat{f} = N$ . Hence the original map factors through the member indexed by $N$ .

L1L2L3algebra

3.1

More generally, [L1] gives this kernel-quotient factorisation for every map from $S$ into an underlying group, which verifies the solution-set property rather than only listing the quotients.

step 1.1L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 41 results over 13 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

T. Leinster, Basic Category Theory, appendix A (standard reference, not scraped)