Determinant From Homomorphism

Lean formalization

The results in this note are formalized in Lean 4 + Mathlib in DeterminantHomomorphismFlow.lean, the flow-faithful development that follows this note’s own construction (it defines its own Leibniz polynomial L and cites no Mathlib determinant lemma), reusing the $\mathbb C^*\to\mathbb C^*$ classification from CstarHomomorphismFlow.lean. Each Lean proof dropdown below includes the corresponding declaration verbatim from the compiled source, so the displayed code cannot drift from what is actually checked. Continuous integration runs lake build (which fails on any error or sorry), so every displayed proof is guaranteed to type-check.

The Lean statements are slightly more general than the note: they hold for every finite index type n (the homomorphism is f : GLₙ(ℂ) →* ℂˣ, with ℂˣ mathlib’s group of units of ℂ, i.e. $\mathbb C^*$ ), and the one-variable factor g is read off at an arbitrary chosen diagonal slot i0 : n rather than slot 1. The single-valued determinant is the self-contained Leibniz polynomial L defined in the file. In the scalar-normalization route below ((H2)), the exponent is $n=\operatorname{Fintype.card}$ of the index type, and Lean additionally assumes it nonempty (so $n\ge 1$ , which makes $\lambda\mapsto\lambda^n$ surjective on $\mathbb C^*$ ).

Assumptions¶

$\mathbb C^* = \mathbb C\setminus\{0\}$ under multiplication; $M_n(\mathbb C)$ all complex $n\times n$ matrices; $GL(n,\mathbb C)$ the invertible ones, a group under multiplication.
$\operatorname{diag}(x_1,\dots,x_n)$ is the diagonal matrix with the listed entries.

We are given a function $f:GL(n,\mathbb C)\to \mathbb C^*$ such that:

(H1) Multiplicativity. $f(AB)=f(A)\,f(B)$ for all $A,B\in GL(n,\mathbb C)$ .

The case $n=1$ is tautological: $GL(1,\mathbb C)=\mathbb C^*$ , and the factorization is $f=g\circ\operatorname{id}$ with $g=f$ . Hence assume $n\ge 2$ below.

We also use only elementary language about rows, spans, and multilinear functions. We do not assume any prior determinant theory, determinant multiplicativity, the polar decomposition, or the spectral theorem. When the Leibniz polynomial appears below, it is introduced as an explicit polynomial and its needed properties are proved directly.

Throughout, $e_1,\dots,e_n$ is the standard basis, and we view a matrix $A$ as its list of rows $r_1,\dots,r_n\in \mathbb C^n$ . The matrix unit $E_{ij}$ is the $n\times n$ matrix with a 1 in row $i$ , column $j$ , and 0 everywhere else. We write $T_{ij}(c)=I+c\,E_{ij}$ (for $i\neq j$ ) for the transvection that adds $c$ times row $j$ to row $i$ under left multiplication.

Step 1 — $f(I)=1$ and conjugation invariance¶

From $I\cdot I=I$ and (H1): $f(I)=f(I)^2$ . Since $f(I)\in \mathbb C^*$ is nonzero, $f(I)=1$ .

For any $P\in GL(n,\mathbb C)$ , using (H1) and the commutativity of $\mathbb C^*$ ,

f(PAP^{-1})=f(P)f(A)f(P^{-1})=f(P)f(P^{-1})f(A)=f(PP^{-1})f(A)=f(A).

(1)

So $f$ is invariant under conjugation.

DeterminantHomomorphismFlow.lean

/-- **Step 1 (`f(I) = 1`).** A homomorphism `GLₙ(ℂ) → ℂˣ` sends the identity matrix to `1`. -/
theorem hom_one_eq_one (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) : f 1 = 1 :=
  map_one f

/--
**Step 1 (conjugation invariance).** A homomorphism `GLₙ(ℂ) → ℂˣ` is invariant under conjugation,
because its target `ℂˣ` is commutative: `f (P A P⁻¹) = f A`.
-/
theorem hom_conj_eq (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ)
    (P A : Matrix.GeneralLinearGroup n ℂ) : f (P * A * P⁻¹) = f A := by
  rw [map_mul, map_mul, map_inv, mul_comm (f P) (f A), mul_assoc, mul_inv_cancel, mul_one]

Step 2 — $f$ equals 1 on every transvection¶

Fix $i\neq j$ . Two observations.

All nonzero $c$ give conjugate transvections. For an invertible diagonal $D=\operatorname{diag}(d_1,\dots,d_n)$ one computes $D\,T_{ij}(c)\,D^{-1}=T_{ij}\!\big(c\,d_i/d_j\big)$ . Choosing $d_i/d_j$ freely, the factor $c\,d_i/d_j$ ranges over all of $\mathbb C^*$ . Hence all $T_{ij}(c)$ with $c\neq 0$ are conjugate, so by (1) the value $f(T_{ij}(c))=:t$ is the same for every $c\neq 0$ .

DeterminantHomomorphismFlow.lean

