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.
The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial
Statement
For a linear map , the sets and are linear subspaces. Moreover, is injective if and only if .
Facts & Assumptions
Given: A linear map of vector spaces over a field .
The kernel and image have the displayed set descriptions (Kernel and image of a linear map).
A nonempty subset is a linear subspace exactly when it is closed under (One-step subspace test: a nonempty is a linear subspace if and only if for all and ).
A linear map carries to , preserves zero, and preserves subtraction (Linear map between vector spaces over the same field, A linear map preserves zero, negatives, and subtraction).
A function is injective when equal outputs have equal inputs (Injection, surjection, bijection).
Proof
The kernel contains by [L3]. If and , then , so .
The image contains . If and , then lies in the image.
If is injective and , then , so and the kernel is trivial.
Conversely, suppose and . Then by [L3], so and .
The subspace criterion proves that both and are linear subspaces.
Thus is injective exactly when its kernel is trivial.
Depends on
- Kernel and image of a linear map
- Linear map between vector spaces over the same field
- One-step subspace test: a nonempty $W \subseteq V$ is a linear subspace if and only if $\lambda u + v \in W$ for all $\lambda \in F$ and $u, v \in W$
- A linear map preserves zero, negatives, and subtraction
- Injection, surjection, bijection
Used by
- Rank and nullity of a linear map with finite-dimensional domain Definition
- Submersions and immersions between Euclidean open sets Definition
- The orthogonal group is a regular level set of dimension n(n-1)/2 Example
- The quotient by the kernel is isometric to the range with its induced quotient norm Example
- A linear functional annihilating the kernel of a surjection is a unique transpose multiple Lemma
- Extending a basis of the kernel to a basis of the domain gives a basis of the image Lemma
- For a subspace U≤ Fⁿ, dim_F U^⊥=n-dim_F U, where U^⊥={x:⟨ x,u⟩=0 for all u∈ U} Lemma
- The quaternion double cover generates the third homotopy group of SO(3) Lemma
- For a finite-dimensional space, λ is an eigenvalue of T if and only if T-λ I is not invertible Proposition
- A linear map T of ℝⁿ sends Lebesgue measurable sets to Lebesgue measurable sets, with λₙ(T[E])=|det T| λₙ(E) when T is invertible and T[E] Lebesgue null when it is not Theorem
- Assuming choice, the canonical map J_V:V→ V^** is linear and injective Theorem
- Complexification preserves kernels, images, finite rank, nullity, and short exact sequences Theorem
- First isomorphism theorem for vector spaces: V/ker T is isomorphic to imT Theorem
- If Ax=b has one solution xₚ, then its full solution set is the affine subspace xₚ+N(A) Theorem
- Invertible matrix theorem: invertibility, full pivot rank, RREF I, trivial nullspace and unique solvability are equivalent Theorem
Cited to discharge well-definedness by Kernel and image of a linear map.
Dependency tree · two levels
11 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
- Axler, Linear Algebra Done Right, Chapter 3 (standard reference, not scraped)