Documentation

CsdLean4.Mathlib.LinearAlgebra.Projectivization.PhaseRigidity

Phase rigidity: unitaries with the same projective action differ by a phase #

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

Two matrix unitaries acting identically on every point of complex projective space are equal up to a global unit-modulus scalar (a "phase"). This is the uniqueness half of the projective-representation dictionary: the kernel of U(N) → PU(N) is the circle U(1) · 1.

Main results #

Proof sketch (rigidity) #

C := B⁻¹ * A fixes every ray, so every nonzero vector is an eigenvector of the induced endomorphism toEuclideanLin C. An endomorphism of a free module over a commutative domain all of whose vectors are eigenvectors is a homothety (LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent, Mathlib), so C = a • 1; unitarity of C forces star a * a = 1, i.e. ‖a‖ = 1. The degenerate N = 0 case is handled separately (Matrix (Fin 0) (Fin 0) ℂ is a subsingleton, so c = 1 works).

Provenance. Needed by the CSD dynamics spine W5-S1 (CsdLean4/LF4/PhaseLift.lean): extracting the U(1) phase cocycle of the one-parameter unitary family realising a projected Kähler-sector flow, the first step of the projective-to-vector phase lift.

Tags #

projectivization, unitary group, projective representation, phase, rigidity

source
theorem Matrix.UnitaryGroup.unit_smul_mem {N : ℕ} {c : ℂ} (hc : ‖c‖ = 1) {M : Matrix (Fin N) (Fin N) ℂ} (hM : M ∈ unitaryGroup (Fin N) ℂ) :
c • M ∈ unitaryGroup (Fin N) ℂ

A unit-modulus scalar multiple of a unitary matrix is unitary: the circle U(1) acts on unitaryGroup (Fin N) ℂ by scalar multiplication.

source
theorem Projectivization.smul_eq_smul_of_eq_smul {N : ℕ} {c : ℂ} {A B : ↥(Matrix.unitaryGroup (Fin N) ℂ)} (hAB : ↑A = c • ↑B) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) :
A • p = B • p

Unitaries whose matrices differ by a scalar act identically on projective space: scalars act trivially on rays. This is the easy (descent) direction of phase rigidity. (No nonzero hypothesis on c is needed: for N ≥ 1 a unitary is nonzero, so c = 0 is vacuous, and for N = 0 the statement is trivial.)

source
theorem Projectivization.exists_unit_smul_of_smul_eq_smul {N : ℕ} (A B : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (h : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), A • p = B • p) :
∃ (c : ℂ), ‖c‖ = 1 ∧ ↑A = c • ↑B

Phase rigidity. Two unitaries acting identically on every point of ℙ ℂ (EuclideanSpace ℂ (Fin N)) are equal up to a global unit-modulus phase: A = c • B as matrices with ‖c‖ = 1. Equivalently, the kernel of U(N) → PU(N) is the circle of phases.

Route: C := B⁻¹ * A fixes every ray, so every nonzero vector is an eigenvector of toEuclideanLin C; by LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent such an endomorphism is a homothety a • 1, and unitarity pins ‖a‖ = 1.