Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16
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.

ker⁡T∗=(im⁡T)⊥ and im⁡T∗=(ker⁡T)⊥ in finite dimension

Statement

For a linear map T:V→W between finite-dimensional inner product spaces,

ker⁡T∗=(im⁡T)⊥,im⁡T∗=(ker⁡T)⊥.

Equivalently, ker⁡T=(im⁡T∗)⊥ and im⁡T=(ker⁡T∗)⊥.

Facts & Assumptions

Given: A finite-dimensional linear map T:V→W.

[L1]

The adjoint identity is ⟨Tv,w⟩=⟨v,T∗w⟩ for all v,w (The adjoint T∗:W→V is characterised by ⟨Tv,w⟩W=⟨v,T∗w⟩V).

[L3]

In finite dimension, U⊥⊥=U for every subspace U (In finite dimension, W⊥⊥=W and dim⁡W+dim⁡W⊥=dim⁡V).

[L4]

A vector lies in U⊥ exactly when it pairs to zero with every vector of U (The orthogonal complement W⊥={v:⟨v,w⟩=0 for all w∈W}).

Proof

technique · direct
1.1L1L4

A vector w∈W lies in ker⁡T∗ exactly when ⟨v,T∗w⟩=0 for every v∈V. By [L1], this is exactly ⟨Tv,w⟩=0 for every v, hence exactly w∈(im⁡T)⊥ by [L4].

2.1step 1.1L2L3

Apply step 1.1 to T∗ and use [L2]: ker⁡T=(im⁡T∗)⊥. Taking orthogonal complements and applying [L3] gives (ker⁡T)⊥=im⁡T∗.

3.1step 1.1L3∎

Taking orthogonal complements in step 1.1 and using [L3] also gives im⁡T=(ker⁡T∗)⊥.

Depends on

Used by

Dependency tree · two levels

13 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