/--
**Step 2 (diagonal conjugation).** Conjugating a transvection by an invertible diagonal matrix
rescales the off-diagonal entry: `D Tᵢⱼ(c) D⁻¹ = Tᵢⱼ((dᵢ/dⱼ) c)`.
-/
theorem diagonal_conj_transvection (d : n → ℂ) (hd : ∀ k, d k ≠ 0) {i j : n} (hij : i ≠ j)
    (c : ℂ) :
    Matrix.diagonal d * Matrix.transvection i j c * Matrix.diagonal (fun k => (d k)⁻¹)
      = Matrix.transvection i j (d i * (d j)⁻¹ * c) := by
  ext k l
  rw [Matrix.mul_diagonal, Matrix.diagonal_mul]
  simp only [Matrix.transvection, Matrix.add_apply, Matrix.one_apply, Matrix.single_apply]
  by_cases h1 : k = l
  · by_cases h2 : i = k ∧ j = l
    · exact absurd (h2.1.trans (h1.trans h2.2.symm)) hij
    · simp only [if_pos h1, if_neg h2, add_zero, mul_one]
      rw [h1]; exact mul_inv_cancel₀ (hd l)
  · by_cases h2 : i = k ∧ j = l
    · simp only [if_neg h1, if_pos h2, zero_add]
      obtain ⟨rfl, rfl⟩ := h2
      ring
    · simp only [if_neg h1, if_neg h2, mul_zero, zero_mul, add_zero]

The common value satisfies $t=t^2$ . Since $E_{ij}^2=0$ , we have $T_{ij}(c)\,T_{ij}(c')=T_{ij}(c+c')$ . Taking $c=c'=1$ and applying (H1): $t=f(T_{ij}(2))=f(T_{ij}(1))^2=t^2$ . As $t\in \mathbb C^*$ , this forces $t=1$ . Together with $T_{ij}(0)=I$ and Step 1,

f\big(T_{ij}(c)\big)=1\qquad\text{for all }c.

(2)

In particular, by (H1), left- or right-multiplying by a transvection does not change $f$ — i.e. adding a multiple of one row (or column) to another leaves $f$ unchanged.

DeterminantHomomorphismFlow.lean

/--
**Step 2 (transvections have trivial image).** Any homomorphism `GLₙ(ℂ) → ℂˣ` sends every
transvection to `1`. Conjugating `Tᵢⱼ(c)` by `diag(2 at i, 1 else)` doubles the parameter
(`D Tᵢⱼ(c) D⁻¹ = Tᵢⱼ(2c) = Tᵢⱼ(c)²`), so by conjugation invariance `f(Tᵢⱼ(c))² = f(Tᵢⱼ(c))`, and a
value of `ℂˣ` with `t² = t` is `1`.
-/
theorem hom_transvection_eq_one (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) {i j : n} (hij : i ≠ j)
    (c : ℂ) : f (transvectionGL hij c) = 1 := by
  set d : n → ℂ := fun k => if k = i then 2 else 1 with hd_def
  have hd : ∀ k, d k ≠ 0 := fun k => by by_cases hk : k = i <;> simp [hd_def, hk]
  have hdi : d i = 2 := by simp [hd_def]
  have hdj : d j = 1 := by simp only [hd_def]; rw [if_neg (Ne.symm hij)]
  have hadd : transvectionGL hij (c + c) = transvectionGL hij c * transvectionGL hij c := by
    change Matrix.SpecialLinearGroup.toGL (Matrix.SpecialLinearGroup.transvection hij (c + c))
      = Matrix.SpecialLinearGroup.toGL (Matrix.SpecialLinearGroup.transvection hij c)
        * Matrix.SpecialLinearGroup.toGL (Matrix.SpecialLinearGroup.transvection hij c)
    rw [Matrix.SpecialLinearGroup.transvection_add, map_mul]
  have hconj : diagonalGL d hd * transvectionGL hij c * (diagonalGL d hd)⁻¹
      = transvectionGL hij (c + c) := by
    apply Units.ext
    simp only [Units.val_mul, coe_diagonalGL, coe_transvectionGL, coe_diagonalGL_inv]
    rw [diagonal_conj_transvection d hd hij c, hdi, hdj]
    congr 1
    rw [inv_one, mul_one]
    ring
  have ht2 : f (transvectionGL hij c) * f (transvectionGL hij c) = f (transvectionGL hij c) := by
    rw [← map_mul, ← hadd, ← hconj, hom_conj_eq]
  have ht1 : f (transvectionGL hij c) * f (transvectionGL hij c)
      = f (transvectionGL hij c) * 1 := by rw [mul_one]; exact ht2
  exact mul_left_cancel ht1

Step 3 — The one-variable function $g$ , and $f$ on diagonal matrices¶

Define

g(x):=f\big(\operatorname{diag}(x,1,\dots,1)\big),\qquad x\in \mathbb C^*.

(3)

$g$ is a homomorphism $\mathbb C^*\to \mathbb C^*$ : from $\operatorname{diag}(xy,1,\dots,1)=\operatorname{diag}(x,1,\dots,1)\operatorname{diag}(y,1,\dots,1)$ and (H1),

g(xy)=g(x)g(y).

(4)

DeterminantHomomorphismFlow.lean

