The unitary group is Zariski dense in the complex matrices

A polynomial in the entries of a square complex matrix is determined by its values on the unitary matrices. The unitary group is cut out by the equations star A * A = 1, which involve complex conjugation and so are not polynomial; it is a real form of GL n ℂ, not an algebraic subgroup of it, and over ℂ it is Zariski dense.

The proof is the singular value decomposition A = U * diagonal d * V with U, V unitary (Matrix.exists_unitary_mul_diagonal_mul_unitary). Substituting U * diagonal z * V into a polynomial gives a polynomial in z ∈ ℂⁿ, and U * diagonal z * V is unitary whenever every zᵢ lies on the unit circle. A polynomial in n variables vanishing on the torus (S¹)ⁿ is zero, since the circle is infinite (MvPolynomial.funext_set), so evaluating at z = d recovers the value at A.

The same holds for the rational functions on GL n ℂ, those of the form P / det ^ m: two of them agreeing on the unitary group agree everywhere. This is the algebraic input to Weyl's unitarian trick, which reduces questions about the rational representations of GL n ℂ to questions about the continuous representations of the compact group U(n).

Over ℝ the analogous statement fails: the orthogonal group is cut out by polynomial equations, so it is a proper Zariski-closed subset of the real matrices.

Main results

• MvPolynomial.eq_of_eval_eq_on_unitaryGroup: two polynomials in the entries of a complex matrix that agree on the unitary group are equal. This is the unitary counterpart of Mathlib's MvPolynomial.eq_of_eval_eq_on_gl.
• TauCeti.Matrix.GeneralLinearGroup.eq_of_mem_rationalFunctions_of_forall_unitary: two rational functions on GL n ℂ that agree on the unitary group are equal.

References

• H. Weyl, The Classical Groups, Princeton University Press (1939), Chapter VIII, §11.
• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants (2009), Section 2.4.

theorem MvPolynomial.eq_of_eval_eq_on_unitaryGroup {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p q : MvPolynomial (ι × ι) ℂ} (h : ∀ U ∈ Matrix.unitaryGroup ι ℂ, (eval fun (ij : ι × ι) => U ij.1 ij.2) p = (eval fun (ij : ι × ι) => U ij.1 ij.2) q) : p = q

The unitary group is Zariski dense in the complex matrices. Two polynomials in the entries of a square complex matrix that take the same value at every unitary matrix are equal.

theorem TauCeti.Matrix.GeneralLinearGroup.eq_of_mem_rationalFunctions_of_forall_unitary {n : ℕ} {f g : GL (Fin n) ℂ → ℂ} (hf : f ∈ rationalFunctions ℂ n) (hg : g ∈ rationalFunctions ℂ n) (h : ∀ (u : ↥(Matrix.unitaryGroup (Fin n) ℂ)), f (Unitary.toUnits u) = g (Unitary.toUnits u)) : f = g

A rational function on GL n ℂ is determined by its values on the unitary group. Two rational functions, polynomials in the entries divided by a power of the determinant, that agree at every unitary matrix are equal.