ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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.

Dual numbers compute the tangent spaces of the general and special linear groups

Example

Let $k$ be any field and let $n \geq 1$ . Write $R : = k [x_{i j} : (i, j) \in n \times n]$ for the polynomial ring on the $n^{2}$ indeterminates $x_{i j}$ , let $X : = (x_{i j}) \in M_{n} (R)$ be the generic $n \times n$ matrix, and let $d : = \det (X)$ and $tr (X)$ be its Leibniz determinant and its trace over the commutative ring $R$ . Put $S : = R / (d - 1), T : = R_{d} = S_{d}^{- 1} R, S_{d} : = {d^{m} : m \in N},$ so that $S$ is the quotient by the principal ideal generated by $d - 1$ and $T$ is the principal localisation of $R$ inverting $d$ . Let ${SL}_{n} : = Spec S, {GL}_{n} : = Spec T$ be the affine $k$ -schemes presented by the determinant condition and by the invertibility of the determinant, and let $e$ be the identity point of either scheme, induced by the evaluation $ev (x_{i j}) = (I_{n})_{i j}$ at the identity matrix. Then $T_{e} {GL}_{n} ≅ M_{n} (k), T_{e} {SL}_{n} ≅ {B \in M_{n} (k) : tr (B) = 0},$ where $T_{e}$ denotes the intrinsic Zariski tangent space at the $k$ -point $e$ . These are tangent-space computations only: no Lie bracket and no Lie-algebra structure on either tangent space is asserted or used, and no characteristic, perfectness or reducedness hypothesis is needed.

Facts & Assumptions

Given: A field $k$ and an integer $n \geq 1$ ; the polynomial ring $R = k [x_{i j} : (i, j) \in n \times n]$ on the finite family of $n^{2}$ indeterminates; the generic matrix $X = (x_{i j}) \in M_{n} (R)$ with determinant $d = \det (X)$ and trace $tr (X)$ ; the principal ideal $(d - 1) \subseteq R$ ; the quotient $S = R / (d - 1)$ with coset map $π : R \to S$ ; the multiplicative set $S_{d} = {d^{m} : m \in N}$ and the principal localisation $T = R_{d} = S_{d}^{- 1} R$ with localisation map $λ : R \to T$ ; the affine $k$ -schemes ${SL}_{n} = Spec S$ and ${GL}_{n} = Spec T$ ; the evaluation homomorphism $ev : R \to k$ with $ev (x_{i j}) = (I_{n})_{i j}$ ; the dual-number ring $D = k [ϵ] / (ϵ^{2})$ with reduction $ρ : D \to k$ sending $ϵ$ to zero; and the identity matrix $I_{n} \in M_{n} (k)$ .

[F1]

Tangent vectors at rational points are dual-number points: for a $k$ -scheme $X$ and a $k$ -rational point $x \in X (k)$ , the intrinsic tangent space $T_{x} X$ is naturally isomorphic, as a $k$ -vector space, to the fibre over $x$ of the based dual-number points ${Hom}_{k} (Spec D, X) \to X (k)$ , and equivalently to ${Der}_{k} (O_{X, x}, k)$ ; the bijection writes a local $k$ -algebra map as $a \mapsto a (x) + ϵ D (a)$ .

[F2]

The affine scheme of dual numbers: the dual-numbers scheme is $D_{k} = Spec (k [ϵ] / (ϵ^{2}))$ , whose class $ϵ$ is nilpotent; thus $D = k [ϵ] / (ϵ^{2})$ is a commutative $k$ -algebra in which every element has a unique form $c + ϵ b$ with $c, b \in k$ , and $ϵ^{2} = 0$ .

[F3]

Schemes and morphisms over a base: a $k$ -morphism is a morphism commuting with the structure maps to $Spec k$ .

[F4]

Affine schemes are contravariantly equivalent to commutative rings: ring maps between commutative rings correspond contravariantly to morphisms of affine schemes, so $k$ -algebra maps $A \to k$ are the $k$ -points of $Spec A$ .

[F5]

Universal property of a polynomial ring on an arbitrary family of indeterminates: a ring homomorphism $R_{0} \to S_{0}$ and a family $(s_{i})$ in $S_{0}$ determine a unique ring homomorphism $R_{0} [x_{i} : i \in I] \to S_{0}$ restricting to it and sending $x_{i} \mapsto s_{i}$ .

[F6]

A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring: a ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring.

[F7]