/--
`eq-dethom-g-homomorphism`. The one-variable factor `g = diagonalFactorOfHom i0 f` is a
homomorphism `ℂˣ → ℂˣ`: `g(xy) = g(x) g(y)`.
-/
theorem diagonalFactorOfHom_mul (i0 : n) (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (x y : ℂˣ) :
    diagonalFactorOfHom i0 f (x * y)
      = diagonalFactorOfHom i0 f x * diagonalFactorOfHom i0 f y :=
  map_mul _ x y

Position does not matter. For $i>1$ let

P_i=I-E_{11}-E_{ii}+E_{1i}+E_{i1},

(5)

the permutation matrix that sends $e_1\mapsto e_i$ , $e_i\mapsto e_1$ , and fixes every other basis vector. Then $P_i^2=I$ , so $P_i\in GL(n,\mathbb C)$ with $P_i^{-1}=P_i$ . Conjugating a diagonal matrix by $P_i$ just relabels the two basis vectors, so it swaps the diagonal entries in slots 1 and $i$ : $P_i\operatorname{diag}(x,1,\dots,1)P_i^{-1}=\operatorname{diag}(1,\dots,\underset{i}{x},\dots,1)$ . By (1)

f\big(\operatorname{diag}(1,\dots,\underset{i}{x},\dots,1)\big)=g(x).

(6)

DeterminantHomomorphismFlow.lean

/--
`eq-dethom-diagonal-slot`. The value of `f` on a single populated diagonal slot is exactly the
one-variable factor `g`: `f(diag(1,…,x at i,…,1)) = g(x)`.
-/
theorem hom_oneSlotDiagonalGL_eq_g (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 i : n) (x : ℂˣ) :
    f (oneSlotDiagonalGL i x) = diagonalFactorOfHom i0 f x :=
  hom_oneSlotDiagonalGL_pos_invariant f i0 i x

Product over the diagonal. Writing $\operatorname{diag}(d_1,\dots,d_n)=\prod_{i=1}^n\operatorname{diag}(1,\dots,\underset{i}{d_i},\dots,1)$ and using (H1), (6), and (4),

f\big(\operatorname{diag}(d_1,\dots,d_n)\big)=\prod_{i=1}^n g(d_i)=g\!\Big(\prod_{i=1}^n d_i\Big).

(7)

DeterminantHomomorphismFlow.lean

/--
**Step 3 (product over the diagonal).** Evaluating a homomorphism `f` on a diagonal matrix gives the
product over the slots of the single-slot factor `g = diagonalFactorOfHom i0 f`, equivalently `g`
applied to the product of the diagonal entries: `f(diag D) = ∏ⱼ g(Dⱼ) = g(∏ⱼ Dⱼ)`.
-/
theorem hom_diagonalGL_eq (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n)
    (D : n → ℂ) (hD : ∀ i, D i ≠ 0) :
    f (diagonalGL D hD)
      = diagonalFactorOfHom i0 f (∏ j : n, Units.mk0 (D j) (hD j)) := by
  rw [← diagOnGL_univ D hD, hom_diagOnGL_eq f i0 D hD Finset.univ,
    ← map_prod (diagonalFactorOfHom i0 f)]

The factorization theorem $f=g\circ\det$ (multiplicativity only)¶

Everything so far (Steps 1–3) used only that $f$ is a homomorphism (H1). Three facts are all we shall use:

(H1) $f$ is a homomorphism $GL(n,\mathbb C)\to \mathbb C^*$ ;
(2): $f\big(T_{ij}(c)\big)=1$ for every transvection;
(7): $f\big(\operatorname{diag}(d_1,\dots,d_n)\big)=g\!\big(\prod_i d_i\big)$ , with $g:\mathbb C^*\to \mathbb C^*$ the homomorphism of Step 3.

We show these force $f=g\circ\det$ , the determinant being supplied — single-valued — by the Leibniz polynomial. We work entirely inside $GL(n,\mathbb C)$ , never evaluating $f$ on a singular matrix, with no appeal to continuity, exterior algebra, or Zariski density.

1. Transvections and diagonal matrices generate $GL(n,\mathbb C)$ . Lemma. Every $A\in GL(n,\mathbb C)$ factors as

A=E\,D,\qquad E=\text{a product of transvections},\quad D=\operatorname{diag}(d_1,\dots,d_n),\quad d_i\in \mathbb C^*.

(8)

Proof. Row-reduce $A$ using only transvections — no row swaps, no pivot normalization. Adding $c$ times row $j$ to row $i$ is left multiplication by $T_{ij}(c)$ , and every intermediate matrix is invertible, being a product of invertible matrices.

Proceed column by column. Suppose columns $1,\dots,k-1$ have already been reduced to nonzero diagonal entries with all their other entries cleared. In column $k$ , at least one entry in rows $k,\dots,n$ is nonzero: otherwise column $k$ would be supported in rows $1,\dots,k-1$ , hence a linear combination of columns $1,\dots,k-1$ (which are nonzero multiples of $e_1,\dots,e_{k-1}$ ), contradicting invertibility. If the pivot entry $a_{kk}$ is zero, pick $\ell>k$ with $a_{\ell k}\neq 0$ and add row $\ell$ to row $k$ (one transvection $T_{k\ell}(1)$ ); this makes the pivot equal to $a_{\ell k}\neq 0$ , and it disturbs nothing in columns $1,\dots,k-1$ , where row $\ell$ has only zeros. Now, with pivot $\alpha=a_{kk}\neq 0$ , for each row $\ell\neq k$ add $-a_{\ell k}/\alpha$ times row $k$ to row $\ell$ to clear the rest of column $k$ ; this leaves the earlier pivot columns untouched because row $k$ has zeros there.

After column $n$ this yields transvections $T_1,\dots,T_m$ with

T_m\cdots T_1 A=D,

(9)

$D$ invertible diagonal. Since $T_{ij}(c)^{-1}=T_{ij}(-c)$ is again a transvection,

A=T_1^{-1}\cdots T_m^{-1}\,D

(10)

is a factorization of the required form. $\square$

DeterminantHomomorphismFlow.lean

/--
`eq-dethom-transvection-diagonal-factorization`. **Generation.** Every `A ∈ GLₙ(ℂ)` factors as
`A = E · D` with `E` a product of transvections and `D` invertible diagonal. The nonvanishing of the
`dᵢ` is obtained *without* the determinant: `diagonal D` is a product of invertible matrices, hence
a unit, so its entries are units (`Matrix.isUnit_diagonal`). -/
theorem exists_transvec_diagonal_factorization (A : Matrix.GeneralLinearGroup n ℂ) :
    ∃ (E : List (Matrix.TransvectionStruct n ℂ)) (D : n → ℂ) (hD : ∀ i, D i ≠ 0),
      A = (E.map transvecStructGL).prod * diagonalGL D hD := by
  obtain ⟨L, L', D, hLDL'⟩ :=
    Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec (A : Matrix n n ℂ)
  set P := (L.map transvecStructGL).prod with hPdef
  set Q := (L'.map transvecStructGL).prod with hQdef
  have hPco : (↑P : Matrix n n ℂ) = (L.map Matrix.TransvectionStruct.toMatrix).prod := by
    rw [hPdef]; exact coe_prod_transvecStructGL L
  have hQco : (↑Q : Matrix n n ℂ) = (L'.map Matrix.TransvectionStruct.toMatrix).prod := by
    rw [hQdef]; exact coe_prod_transvecStructGL L'
  have hAeq : (A : Matrix n n ℂ) = (P : Matrix n n ℂ) * Matrix.diagonal D * (Q : Matrix n n ℂ) := by
    rw [hPco, hQco]; exact hLDL'
  have hPinv : (↑(P⁻¹) : Matrix n n ℂ) * (P : Matrix n n ℂ) = 1 := by
    rw [← Units.val_mul, inv_mul_cancel, Units.val_one]
  have hQinv : (Q : Matrix n n ℂ) * (↑(Q⁻¹) : Matrix n n ℂ) = 1 := by
    rw [← Units.val_mul, mul_inv_cancel, Units.val_one]
  have hDeq : (↑(P⁻¹ * A * Q⁻¹) : Matrix n n ℂ) = Matrix.diagonal D := by
    rw [Units.val_mul, Units.val_mul, hAeq]
    calc (↑(P⁻¹) : Matrix n n ℂ) * ((P : Matrix n n ℂ) * Matrix.diagonal D * (Q : Matrix n n ℂ))
          * (↑(Q⁻¹) : Matrix n n ℂ)
        = ((↑(P⁻¹) : Matrix n n ℂ) * (P : Matrix n n ℂ)) * Matrix.diagonal D
            * ((Q : Matrix n n ℂ) * (↑(Q⁻¹) : Matrix n n ℂ)) := by simp only [Matrix.mul_assoc]
      _ = Matrix.diagonal D := by rw [hPinv, hQinv, Matrix.one_mul, Matrix.mul_one]
  have hDunit : IsUnit (Matrix.diagonal D) := hDeq ▸ (P⁻¹ * A * Q⁻¹).isUnit
  have hD : ∀ i, D i ≠ 0 := by
    intro i
    have hu := Matrix.isUnit_diagonal.mp hDunit
    rw [Pi.isUnit_iff] at hu
    exact (hu i).ne_zero
  have hAtwo : A = P * diagonalGL D hD * Q := by
    apply Units.ext
    rw [Units.val_mul, Units.val_mul, hPco, coe_diagonalGL, hQco]
    exact hLDL'
  refine ⟨L ++ L'.map (conjDiagStruct D), D, hD, ?_⟩
  rw [List.map_append, List.prod_append, ← conjGL_prod D hD L', hAtwo, hPdef, hQdef]
  group

2. Existence: the Leibniz polynomial. Before drawing any conclusion about the abstract $f$ , exhibit one explicit function we can evaluate unambiguously. Let

L(A):=\sum_{\sigma\in S_n}\operatorname{sgn}(\sigma)\prod_{i=1}^n a_{i,\sigma(i)},

(11)

a polynomial defined for every matrix by this formula — hence single-valued by construction. The following are formal identities in the entries, valid for all $A$ (singular included) and checked directly on the sum:

(a) $L(I)=1$ , and more generally $L\big(\operatorname{diag}(d_1,\dots,d_n)\big)=\prod_i d_i$ — only $\sigma=\mathrm{id}$ survives;
(b) two equal rows $\Rightarrow L=0$ : if rows $p$ and $q$ are equal and $\tau=(p\ q)$ , then pairing each $\sigma$ with $\sigma\circ\tau$ gives equal products with opposite signs, so the sum cancels pair by pair;
(c) $L$ is linear in each row — every summand is.

From (b) and (c), adding a multiple of one row to another leaves $L$ unchanged. Explicitly, write $L(r_1,\dots,r_n)$ for $L$ evaluated on the matrix with rows $r_1,\dots,r_n$ . If $i\neq j$ , then multilinearity in the $i$ -th row gives

\begin{aligned} L(r_1,\dots,\underset{i}{r_i+c r_j},\dots,r_n) &=L(r_1,\dots,\underset{i}{r_i},\dots,r_n)\\ &\quad+c\,L(r_1,\dots,\underset{i}{r_j},\dots,r_n)\\ &=L(r_1,\dots,\underset{i}{r_i},\dots,r_n), \end{aligned}

(12)

because the second term has rows $i$ and $j$ equal. Hence $L\big(T_{ij}(c)\,X\big)=L(X)$ ; taking $X=I$ and using (a) gives in particular $L(T_{ij}(c))=1$ . Thus $L$ satisfies $L(T_{ij}(c))=1$ and $L(\operatorname{diag}(d_1,\dots,d_n))=\prod_i d_i$ outright — and, unlike the abstract $f$ on $GL$ , with no domain caveat, because $L$ is everywhere-defined and (b) is a genuine polynomial identity even though “two equal rows” is a singular configuration.

Feed $L$ a factorization (8). Peeling the transvections of $E$ off one at a time by $L(T_{ij}(c)X)=L(X)$ , then applying (a),

L(A)=L(E\,D)=L(D)=\prod_i d_i.

(13)

In particular, $L(A)\in \mathbb C^*$ for $A\in GL(n,\mathbb C)$ .

DeterminantHomomorphismFlow.lean

/-- **`eq-dethom-leibniz-factorization` (derived).** The determinant of a transvection–diagonal
factorization is the product of the diagonal entries. -/
theorem L_factorization (ts : List (Matrix.TransvectionStruct n ℂ)) (D : n → ℂ) :
    L ((ts.map Matrix.TransvectionStruct.toMatrix).prod * Matrix.diagonal D)
      = ∏ i, D i := by
  rw [L_transvecList_mul, L_diagonal]

3. $\prod_i d_i$ is well-defined. A priori the product in (13) could depend on the factorization (8) chosen, and the concrete $L$ is exactly what rules this out: any two factorizations $A=ED=E'D'$ both satisfy (13), so both diagonal products equal the one unambiguous number $L(A)$ .

4. $L$ is multiplicative on $GL(n,\mathbb C)$ . Let $A,B\in GL(n,\mathbb C)$ . Choose factorizations

A=E_A D_A,\qquad B=E_B D_B,

(14)

with $E_A,E_B$ products of transvections and

D_A=\operatorname{diag}(a_1,\dots,a_n),\qquad D_B=\operatorname{diag}(b_1,\dots,b_n).

(15)

Then

AB=E_A\,D_A\,E_B\,D_B =E_A\,(D_AE_BD_A^{-1})\,D_AD_B.

(16)

If $E_B=T_1\cdots T_m$ is a product of transvections, then

D_AE_BD_A^{-1}=(D_AT_1D_A^{-1})\cdots(D_AT_mD_A^{-1}),

(17)

and each factor $D_AT_kD_A^{-1}$ is again a transvection by the diagonal-conjugation formula of Step 2. Therefore the displayed expression for $AB$ is a factorization of the form (8), with diagonal factor $D_AD_B=\operatorname{diag}(a_1b_1,\dots,a_nb_n)$ . Applying (13) to the chosen factorizations of $A$ , $B$ , and $AB$ gives

L(AB)=\prod_i a_i b_i=\Big(\prod_i a_i\Big)\Big(\prod_i b_i\Big)=L(A)L(B).

(18)

Thus the Leibniz polynomial is multiplicative on $GL(n,\mathbb C)$ . This note deliberately restricts the determinant derivation to $GL(n,\mathbb C)$ , not all matrices, to keep the foundational factorization theorem completely internal to invertible matrices. Multiplicativity and other determinant facts on singular matrices can be developed separately when needed; the rock-solid $GL(n,\mathbb C)$ factorization theorem is the piece used in many applications in separate notes.

DeterminantHomomorphismFlow.lean

/-- `eq-dethom-leibniz-multiplicativity`, packaged: `det(AB) = det A · det B`. -/
theorem detGL_mul (A B : Matrix.GeneralLinearGroup n ℂ) :
    detGL (A * B) = detGL A * detGL B :=
  map_mul detGL A B

5. Uniqueness: $f$ is determined by its values on diagonal matrices, and $f=g\circ\det$ . Points 2–4 were the existence half: the explicit homomorphism $L$ exists, is single-valued, and is multiplicative on $GL(n,\mathbb C)$ . Now the uniqueness half. For any factorization (8), using (H1), then (2) (so $f(E)=1$ ), then (7),

f(A)=f(E)\,f(D)=f(D)=g\!\Big(\prod_i d_i\Big)=g\big(L(A)\big),

(19)

the last equality by (13). This forces the value of $f$ at every $A\in GL(n,\mathbb C)$ : it must equal $g(L(A))$ , where $g$ is read off from $f$ on the matrices $\operatorname{diag}(x,1,\dots,1)$ (Step 3). So a homomorphism has no freedom beyond its values on diagonal matrices — two homomorphisms $GL(n,\mathbb C)\to\mathbb C^*$ that agree on the invertible diagonal matrices agree everywhere — and every homomorphism factors as $f=g\circ L$ .

DeterminantHomomorphismFlow.lean

/-- **Uniqueness.** Two homomorphisms agreeing on the diagonal slots agree everywhere. -/
theorem hom_eq_of_eq_on_oneSlot (i0 : n) (f₁ f₂ : Matrix.GeneralLinearGroup n ℂ →* ℂˣ)
    (h : ∀ x, f₁ (oneSlotDiagonalGL i0 x) = f₂ (oneSlotDiagonalGL i0 x))
    (A : Matrix.GeneralLinearGroup n ℂ) : f₁ A = f₂ A := by
  rw [hom_factor_det f₁ i0, hom_factor_det f₂ i0]
  exact h (detGL A)

/-- **Characterization of the determinant.** A homomorphism normalized so that `g = id` is `det`. -/
theorem hom_eq_detGL_of_normalized (i0 : n) (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ)
    (h : ∀ x, f (oneSlotDiagonalGL i0 x) = x) (A : Matrix.GeneralLinearGroup n ℂ) :
    f A = detGL A := by
  rw [hom_factor_det f i0]
  exact h (detGL A)

In particular, suppose $f$ satisfies the normalization $f\big(\operatorname{diag}(d_1,\dots,d_n)\big)=\prod_i d_i$ , i.e. $g=\operatorname{id}$ . Then the displayed equation reads $f(A)=L(A)$ for all $A$ . Combined with existence, this characterizes the determinant:

$L=\det$ is the unique homomorphism $GL(n,\mathbb C)\to\mathbb C^*$ whose value on every invertible diagonal matrix is the product of its diagonal entries.

For a general $f$ , this is the factorization theorem:

\boxed{\,f(A)=g(L(A)),\qquad L(A):=\sum_{\sigma\in S_n}\operatorname{sgn}(\sigma)\prod_{i=1}^n A_{i,\sigma(i)} \equiv \det A \qquad(A\in GL(n,\mathbb C)),\,}

(20)

for some homomorphism $g:\mathbb C^*\to \mathbb C^*$ — derived from multiplicativity alone, with no continuity, measurability, or Zariski density. The single-valued determinant is the explicit polynomial $L$ , the well-definedness of $\prod_i d_i=\det A$ is anchored on $L$ , and the factorization is $f=g\circ\det$ .

DeterminantHomomorphismFlow.lean

/--
**Factorization theorem `f = g ∘ det`** (the note's Step 5, derived directly). Every homomorphism
`f : GLₙ(ℂ) → ℂˣ` factors as `f(A) = f(E)·f(D) = 1·g(∏ dᵢ) = g(det A)` along a factorization
`A = E·D`, with `g = diagonalFactorOfHom i0 f`. -/
theorem hom_factor_det (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n)
    (A : Matrix.GeneralLinearGroup n ℂ) :
    f A = diagonalFactorOfHom i0 f (detGL A) := by
  obtain ⟨E, D, hD, hA⟩ := exists_transvec_diagonal_factorization A
  rw [hA, map_mul, hom_prod_transvecStructGL_eq_one, one_mul, hom_diagonalGL_eq f i0 D hD]
  congr 1
  apply Units.ext
  rw [coe_detGL]
  have hco : (↑((E.map transvecStructGL).prod * diagonalGL D hD) : Matrix n n ℂ)
      = (E.map Matrix.TransvectionStruct.toMatrix).prod * Matrix.diagonal D := by
    rw [Units.val_mul, coe_prod_transvecStructGL, coe_diagonalGL]
  rw [hco, L_factorization, Units.coe_prod]
  simp [Units.val_mk0]

/-- The boxed statement in existential form: `f = g ∘ det` for some homomorphism `g : ℂˣ → ℂˣ`. -/
theorem exists_hom_factor_det (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n) :
    ∃ g : ℂˣ →* ℂˣ, ∀ A : Matrix.GeneralLinearGroup n ℂ, f A = g (detGL A) :=
  ⟨diagonalFactorOfHom i0 f, hom_factor_det f i0⟩

/-- The factor `g` is unique (the determinant is surjective onto `ℂˣ`). -/
theorem existsUnique_hom_factor_det (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n) :
    ∃! g : ℂˣ →* ℂˣ, ∀ A : Matrix.GeneralLinearGroup n ℂ, f A = g (detGL A) := by
  refine ⟨diagonalFactorOfHom i0 f, hom_factor_det f i0, ?_⟩
  intro g hg
  refine MonoidHom.ext fun w => ?_
  have hA := hg (oneSlotDiagonalGL i0 w)
  rw [hom_factor_det f i0, detGL_oneSlotDiagonalGL] at hA
  exact hA.symm

DeterminantHomomorphismFlow.lean

/-- `L` is, by definition, the Leibniz polynomial in the note's index convention `Aᵢ,σ(i)`. -/
theorem determinant_leibniz_formula (A : Matrix n n ℂ) :
    L A = ∑ σ : Equiv.Perm n, ((Equiv.Perm.sign σ : ℤ) : ℂ) * ∏ i, A i (σ i) :=
  rfl

Conversely, every $g\circ\det$ with $g\in\operatorname{Hom}(\mathbb C^*,\mathbb C^*)$ is a homomorphism $GL(n,\mathbb C)\to \mathbb C^*$ : by (18), $L(AB)=L(A)L(B)$ on $GL(n,\mathbb C)$ , and then $g(L(AB))=g(L(A))g(L(B))$ . Hence these are exactly all of them: the determinant is the universal homomorphism, and every other homomorphism is obtained by post-composing it with an arbitrary group homomorphism $g:\mathbb C^*\to\mathbb C^*$ .

DeterminantHomomorphismFlow.lean

/-- Post-composing determinant with a homomorphism `ℂˣ → ℂˣ`. -/
def postcomposeDetGL (g : ℂˣ →* ℂˣ) : Matrix.GeneralLinearGroup n ℂ →* ℂˣ :=
  g.comp detGL

@[simp] theorem postcomposeDetGL_apply (g : ℂˣ →* ℂˣ) (A : Matrix.GeneralLinearGroup n ℂ) :
    postcomposeDetGL g A = g (detGL A) := rfl

/-- **Converse.** Every `g ∘ det` is a homomorphism `GLₙ(ℂ) → ℂˣ`. -/
theorem postcomposeDetGL_mul (g : ℂˣ →* ℂˣ) (A B : Matrix.GeneralLinearGroup n ℂ) :
    postcomposeDetGL g (A * B) = postcomposeDetGL g A * postcomposeDetGL g B :=
  map_mul (postcomposeDetGL g) A B

DeterminantHomomorphismFlow.lean

/-- Every homomorphism is some `g ∘ det`; together with the converse, these are exactly all of
them. -/
theorem hom_eq_postcomposeDetGL (i0 : n) (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) :
    f = postcomposeDetGL (diagonalFactorOfHom i0 f) := by
  ext A
  rw [postcomposeDetGL_apply, hom_factor_det f i0]

The complete classification of the homomorphisms $f$ ¶

Everything so far used only that $f$ is a homomorphism, and one further computation in that same spirit will be needed below. Evaluating $f$ on a scalar matrix $\lambda I=\operatorname{diag}(\lambda,\dots,\lambda)$ requires no new hypothesis: putting $d_1=\dots=d_n=\lambda$ in (7),

f(\lambda I)=g\!\Big(\prod_{i=1}^n\lambda\Big)=g\big(\lambda^{\,n}\big),\qquad \lambda\in\mathbb C^*.

(21)

In particular the determinant — the case $g=\operatorname{id}$ — satisfies $\det(\lambda I)=\prod_i\lambda=\lambda^n$ , read off directly from (13). We return to this in the final section.

DeterminantHomomorphismFlow.lean

/--
**`eq-dethom-scalar` (from multiplicativity alone).** Evaluating any homomorphism `f` on the scalar
matrix `λI` gives `g(λⁿ)`, where `g = diagonalFactorOfHom i0 f` and `n = Fintype.card n`: by Step 3
(`eq-dethom-diagonal-product`), `f(λI) = g(∏ᵢ λ) = g(λⁿ)`. -/
theorem hom_scalarGL_eq (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n) (x : ℂˣ) :
    f (scalarGL x) = diagonalFactorOfHom i0 f (x ^ Fintype.card n) := by
  rw [scalarGL, hom_diagonalGL_eq f i0 (fun _ => (x : ℂ)) (fun _ => x.ne_zero)]
  congr 1
  simp [Finset.prod_const, Finset.card_univ, Units.mk0_val]

/-- The determinant realizes the normalization (it is the `g = id` case): `det(λI) = λⁿ`, directly
from the Leibniz identity `L(diag d) = ∏ᵢ dᵢ`. -/
theorem detGL_scalarGL (x : ℂˣ) :
    detGL (scalarGL x : Matrix.GeneralLinearGroup n ℂ) = x ^ Fintype.card n := by
  apply Units.ext
  rw [coe_detGL, coe_scalarGL, L_diagonal]
  simp [Finset.prod_const, Finset.card_univ, Units.val_pow_eq_pow_val]

The factorization theorem already collapsed all freedom in $f$ onto the single homomorphism $g:\mathbb C^*\to\mathbb C^*$ , so classifying the homomorphisms $f$ is exactly classifying the group homomorphisms $g$ . Assuming nothing further, these split into precisely two kinds:

$g$ is not measurable. Already the radial factor misbehaves: $\mathbb R_{>0}\cong(\mathbb R,+)$ via $\log$ , and the additive self-maps of $\mathbb R$ include wildly discontinuous, non-measurable ones built from a Hamel basis of $\mathbb R$ over $\mathbb Q$ (existing only through the axiom of choice). Extending such a map by the trivial map on the circle factor $S^1$ yields a non-measurable homomorphism $g:\mathbb C^*\to\mathbb C^*$ with no closed form. These are pathological and irrelevant to every application, so we do not investigate them further. (The same Hamel-basis pathology, for the additive Cauchy equation, is treated in Homomorphisms $\mathbb C^*\to\mathbb C^*$ .)
$g$ is measurable. Then — not even continuity is required; mere Borel measurability suffices — $g$ is forced into the closed form
$g(w)=|w|^s\left(\frac{w}{|w|}\right)^k,\qquad s\in\mathbb C,\quad k\in\mathbb Z,$
(22)
with the pair $(s,k)$ unique, as derived in Homomorphisms $\mathbb C^*\to\mathbb C^*$ . There is no other option.

We assumed nothing, so this is the complete classification: every homomorphism is $f=g\circ\det$ with $g$ either a (useless) non-measurable solution or the polar form, in which case

f(A)=|\det A|^s\left(\frac{\det A}{|\det A|}\right)^k.

(23)

DeterminantHomomorphismFlow.lean

/-- The determinant's own factor is the identity (`det` is `s = 1`, `k = 1`). -/
theorem diagonalFactorOfHom_detGL (i0 : n) :
    diagonalFactorOfHom i0 detGL = MonoidHom.id ℂˣ := by
  ext x
  simp [diagonalFactorOfHom, detGL_oneSlotDiagonalGL]

/--
**Link to `ℂ* → ℂ*` classification.** If the one-variable factor `g = diagonalFactorOfHom i0 f`
is Borel measurable (in particular if it is continuous), then `f` has the closed form
`f(A) = |det A|ˢ · (det A / |det A|)ᵏ` for some `s ∈ ℂ`, `k ∈ ℤ`, by the flow-faithful
classification `CstarFlow.cstar_homomorphism_formula_measurable`. The determinant itself is the
case `s = 1`, `k = 1` (`diagonalFactorOfHom_detGL`).
-/
theorem hom_factor_det_cstar (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n)
    (hg : Measurable (diagonalFactorOfHom i0 f)) :
    ∃ s : ℂ, ∃ k : ℤ, ∀ A : Matrix.GeneralLinearGroup n ℂ,
      f A = cstarNormCPow s (detGL A) * cstarCircleUnit (detGL A) ^ k := by
  obtain ⟨s, k, hsk⟩ := cstar_homomorphism_formula_measurable (diagonalFactorOfHom i0 f) hg
  exact ⟨s, k, fun A => by rw [hom_factor_det f i0, hsk]⟩

/-- **Link to the `ℂ* → ℂ*` classification.** If `g` is measurable, `f(A) = |det A|ˢ (det A/|det
A|)ᵏ` with `(s, k)` unique. -/
theorem existsUnique_hom_factor_det_cstar (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n)
    (hg : Measurable (diagonalFactorOfHom i0 f)) :
    ∃! sk : ℂ × ℤ, ∀ A : Matrix.GeneralLinearGroup n ℂ,
      f A = cstarNormCPow sk.1 (detGL A) * cstarCircleUnit (detGL A) ^ sk.2 := by
  obtain ⟨s, k, hsk⟩ := cstar_homomorphism_formula_measurable (diagonalFactorOfHom i0 f) hg
  refine ⟨(s, k), fun A => by rw [hom_factor_det f i0, hsk], ?_⟩
  rintro ⟨s', k'⟩ hf'
  have hg' : ∀ w : ℂˣ, diagonalFactorOfHom i0 f w = cstarFormulaHom s' k' w := by
    intro w
    have hw := hf' (oneSlotDiagonalGL i0 w)
    rw [hom_factor_det f i0, detGL_oneSlotDiagonalGL] at hw
    exact hw
  have hkey : cstarFormulaHom s k = cstarFormulaHom s' k' := by
    refine MonoidHom.ext fun w => ?_
    rw [← hg' w]
    exact (hsk w).symm
  obtain ⟨hs, hk⟩ := cstarFormulaHom_injective hkey
  simp only [Prod.mk.injEq]
  exact ⟨hs.symm, hk.symm⟩

Selecting the determinant by $f(\lambda I)=\lambda^n$ ¶

Within the measurable family the determinant is the regular member $s=1,\,k=1$ (i.e. $g(w)=w$ ). Remarkably, it can be singled out of the entire classification above — bypassing the measurable/non-measurable split altogether — by one purely algebraic condition, with no regularity assumed at all:

(H2) Scalar normalization. $f(\lambda I)=\lambda^n$ for all $\lambda\in\mathbb C^*$ .

By (21), (H2) says precisely that $g(\lambda^n)=\lambda^n$ for all $\lambda\in\mathbb C^*$ . Now $\lambda\mapsto\lambda^n$ is surjective onto $\mathbb C^*$ : since $\mathbb C$ is algebraically closed, every $w\in\mathbb C^*$ has an $n$ -th root $\lambda$ , nonzero because $w=\lambda^n\neq0$ . Hence for every $w=\lambda^n$ ,

g(w)=g\big(\lambda^{\,n}\big)=\lambda^{\,n}=w,

(24)

so $g=\operatorname{id}$ , that is $s=1,\,k=1$ . The single condition (H2) thus reaches into the full classification and fixes the regular solution outright — excluding every other measurable $(s,k)$ and every non-measurable Hamel-basis solution — using only the existence of $n$ -th roots, with no continuity, measurability, or Zariski density. Substituting $g=\operatorname{id}$ into $f=g\circ\det$ ,

\boxed{\,f(\lambda I)=\lambda^n\ \ (\forall\lambda\in\mathbb C^*)\quad\Longrightarrow\quad f(A)=\det A\ \ (\forall A\in GL(n,\mathbb C)).\,}

(25)

DeterminantHomomorphismFlow.lean

/--
**The normalization forces `g = id`.** If `f(λI) = λⁿ` for every `λ ∈ ℂ*`, then the one-variable
factor `g = diagonalFactorOfHom i0 f` is the identity: by `eq-dethom-scalar`, `g(λⁿ) = λⁿ` for all
`λ`, and since `λ ↦ λⁿ` is surjective on `ℂ*`, every `w` is some `λⁿ`, so `g(w) = g(λⁿ) = λⁿ = w`.
**No continuity or measurability is used.** -/
theorem diagonalFactorOfHom_eq_id_of_scalar_pow [Nonempty n]
    (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n)
    (h : ∀ x : ℂˣ, f (scalarGL x) = x ^ Fintype.card n) :
    diagonalFactorOfHom i0 f = MonoidHom.id ℂˣ := by
  refine MonoidHom.ext fun w => ?_
  obtain ⟨z, hz⟩ := exists_unit_pow_eq (Fintype.card n) Fintype.card_pos w
  have hx := h z
  rw [hom_scalarGL_eq f i0 z, hz] at hx
  rw [MonoidHom.id_apply]
  exact hx

/--
**Determinant from the scalar normalization.** A homomorphism with `f(λI) = λⁿ` on every scalar
matrix *is* the determinant: `f(A) = det A` for all `A ∈ GLₙ(ℂ)` — derived purely algebraically,
with no continuity, measurability, or other regularity assumption. -/
theorem hom_eq_detGL_of_scalar_pow [Nonempty n]
    (f : Matrix.GeneralLinearGroup n ℂ →* ℂˣ) (i0 : n)
    (h : ∀ x : ℂˣ, f (scalarGL x) = x ^ Fintype.card n)
    (A : Matrix.GeneralLinearGroup n ℂ) : f A = detGL A := by
  rw [hom_factor_det f i0, diagonalFactorOfHom_eq_id_of_scalar_pow f i0 h, MonoidHom.id_apply]

Determinant From Homomorphism

Assumptions¶

Step 1 — f(I)=1f(I)=1f(I)=1 and conjugation invariance¶

Step 2 — fff equals 1 on every transvection¶

Step 3 — The one-variable function ggg, and fff on diagonal matrices¶

The factorization theorem f=g∘det⁡f=g\circ\detf=g∘det (multiplicativity only)¶

The complete classification of the homomorphisms fff¶

Selecting the determinant by f(λI)=λnf(\lambda I)=\lambda^nf(λI)=λn¶

Step 1 — $f(I)=1$ and conjugation invariance¶

Step 2 — $f$ equals 1 on every transvection¶

Step 3 — The one-variable function $g$ , and $f$ on diagonal matrices¶

The factorization theorem $f=g\circ\det$ (multiplicativity only)¶

The complete classification of the homomorphisms $f$ ¶

Selecting the determinant by $f(\lambda I)=\lambda^n$ ¶