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.

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

Example

For a fixed natural number $n \geq 1$ , 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 \geq 1$ and unit-preserving homomorphisms of commutative rings.

[L1]

Commutative rings form a full subcategory of $R i n g$ , groups form $G r p$ , 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 $R i n g$ , Groups and group homomorphisms form the large locally small category $G r p$ , 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 (m a) = m f (a)$ for $m \in 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 \geq 1$ , 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 (A B) = \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 $φ : R \to S$ , restrict $φ$ 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 $G r p$ .

L1L2

1.2

Put $G_{n} (R) = {GL}_{n} (R)$ and apply $φ$ entrywise. From the product formula, $φ ((A B)_{i k}) = \sum_{j} φ (a_{i j}) φ (b_{j k})$ , 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 $G r p$ .

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 $φ$ to the finite Leibniz sum term by term gives $\det_{S} (G_{n} (φ) (A)) = φ (\det_{R} (A)) = U (φ) (\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 · two levels

49 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

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

For n≥1n≥1, determinant is a natural transformation det⁡:GL⁡n(−)⇒(−)×det:GLn​(−)⇒(−)× from commutative rings to groups