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

For $n\ge 1$ , determinant is a natural transformation $\det:\operatorname{GL}_n(-)\Rightarrow(-)^{\times}$ from commutative rings to groups

Example

For a fixed natural number $n\ge1$ , entrywise application of ring homomorphisms makes invertible matrices and units group-valued functors, and determinant is natural between them.

Facts & Assumptions

Given: A natural number $n\ge1$ and unit-preserving homomorphisms of commutative rings.

[L1]

Commutative rings form a full subcategory of $\mathbf{Ring}$ , groups form $\mathbf{Grp}$ , and functors and natural transformations have their usual equations (Subcategory and full subcategory, Commutative ring, Unital rings and unit-preserving ring homomorphisms form the large locally small category $\mathbf{Ring}$ , Groups and group homomorphisms form the large locally small category $\mathbf{Grp}$ , Covariant functor, identity functor, composite functor, and contravariant functor, Natural transformation and its components).

[L2]

Units form a group and ring homomorphisms preserve the ring operations and units (A ring homomorphism satisfies $f(0) = 0$ , $f(-a) = -f(a)$ and $f(ma) = m f(a)$ for $m \in \mathbb{Z}$ , carries units to units, and has a subring as its image; composites of ring homomorphisms are ring homomorphisms, The units of a ring are the invertible elements of its multiplicative monoid, and $R^{\times}$ is a group under multiplication; $0 \in R^{\times}$ only in the zero ring).

[L3]

Matrices, their products and identities, their arithmetic laws, and invertibility over a commutative ring are given by Finite rectangular matrices over a commutative ring, their entries, rows and columns, Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose, Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products, and Invertible square matrices and similarity over a commutative ring.

[L4]

Determinant is given by the Leibniz formula, is multiplicative, and sends invertible matrices to units (For $n\ge1$ , the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix, For same-sized finite square matrices over a commutative ring, $\det(AB)=\det(A)\det(B)$ , An invertible square matrix over a commutative ring has unit determinant).

Verification

technique · direct

1.1

For a commutative ring $R$ , put $U(R)=R^\times$ . For $\varphi:R\to S$ , restrict $\varphi$ to units; it is a group homomorphism because ring homomorphisms preserve products, identities, and inverses. Identity and composition are inherited, so $U$ is a functor to $\mathbf{Grp}$ .

L1L2

1.2

Put $G_n(R)=\operatorname{GL}_n(R)$ and apply $\varphi$ entrywise. From the product formula, $\varphi((AB)_{ik})=\sum_j\varphi(a_{ij})\varphi(b_{jk})$ , so this assignment preserves matrix products and identities and carries an inverse matrix to an inverse matrix. Entrywise identity and composition make $G_n$ a functor to $\mathbf{Grp}$ .

L1L2L3algebra

2.1

Multiplicativity and the unit result in [L4] make $\det_R:G_n(R)\to U(R)$ a group homomorphism.

step 1.1step 1.2L4

2.2

Applying $\varphi$ to the finite Leibniz sum term by term gives $\det_S(G_n(\varphi)(A))=\varphi(\det_R(A))=U(\varphi)(\det_R(A))$ .

step 1.1step 1.2L2L4

3.1

Step 2.2 is the naturality square for every commutative-ring homomorphism. Hence $(\det_R)_R$ defines a natural transformation $G_n\Rightarrow U$ .

step 2.1step 2.2L1∎

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: 112 results over 22 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

Saunders Mac Lane, Categories for the Working Mathematician, Chapter I, section 4, p. 16 (standard reference, not scraped)

For n≥1n\ge 1n≥1, determinant is a natural transformation det⁡:GL⁡n(−)⇒(−)×\det:\operatorname{GL}_n(-)\Rightarrow(-)^{\times}det:GLn​(−)⇒(−)× from commutative rings to groups