Conjugate transpose

The conjugate transpose of a complex matrix combines two familiar moves: flip the matrix across its main diagonal, then replace every complex entry by its complex conjugate. It is commonly written \(A^*\), \(A^\dagger\), or \(A^{\mathrm H}\). This project and Mathlib use the Lean notation Aᴴ.

Start with one complex 2 by 2 matrix

Take

First transpose: exchange row and column positions without changing the scalar values.

Then conjugate each entry. Complex conjugation changes \(i\) to \(-i\), so \(\overline{-3i}=3i\) and \(\overline{2+i}=2-i\):

Entry by entry, the rule is

or, after renaming the two indices,

Both displays say the same thing: the entry moves across the diagonal and is then conjugated.

Transpose, conjugation, and conjugate transpose

The three operations answer different questions.

Transposition and entrywise conjugation commute, so one may conjugate first and transpose second. Keeping the two stages conceptually separate still prevents the most common sign and index mistakes.

For a real matrix, complex conjugation changes nothing. Its conjugate transpose is therefore its ordinary transpose.

Why multiplication order reverses

Suppose \(A\) and \(B\) have compatible dimensions. Then

The reversal is not cosmetic. Acting on a column vector, \(AB\) means apply \(B\) first and \(A\) second:

The adjoint route reverses those stages:

The matrix dimensions enforce the same order. If \(A\) is \(m\) by \(n\) and \(B\) is \(n\) by \(\ell\), then \(B^{\mathrm H}\) is \(\ell\) by \(n\) and \(A^{\mathrm H}\) is \(n\) by \(m\), so \(B^{\mathrm H}A^{\mathrm H}\) is \(\ell\) by \(m\), exactly the shape of \((AB)^{\mathrm H}\). Writing \(A^{\mathrm H}B^{\mathrm H}\) would generally have the wrong intermediate dimensions.

Two other useful identities are

The first says the operation is an involution: applying it twice returns the original matrix.

Hermitian and non-Hermitian boundaries

A matrix is Hermitian precisely when \(A^{\mathrm H}=A\). The running example is not Hermitian. Its upper-right entry is \(A_{12}=2+i\), but the corresponding entry in \(A^{\mathrm H}\) is \(3i\). Equivalently, \(A_{21}=-3i\) is not the conjugate \(2-i\) of \(A_{12}\).

The transformation

does produce a Hermitian matrix. For the example,

The project uses exactly this unnormalized symmetrization for a random matrix . Dividing by two gives the usual Hermitian part over \(\mathbb C\), but that factor is not hidden in the project constructor. In particular, the unnormalized map sends an already Hermitian matrix \(H\) to \(2H\), not to \(H\).

Do not confuse the conjugate transpose with an inverse. The equality \(U^{\mathrm H}=U^{-1}\) is an additional unitary condition, not an identity for every complex matrix.

In Lean

Mathlib’s entrywise theorem is the direct translation of “flip, then conjugate.”

Matrix.conjTranspose_apply A i j : Aᴴ j i = star (A i j)

Try the entry arithmetic locally

The project theorem below uses Mathlib’s general matrix and complex-number interfaces. Before importing those dependencies, a reader can reproduce the opening calculation with integer real-and-imaginary pairs. Save this file as ConjugateTransposeScratch.lean in a scratch directory outside formalization/:

import Std

structure GaussianInt where
  re : Int
  im : Int
  deriving DecidableEq, Repr

def GaussianInt.conj (z : GaussianInt) : GaussianInt :=
  { re := z.re, im := -z.im }

structure Mat2 where
  a11 : GaussianInt
  a12 : GaussianInt
  a21 : GaussianInt
  a22 : GaussianInt
  deriving DecidableEq, Repr

def Mat2.conjTranspose (M : Mat2) : Mat2 :=
  { a11 := M.a11.conj
    a12 := M.a21.conj
    a21 := M.a12.conj
    a22 := M.a22.conj }

def A : Mat2 :=
  { a11 := { re := 1, im := 0 }
    a12 := { re := 2, im := 1 }
    a21 := { re := 0, im := -3 }
    a22 := { re := 4, im := 0 } }

