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.

✓ 1 result · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Linear Transformations, Rank-Nullity and Quotient Spaces: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

The forward shift on $F^{N}$ is injective but not surjective

Example

Let $F$ be a field and let $F^{N}$ be the vector space of all functions $x : N \to F$ with pointwise operations. Define the forward shift $S : F^{N} \to F^{N}$ by

$(S x) (0) : = 0_{F}, (S x) (σ (n)) : = x (n) (n \in N) .$

Then $S$ is linear and injective, but it is not surjective. Thus the implication “injective linear map implies surjective” fails when finite-dimensionality is removed.

Facts & Assumptions

Given: A field $F$ and the function space $F^{N}$ .

[L1]

Function equality and the vector-space operations on $F^{X}$ are pointwise (The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = {0, 1, \dots, n - 1}$ ).

[L2]

A function $T$ is linear when $T (a u + b v) = a T (u) + b T (v)$ for all scalars and vectors (Linear map between vector spaces over the same field).

[L3]

A function is injective when equal outputs force equal inputs, and it is surjective when every codomain element has a preimage (Injection, surjection, bijection).

[L4]

A field has distinct elements $0_{F} \neq 1_{F}$ . Every natural is either zero or a successor; zero is not a successor; and the successor map is injective (Field, Every nonzero natural number is a successor, The von Neumann naturals form a Peano system).

Proof

technique · direct

1.1

The two displayed clauses define one function $S x : N \to F$ for each $x$ : they specify coordinate $0$ , and every other natural coordinate is a successor.

L1L4construct

2.1

For $a, b \in F$ and $x, y \in F^{N}$ , both $S (a x + b y)$ and $a S x + b S y$ have coordinate $0_{F}$ at $0$ . At a successor $σ (n)$ they both have value $a x (n) + b y (n)$ . Hence the functions are equal pointwise, and $S$ is linear.

step 1.1L1L2

2.2

If $S x = S y$ , then for every $n \in N$ evaluation at $σ (n)$ gives $x (n) = y (n)$ . Thus $x = y$ pointwise, so $S$ is injective.

step 1.1L1L3

2.3

Let $e \in F^{N}$ have $e (0) = 1_{F}$ and $e (n) = 0_{F}$ for $n \neq 0$ . Every $S x$ has value $0_{F}$ at coordinate $0$ , so $S x \neq e$ by $0_{F} \neq 1_{F}$ . Therefore $e$ has no preimage and $S$ is not surjective.

step 1.1L1L3L4

3.1

The preceding three steps show that $S$ is a linear injection which is not a surjection.

step 2.1step 2.2step 2.3∎

Remarks

The ambient space contains all scalar-valued sequences, not only the eventually zero ones.
The reverse shift $L (x) (n) = x (σ (n))$ satisfies $L \circ S$ equal to the identity, while $S \circ L$ need not be the identity; this is orientation and is not used as a dependency.

Sources

Axler, Linear Algebra Done Right, 4th ed., forward-shift exercise in Chapter 3