Universal property of localisation: maps that invert $S$ factor uniquely through $S^{- 1} R$ : a unital homomorphism $f : R_{0} \to A$ of commutative rings that sends every element of a multiplicative subset $S_{0}$ to a unit factors uniquely as $\tilde{f} \circ λ_{S_{0}}$ through $S_{0}^{- 1} R_{0}$ , with $\tilde{f} (r / s) = f (r) f (s)^{- 1}$ .

[F8]

The quotient ring $R / I$ with $(r + I) (s + I) = r s + I$ : the quotient ring $R_{0} / I$ is formed from the additive cosets $r + I$ with $(r + I) (s + I) = r s + I$ , so the coset map $R_{0} \to R_{0} / I$ is a surjective ring homomorphism.

[F9]

Principal localisation $R_{f} = {1, f, f^{2}, \dots}^{- 1} R$ : for $f \in R_{0}$ the powers $S_{f} = {1, f, f^{2}, \dots} = {f^{n} : n \in N}$ form a multiplicative subset, the principal localisation is $R_{f} = S_{f}^{- 1} R_{0}$ , and its elements may be written $r / f^{n}$ .

[F10]

The ideal generated by a subset and principal ideals: for a subset $S_{0}$ of a ring, $(S_{0})$ is the smallest two-sided ideal containing it, and for an element $a$ the ideal $({a})$ is written $(a)$ and called principal.

[F11]

Finite rectangular matrices over a commutative ring, their entries, rows and columns: an $m \times n$ matrix over a commutative ring is a function $m \times n \to R_{0}$ with value $a_{i j}$ at $(i, j)$ , and $M_{n} (R_{0}) : = M_{n \times n} (R_{0})$ .

[F12]

Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose: matrices are added and scaled entrywise, $(A B)_{i k} = \sum_{j < n} a_{i j} b_{j k}$ , the identity matrix $I_{n}$ has entry $1$ on the diagonal and $0$ elsewhere, and transpose is $(A^{T})_{j i} = a_{i j}$ .

[F13]

The trace of a square matrix over a commutative ring: the trace of $A = (a_{i j}) \in M_{p} (R_{0})$ is ${tr}_{R} (A) = \sum_{i < p} a_{i i}$ , the empty sum being $0$ .

[F14]

For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix: for $n \geq 1$ and a commutative ring $R_{0}$ the determinant is the finite Leibniz sum $\det (A) = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} a_{σ (i), i}$ , the signs acting through the ring identities.

[F15]

The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring: over every commutative ring and $n \geq 1$ the Leibniz determinant is column-multilinear, alternating and normalized.

[F16]

Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring: column-multilinear means additive and scalar-compatible in each selected column with the other columns fixed; alternating means vanishing whenever two columns are equal; normalized means the value $1$ at $I_{n}$ .

[F17]

Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products: over a commutative ring, matrix multiplication is associative, $I_{n}$ is a two-sided identity, and multiplication distributes over addition on both sides.

[F18]

Invertible square matrices and similarity over a commutative ring: a matrix $A \in M_{n} (R_{0})$ is invertible when there is $B$ with $A B = I_{n} = B A$ , the inverse is unique, and the general linear group over $R_{0}$ is the set of such matrices.

[F19]

An invertible square matrix over a commutative ring has unit determinant: for $n \geq 1$ , if $A \in M_{n} (R_{0})$ is invertible over the commutative ring $R_{0}$ , then $\det (A)$ is a unit of $R_{0}$ , and $\det (A^{- 1})$ is its inverse.

[F20]

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: the units of a commutative ring form a group under multiplication, so products of units are units and inverses are unique.

[F21]

Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring: every field is a commutative ring with $1 \neq 0$ .

[F22]

Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ : a ring homomorphism is additive and multiplicative and sends $1$ to $1$ , hence preserves finite sums, finite products and the values of the determinant and trace polynomials.

Verification

technique · direct

1.1givenF5F8F10F11F13F14F15F16F21F22algebra