def AH : Mat2 :=
  { a11 := { re := 1, im := 0 }
    a12 := { re := 0, im := 3 }
    a21 := { re := 2, im := -1 }
    a22 := { re := 4, im := 0 } }

def entries (M : Mat2) : List (Int × Int) :=
  [(M.a11.re, M.a11.im), (M.a12.re, M.a12.im),
   (M.a21.re, M.a21.im), (M.a22.re, M.a22.im)]

#eval entries A.conjTranspose
#eval [decide (A.conjTranspose = AH),
       decide (Mat2.conjTranspose (Mat2.conjTranspose A) = A)]

example : A.conjTranspose = AH := by decide
example : Mat2.conjTranspose (Mat2.conjTranspose A) = A := by decide

The four pairs list entries in row order as (real part, imaginary part). Run the file with exactly:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean ConjugateTransposeScratch.lean

This exact worksheet was executed successfully with Lean 4.32.0 and printed:

[(1, 0), (0, 3), (2, -1), (4, 0)]
[true, true]

This bounded file imports only Std, so it is suitable for a normal Mac or Linux machine. It checks the exact four-entry ledger and involution for this example. It does not import Mathlib, define its general Matrix.conjTranspose, or prove measurability. Those exact project obligations use the full project workflow below.

The project’s random-matrix foundation contains this exact checked theorem:

theorem measurable_conjTranspose {X : RandomMatrix Ω ι κ ℂ}
    (hX : Measurable X) :
    Measurable fun ω ↦ (X ω)ᴴ := by
  rw [measurable_iff_entries]
  intro j i
  change Measurable (star ∘ fun ω ↦ X ω i j)
  exact continuous_star.measurable.comp (measurable_entry hX i j)

The proof exposes both parts of the operation. After the transpose, the target entry has indices j i. It is the composition of the original coordinate function with star, and complex conjugation is continuous, hence measurable.

Full project check

The following scratch file imports the real project module, asks Lean for the relevant theorem types, and then proves the product and involution identities by applying those declarations.

import NonlinearDynamics.Random.RandomMatrices.Basic

open scoped Matrix

universe u v w

variable {m : Type u} {n : Type v} {l : Type w} [Fintype n]
variable (A : Matrix m n ℂ) (B : Matrix n l ℂ)

#check Matrix.conjTranspose_apply
#check Matrix.conjTranspose_mul
#check Matrix.conjTranspose_conjTranspose
#check NonlinearDynamics.Random.RandomMatrix.measurable_conjTranspose

example : (A * B)ᴴ = Bᴴ * Aᴴ := by
  exact Matrix.conjTranspose_mul A B

example : (Aᴴ)ᴴ = A := by
  exact Matrix.conjTranspose_conjTranspose A

The open scoped Matrix line enables the postfix ᴴ notation. The three types m, n, and l keep the rectangular dimensions visible. The [Fintype n] assumption makes the shared multiplication index finite, which matrix multiplication needs here.

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomMatrices/Basic.lean

Boundaries and nonclaims

• Conjugate transpose is not entrywise conjugation alone and is not transpose alone when entries are genuinely complex.
• The factor order in \((AB)^{\mathrm H}\) must reverse. The operation is an adjoint-like anti-homomorphism, not an order-preserving multiplication map.
• The condition \(A^{\mathrm H}=A\) defines Hermitian matrices. It does not define unitary matrices, which instead satisfy inverse identities involving \(A^{\mathrm H}\).
• The map \(A\mapsto A+A^{\mathrm H}\) is unnormalized. It proves Hermiticity of the output but does not preserve an already Hermitian input.
• Measurability of \(\omega\mapsto X(\omega)^{\mathrm H}\) follows from measurability of \(X\). It does not by itself choose a probability law or prove independence or integrability.

Where to continue

The Hermitian coordinate space uses conjugation on the reflected lower triangle so each free complex coordinate is supplied once. The Hermitian Frobenius geometry uses \(A^{\mathrm H}B\) in its inner-product formulas. The unitary-invariance page explains why congruence by \(U\) uses \(UAU^{\mathrm H}\).

Further reading

Mathlib’s conjugate-transpose source documents the entry rule, involution, and reversed-product theorem. Its Hermitian-matrix module uses conjugate transpose in the core fixed-point definition.