TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29

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.

Complexification preserves kernels, images, finite rank, nullity, and short exact sequences

Statement

Let $T : V \to W$ be a real-linear map. Under the canonical isomorphism of The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic, the complexification acts componentwise: $T_{C} (v + i w) = T v + i T w$ . Consequently

$\ker (T_{C}) = (\ker T) \oplus i (\ker T), im (T_{C}) = (im T) \oplus i (im T),$

the complexifications of the real subspaces. If $V$ and $W$ are finite-dimensional, then ${rank}_{C} (T_{C}) = {rank}_{R} (T)$ and ${nullity}_{C} (T_{C}) = {nullity}_{R} (T)$ . If $0 \to U \overset{i}{\to} V \overset{p}{\to} W \to 0$ is a short exact sequence of real vector spaces, then

$0 ⟶ U_{C} \overset{i_{C}}{\to} V_{C} \overset{p_{C}}{\to} W_{C} ⟶ 0$

is a short exact sequence of complex vector spaces.

Facts & Assumptions

Given: A real-linear map $T : V \to W$ , and in the exactness clause real-linear maps $i : U \to V$ and $p : V \to W$ with $p \circ i = 0$ .

[L1]

The complexification of a real-linear map is $T_{C} (z \otimes v) = z \otimes T (v)$ (Complexification of a real-linear map).

[L2]

The canonical isomorphism $Φ : C \otimes_{R} V \to V \oplus i V$ satisfies $Φ (z \otimes v) = z (v, 0)$ , with inverse $Ψ (v + i w) = 1 \otimes v + i \otimes w$ (The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic).

[L3]

Kernel and image of a linear map are linear subspaces, and a linear map is injective exactly when its kernel is zero (The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial).

[L4]

For a linear map from a finite-dimensional space, $\dim V = nullity T + rank T$ (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[L5]

A short exact sequence is exact at every displayed module, so $im i = \ker p$ at the middle term (Exact sequences and short exact sequences of modules).

[L6]

Complexification of maps respects composition: $(p \circ i)_{C} = p_{C} \circ i_{C}$ (Complexification is a functor on real vector spaces and real-linear maps).

Proof

technique · direct

1.1L1L2algebra

In the direct-sum model, $T_{C} (v + i w) = T v + i T w$ : applying $Φ$ to the formula of [L1], $Φ (T_{C} (1 \otimes v + i \otimes w)) = Φ (1 \otimes T v + i \otimes T w) = T v + i T w$ by [L2].

1.2L2algebra

If $U \leq V$ is a real subspace with real basis $u_{1}, \dots, u_{m}$ , then every element of $U \oplus i U$ is $\sum_{j \leq m} (a_{j} + i b_{j}) u_{j}$ with $a_{j}, b_{j} \in R$ : the real and imaginary components are real combinations of the $u_{j}$ .

1.3L2algebra

The list $u_{1}, \dots, u_{m}$ is complex-linearly independent in $U \oplus i U$ : $\sum_{j} (a_{j} + i b_{j}) u_{j} = 0$ means $(\sum_{j} a_{j} u_{j}, \sum_{j} b_{j} u_{j}) = (0, 0)$ in $V \oplus i V$ , and the real independence of the $u_{j}$ forces every $a_{j} = b_{j} = 0$ .

1.4L6givenalgebra

By [L6] and the hypothesis $p \circ i = 0$ , one has $p_{C} \circ i_{C} = 0$ , hence $im i_{C} \subseteq \ker p_{C}$ .

2.1step 1.1L2L3

$\ker (T_{C}) = {v + i w : T v = T w = 0} = (\ker T) \oplus i (\ker T)$ : the equality of the two descriptions is step 1.1, and by [L3] the kernel of the componentwise map is the complexification of $\ker T$ .

2.2step 1.1L2

$im (T_{C}) = {T v + i T w} = (im T) \oplus i (im T)$ , again directly from step 1.1.

2.3step 1.2step 1.3

For a finite-dimensional real subspace $U$ , steps 1.2 and 1.3 exhibit $u_{1}, \dots, u_{m}$ as a complex basis of $U \oplus i U$ , so $\dim_{C} (U \oplus i U) = \dim_{R} U$ .

3.1step 2.1step 2.2step 2.3L4

Combining steps 2.1, 2.2 and 2.3 gives ${nullity}_{C} (T_{C}) = \dim_{C} \ker (T_{C}) = \dim_{R} \ker T = {nullity}_{R} (T)$ and the matching rank identity, with rank and nullity as in [L4].

3.2step 2.1step 2.2L5

At the middle term, $\ker p_{C} = (\ker p) \oplus i (\ker p) = (im i) \oplus i (im i) = im i_{C}$ by [L5] and steps 2.1 and 2.2 applied to $i$ and $p$ .

3.3step 2.1step 2.2L3

The map $i_{C}$ is injective because $\ker i_{C} = (\ker i) \oplus i (\ker i) = 0$ by [L3], and $p_{C}$ is surjective because $im p_{C} = (im p) \oplus i (im p) = W_{C}$ .

4.1step 1.4step 3.2step 3.3L5

By [L5], exactness of the complexified sequence is: $0 = \ker i_{C}$ at $U_{C}$ , $im i_{C} = \ker p_{C}$ at $V_{C}$ , and $im p_{C} = W_{C}$ at $W_{C}$ ; these are step 3.3, step 3.2 and step 3.3 respectively, with the containment of step 1.4 absorbed into the equality.

5.1step 3.1step 4.1∎

Steps 2.1 and 2.2 prove the kernel and image formulas, step 3.1 the rank and nullity preservation, and step 4.1 the short-exact-sequence clause.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Keith Conrad, Complexification (notes) (standard reference, not scraped)