Compactness and measurability of the matrix unitary group

Category: 1-Mathlib (CSD-free Mathlib upstream candidate).

For N : ℕ, the matrix unitary group Matrix.unitaryGroup (Fin N) ℂ is a compact Hausdorff topological group:

• topological group: from Mathlib's Topology/Algebra/Star/Unitary.lean (unitary R is a topological group whenever R is a topological star monoid with continuous multiplication and continuous star);
• compact: closed in Matrix (Fin N) (Fin N) ℂ (from isClosed_unitary) plus bounded (each entry's modulus ≤ 1 because columns are ℓ²-unit), and Matrix (Fin N) (Fin N) ℂ is a finite-dim normed space over ℂ (proper, by Heine-Borel via FiniteDimensional.proper_rclike).

This is the substrate Mathlib's MeasureTheory.Measure.haar needs to produce a Haar measure on Matrix.unitaryGroup (Fin N) ℂ. The remaining ingredients (MeasurableSpace, BorelSpace) are also installed here.

Main results

• Matrix.UnitaryGroup.val_norm_apply_le_one: entry bound for unitary matrices.
• Matrix.UnitaryGroup.val_norm_le_one: matrix-norm bound (L∞-elementwise).
• Matrix.UnitaryGroup.instCompactSpace: compactness instance.
• Matrix.UnitaryGroup.instMeasurableSpace: Borel σ-algebra.
• Matrix.UnitaryGroup.instBorelSpace: witness that the σ-algebra is Borel.

Hypothesis pattern

Specialised to Matrix.unitaryGroup (Fin N) ℂ. The argument works for any Matrix.unitaryGroup n α where n is finite and α is an RCLike field, but we install the concrete case used by LF4's eventual U(N) Haar construction.

Provenance

Staged as upstream Mathlib material. The file is intended to land in Mathlib/LinearAlgebra/Matrix/UnitaryCompact.lean (or similar) once usage stabilises.

Tags

unitary group, compactness, Haar measure

theorem Matrix.UnitaryGroup.sum_norm_sq_col {N : ℕ} (A : ↥(unitaryGroup (Fin N) ℂ)) (j : Fin N) : ∑ k : Fin N, ‖↑A k j‖ ^ 2 = 1

For a unitary matrix A, the sum of squared moduli of any column equals 1. This is the j-th diagonal entry of star A * A = 1.

theorem Matrix.UnitaryGroup.val_norm_apply_le_one {N : ℕ} (A : ↥(unitaryGroup (Fin N) ℂ)) (i j : Fin N) : ‖↑A i j‖ ≤ 1

Each entry of a unitary matrix has modulus ≤ 1. Follows from sum_norm_sq_col: ‖A_ij‖² ≤ ∑_k ‖A_kj‖² = 1.

theorem Matrix.UnitaryGroup.val_norm_le_one {N : ℕ} (A : ↥(unitaryGroup (Fin N) ℂ)) : ‖↑A‖ ≤ 1

The L∞-elementwise matrix norm of a unitary matrix is ≤ 1.

theorem Matrix.UnitaryGroup.isBounded_underlyingSet {N : ℕ} : Bornology.IsBounded ↑(unitaryGroup (Fin N) ℂ)

The unitary group is bounded as a subset of Matrix (Fin N) (Fin N) ℂ.

theorem Matrix.UnitaryGroup.isClosed_underlyingSet {N : ℕ} : IsClosed ↑(unitaryGroup (Fin N) ℂ)

The unitary group is closed in Matrix (Fin N) (Fin N) ℂ. Mathlib generic via isClosed_unitary (requires T1 ambient, ContinuousStar, ContinuousMul — all satisfied for Matrix _ _ ℂ).

instance Matrix.UnitaryGroup.instCompactSpace {N : ℕ} : CompactSpace ↥(unitaryGroup (Fin N) ℂ)

The matrix unitary group is compact.

Routes through Metric.isCompact_iff_isClosed_isBounded on the finite-dim normed Matrix (Fin N) (Fin N) ℂ (proper via FiniteDimensional.proper_rclike), discharging IsClosed via isClosed_underlyingSet and IsBounded via isBounded_underlyingSet.

@[instance_reducible]

noncomputable instance Matrix.UnitaryGroup.instMeasurableSpace {N : ℕ} : MeasurableSpace ↥(unitaryGroup (Fin N) ℂ)

The matrix unitary group carries the Borel σ-algebra induced from its subspace topology.

Equations

• Matrix.UnitaryGroup.instMeasurableSpace = borel ↥(Matrix.unitaryGroup (Fin N) ℂ)

instance Matrix.UnitaryGroup.instBorelSpace {N : ℕ} : BorelSpace ↥(unitaryGroup (Fin N) ℂ)