ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11

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.

Underlying-set and structure-forgetting functors among $G r p$ , $R i n g$ , ${V e c t}_{F}$ , $R - M o d$ , $T o p$ , and $S e t$

Example

Each familiar category of structured objects has an underlying-set functor to $S e t$ . It sends an object to its carrier and a morphism to its underlying function.

Facts & Assumptions

Given: The five standard structured categories named in the example.

[L1]

Sets and functions form $S e t$ (Sets and functions form the large locally small category $S e t$ ).

[L2]

Groups, unital rings, vector spaces, modules, and spaces with their standard morphisms form categories (Groups and group homomorphisms form the large locally small category $G r p$ , Unital rings and unit-preserving ring homomorphisms form the large locally small category $R i n g$ , Vector spaces over a fixed field and linear maps form the large locally small category ${V e c t}_{F}$ , Left modules over a fixed ring and module homomorphisms form the large locally small category $R - M o d$ , Topological spaces and continuous maps form the large locally small category $T o p$ ).

Verification

technique · direct

1.1

For each of the five structured categories in [L2], define $U$ on objects by $U (A) =$ the carrier of $A$ , and define $U (f)$ to be the same ordered-pair relation as the structure-preserving map $f$ , now regarded only as a function.

L1L2

2.1

The underlying function of the identity morphism of $A$ is $1_{U (A)}$ , so $U (1_{A}) = 1_{U (A)}$ .

step 1.1

2.2

Composition in every category in [L2] is composition of the underlying functions. Hence $U (g \circ f) = U (g) \circ U (f)$ .

step 1.1L2

3.1

Thus the underlying-set assignments from $G r p$ , $R i n g$ , ${V e c t}_{F}$ , $R - M o d$ , and $T o p$ to $S e t$ are functors. They forget structure but not the identity and composition laws.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

Emily Riehl, Category Theory in Context, Example 1.3.2 (standard reference, not scraped)

Underlying-set and structure-forgetting functors among GrpGrp, RingRing, VectFVectF​, R-ModR-Mod, TopTop, and SetSet