Setup at the identity: $k$ is a commutative ring [F21], so $R$ is a commutative $k$ -algebra on which the family $(x_{i j})$ is tautological; the generic matrix $X = (x_{i j})$ and its Leibniz determinant $d = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} x_{σ (i), i}$ and trace $tr (X) = \sum_{i < n} x_{i i}$ are elements of $R$ [F11, F13, F14]; $S = R / (d - 1)$ is the quotient by the principal ideal generated by $d - 1$ [F8, F10]; the evaluation $ev : R \to k$ with $ev (x_{i j}) = (I_{n})_{i j}$ exists and is the unique such $k$ -algebra map [F5]; and $ev (d) = \det (I_{n}) = 1$ , because $ev$ , being a unital ring homomorphism [F22], sends the finite Leibniz sum of monomials in the indeterminates to the same sum evaluated at the entries of $I_{n}$ [F14], and the Leibniz determinant is normalized [F15, F16]; consequently $ev (d - 1) = 0$ , $ev (d^{m}) = 1$ for every $m \in N$ , and $d \neq 0$ because $ev (d) = 1 \neq 0$ .

1.2givenF1F3F4F6F7F9F20F22algebra

The identity points: the quotient universal property [F6] applied to $ev$ and the ideal $(d - 1)$ gives a unique ring homomorphism $e_{S} : S \to k$ with $e_{S} \circ π = ev$ ; the localisation universal property [F7] applied to $ev$ and the multiplicative set $S_{d}$ [F9] gives a unique ring homomorphism $e_{T} : T \to k$ with $e_{T} \circ λ = ev$ , its hypothesis holding because $ev (d^{m}) = ev (d)^{m} = 1$ is a unit of $k$ for every $m$ [F20]; both are $k$ -algebra maps, since the $k$ -algebra structures of $S$ and $T$ are induced by $k \to R$ followed by $π$ and $λ$ and $e_{S} \circ π = ev = e_{T} \circ λ$ restricts to the identity on $k$ [F22]; by the anti-equivalence [F4] these $k$ -algebra maps $S \to k$ and $T \to k$ are $k$ -points $e$ of ${SL}_{n}$ and of ${GL}_{n}$ , the identity points of the two schemes, and $T_{e}$ denotes the intrinsic tangent space at these points [F1, F3].

1.3givenF2F11F12F13F15F16algebra

The determinant of $I_{n} + ϵ B$ : fix $B \in M_{n} (k)$ and put $Y : = I_{n} + ϵ B \in M_{n} (D)$ , so that $Y_{i j} = (I_{n})_{i j} + ϵ b_{i j}$ by the entrywise rules [F2, F11, F12]; the $j$ -th column of $Y$ is the sum of the $j$ -th standard basis column $e_{j}$ of $I_{n}$ and the $ϵ$ -multiple of the $j$ -th column $B^{(j)}$ of $B$ ; iterating the column-additivity of the determinant through the $n$ columns [F15, F16] and discarding every term containing the factor $ϵ^{2} = 0$ [F2] gives $\det (Y) = \det (I_{n}) + ϵ \sum_{j < n} \det (A_{j})$ , where $A_{j}$ is obtained from $I_{n}$ by replacing column $j$ by $B^{(j)}$ ; expanding $B^{(j)} = \sum_{i < n} b_{i j} e_{i}$ in that column by column-additivity [F15, F16], every term with $i \neq j$ has the column $e_{i}$ occurring twice and has determinant $0$ by alternation, while the term $i = j$ is $I_{n}$ and has determinant $1$ by normalization [F15, F16]; therefore $\det (A_{j}) = b_{j j}$ and $\det (I_{n} + ϵ B) = 1 + ϵ tr (B)$ with $tr (B) = \sum_{j < n} b_{j j}$ [F13]; replacing $B$ by $- B$ and using the entrywise identity $tr (- B) = - tr (B)$ gives $\det (I_{n} - ϵ B) = 1 - ϵ tr (B)$ .

2.1step 1.3F2F17F18F19algebra

The determinant of $I_{n} + ϵ B$ is a unit: by associativity, distributivity and the identity laws for matrices over the commutative ring $D$ [F17], $(I_{n} + ϵ B) (I_{n} - ϵ B) = I_{n} + ϵ B - ϵ B - ϵ^{2} B^{2} = I_{n}$ , because $ϵ^{2} = 0$ [F2]; hence $I_{n} + ϵ B$ is invertible in $M_{n} (D)$ with inverse $I_{n} - ϵ B$ [F18]; the invertible-matrix corollary [F19] then makes $\det (I_{n} + ϵ B)$ a unit of $D$ whose inverse is $\det (I_{n} - ϵ B)$ , so by step 1.3 the element $1 + ϵ tr (B)$ is a unit of $D$ with inverse $1 - ϵ tr (B)$ , for every $B \in M_{n} (k)$ .

2.2F1F2F3F4F5F6F11F12F14F22step 1.2step 1.3algebra

The tangent space of ${SL}_{n}$ : by [F1] applied to the $k$ -scheme ${SL}_{n}$ and its $k$ -point $e$ of step 1.2, $T_{e} {SL}_{n}$ is $k$ -linearly isomorphic to the based dual-number points, that is to the $k$ -algebra maps $φ : S \to D$ with $ρ \circ φ = e_{S}$ [F2, F3, F4]; by the quotient universal property [F6] such $φ$ correspond bijectively to the $k$ -algebra maps $ψ : R \to D$ with $ρ \circ ψ = ev$ and $ψ (d - 1) = 0$ ; by the polynomial universal property [F5] such $ψ$ correspond bijectively to families $(y_{i j}) \in D^{n \times n}$ , that is to matrices $Y \in M_{n} (D)$ [F11], and $ψ (d) = \det (Y)$ because $ψ$ is a unital ring homomorphism [F22] applied to the Leibniz formula [F14]; the reduction condition says that $y_{i j}$ has constant term $(I_{n})_{i j}$ , so by the unique form $c + ϵ b$ of elements of $D$ [F2] one has $Y = I_{n} + ϵ B$ for a unique $B \in M_{n} (k)$ [F11, F12]; the condition $ψ (d - 1) = 0$ says $\det (Y) = 1$ , which by step 1.3 reads $1 + ϵ tr (B) = 1$ , equivalently $ϵ tr (B) = 0$ , equivalently $tr (B) = 0$ by the uniqueness of that form [F2]; the assignment $B \mapsto φ_{B}$ is $k$ -linear, since $ϵ (b + b^{'}) = ϵ b + ϵ b^{'}$ and $ϵ (c b) = c ϵ b$ in $D$ [F2], so under the $k$ -linear isomorphism of [F1] we obtain $T_{e} {SL}_{n} ≅ {B \in M_{n} (k) : tr (B) = 0}$ , both directions being proved: every based dual-number point yields such a $B$ , and every such $B$ yields a based dual-number point.

3.1F1F2F3F4F5F7F11F12F14F20F22step 1.2step 1.3step 2.1step 2.2algebra

The tangent space of ${GL}_{n}$ : by [F1] applied to the $k$ -scheme ${GL}_{n}$ and its $k$ -point $e$ of step 1.2, $T_{e} {GL}_{n}$ is $k$ -linearly isomorphic to the based dual-number points, that is to the $k$ -algebra maps $φ : T \to D$ with $ρ \circ φ = e_{T}$ [F2, F3, F4]; by the localisation universal property [F7] such $φ$ correspond bijectively to the $k$ -algebra maps $ψ : R \to D$ with $ρ \circ ψ = ev$ and $ψ (d)$ a unit of $D$ , the further conditions that each $ψ (d^{m}) = ψ (d)^{m}$ be a unit being automatic because units form a group [F20]; as in step 2.2 such $ψ$ correspond bijectively to the matrices $Y = I_{n} + ϵ B$ with $B \in M_{n} (k)$ unique [F5, F11, F12], and $ψ (d) = \det (Y) = 1 + ϵ tr (B)$ [F14, F22, step 1.3], which by step 2.1 is a unit of $D$ for every $B \in M_{n} (k)$ , with the explicit inverse $1 - ϵ tr (B)$ ; hence the unit condition excludes no matrix and the correspondence is a $k$ -linear isomorphism $T_{e} {GL}_{n} ≅ M_{n} (k)$ , the inverse of $1 + ϵ tr (B)$ being exhibited explicitly.

4.1F1step 2.1step 2.2step 3.1

Conclusion: for every field $k$ and every $n \geq 1$ , the identity point $e$ of ${SL}_{n} = Spec (k [x_{i j}] / (\det (X) - 1))$ has $T_{e} {SL}_{n} ≅ {B \in M_{n} (k) : tr (B) = 0}$ , the trace-zero matrices, and the identity point of ${GL}_{n} = Spec (k [x_{i j}]_{\det})$ has $T_{e} {GL}_{n} ≅ M_{n} (k)$ , the full matrix space; the zero matrix corresponds to the identity map $ψ = ev$ in both computations, so it is the zero tangent vector, and no Lie bracket, Lie-algebra structure, characteristic hypothesis or choice principle is involved.

5.1F2F13F20step 1.1step 1.3step 2.1step 2.2step 3.1∎

Boundary and scope dispositions: neither scheme is empty and no list here is empty, because $n \geq 1$ makes $n \times n$ nonempty, the identity matrix $I_{n}$ exists, step 1.2 exhibits the $k$ -points $e$ , and the families $(x_{i j})$ , $(y_{i j})$ and the generating list ${d - 1}$ of the principal ideal are nonempty (steps 1.1 and 1.2); the zero cases are the zero matrix $B = 0$ , which gives $ψ = ev$ with $\det (I_{n}) = 1$ and $tr (0) = 0$ by [F13], the vanishing $ev (d - 1) = 0$ of step 1.1, and the zero element of $M_{n} (k)$ , while $M_{n} (k)$ is nonzero for every $n \geq 1$ , and the trace-zero space is zero for $n = 1$ and nonzero for $n \geq 2$ (it contains the nonzero off-diagonal matrix unit $E_{01}$ ); there is one determinant $d$ , one equation $d - 1$ , one localisation $T = R_{d}$ , one trace functional and one correspondence per scheme, each with two directions (steps 2.2 and 3.1); the degenerate cases are handled: characteristic plays no role because the expansion of step 1.3 uses only $ϵ^{2} = 0$ and never divides by an integer [F2], the matrix $B$ itself need not be invertible although $I_{n} + ϵ B$ always is, and when $tr (B) \neq 0$ the element $1 + ϵ tr (B)$ is a unit different from $1$ with inverse $1 - ϵ tr (B)$ [F20], so the trace-zero condition is strict; the endpoints are $n = 1$ , where ${GL}_{1} = Spec (k [x]_{x})$ has tangent space $M_{1} (k) = k$ and ${SL}_{1} = Spec (k [x] / (x - 1))$ has tangent space ${0}$ because $tr (B) = 0$ forces $B = 0$ , together with the exponent endpoints $d^{0} = 1$ and the general power $d^{m}$ in $S_{d}$ ; both directions of the equivalence $\det (I_{n} + ϵ B) = 1 ⟺ tr (B) = 0$ are proved in step 2.2 and both directions of the factorisation through $T$ are proved in step 3.1; and no Axiom of Choice or dependent choice is used, every map, matrix and unit inverse being exhibited explicitly and every cited supplier being choice-free, with no def-axiom-of-choice dependency declared.

Source qualification

Milne, Algebraic Geometry v6.10, §4j (printed pp. 97–98) introduces the dual-number description of tangent spaces for group varieties given by their points functors. In Example 4.46 the source observes that a matrix $I + ϵ A$ has inverse $I - ϵ A$ in $M_{n} (k [ϵ])$ , so that it lies in ${GL}_{n} (k [ϵ])$ , and concludes $T_{e} ({GL}_{n}) = {I + ϵ A : A \in M_{n}} ≅ M_{n} (k);$ this is exactly the invertibility computation of step 2.1, and the present item records the same fact scheme-theoretically through the localisation condition on the map $ψ$ . In Example 4.47 the source expands $\det (I + ϵ A)$ as a sum of signed products and uses $ϵ^{2} = 0$ to obtain $\det (I + ϵ A) = 1 + ϵ trace (A)$ , hence $T_{e} ({SL}_{n}) ≅ {A \in M_{n} (k) : trace (A) = 0}$ ; the present item reproduces this expansion as the column-multilinear computation of step 1.3 and derives both inclusions from the quotient condition. Arapura, Notes on Basic Algebraic Geometry, Exercise 5.1.4 (printed p. 35) asks for the identity $\det (I + B ϵ) = 1 + trace (B) ϵ$ and the conclusion $T_{I} {SL}_{n} (k) = {B \in {Mat}_{n \times n} (k) : trace (B) = 0}$ ; it is an exercise, so it is cited as a source for the statement and not as a proof. Milne's chapter works with classical varieties over an algebraically closed field and Milne's Aside 4.49 (the Lie bracket on $T_{e} {GL}_{n}$ ) is deliberately not used: the item asserts only the two $k$ -vector-space isomorphisms and infers no bracket. The item adds the affine presentations ${GL}_{n} = Spec (k [x_{i j}]_{\det})$ and ${SL}_{n} = Spec (k [x_{i j}] / (\det (X) - 1))$ over an arbitrary field, the passage to the two universal properties of the quotient and the localisation, and the identification of the based dual-number points with the matrices $I_{n} + ϵ B$ ; no characteristic, perfectness, reducedness or algebraic-closedness hypothesis is used anywhere.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

77 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.