A continuous projective one-parameter unitary group lifts

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

Glossary: https://glossary.constraintsurfacedynamics.com/bargmann/ Plain-language and CSD-role statements of the Bargmann invariant and of the theorem this file makes unnecessary for the one-parameter case.

A family U : ℝ → U(N) that is a homomorphism only up to phase,

U (s + t) = c s t • (U s * U t),

is a projective representation of ℝ. This file shows that when U is continuous the phase cocycle c is a coboundary: there is a continuous unit-modulus b : ℝ → ℂ with

c s t * b (s + t) = b s * b t (exists_continuous_phase_trivialisation),

so t ↦ b t • U t is a genuine unitary group. Equivalently: a continuous projective one-parameter unitary group in finite dimensions lifts to an honest one.

Why this needs no Bargmann theorem

For a general group the obstruction is a class in H²(G, U(1)) and killing it is Bargmann's theorem. For G = ℝ there is no obstruction to kill — Λ²(ℝ) = 0 — and the proof is elementary:

• Determinants reduce N phases to one. det (c • A) = c ^ N * det A, so with d t := det (U t) the cocycle becomes d (s + t) = c s t ^ N * d s * d t, a statement about the circle, where d is continuous with ‖d t‖ = 1.
• ℝ is simply connected, so d lifts. Circle.exp is a covering map (Circle.isCoveringMap_exp), and a continuous map from a simply-connected, locally-path-connected space lifts through it (IsCoveringMap.existsUnique_continuousMap_lifts), giving continuous θ : ℝ → ℝ with d t = exp (θ t · i).
• b₀ t := exp (−θ t · i / N) trivialises up to a root of unity. By construction b₀ t ^ N = (d t)⁻¹, so the residual μ s t := c s t * b₀ (s + t) / (b₀ s * b₀ t) satisfies μ ^ N = 1.
• A continuous map into the N-th roots of unity on a connected domain is constant. ℝ × ℝ is preconnected and the roots of unity are finite, so μ is a constant κ, and rescaling b := κ • b₀ makes it 1.

Honest scope

ℝ only, and finite dimensions only — both are load-bearing (Λ²(ℝ) = 0 is what makes the cocycle die, and det is what reduces to the circle). Nothing here is Bargmann's theorem for a general topological group, which stays out of scope and out of Mathlib. MATHLIB-ABSENT(Bargmann)

Reference: Bargmann, Ann. Math. 59 (1954) 1 (the general theorem this deliberately avoids); Simms, Lie Groups and Quantum Mechanics §3 (the one-parameter case).

Two general engines

theorem Matrix.ProjectiveLift.const_of_finite_range {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] {f : X → ℂ} (hf : Continuous f) (hfin : (Set.range f).Finite) (x y : X) : f x = f y

A continuous complex-valued function with finite range on a preconnected space is constant: the range is a preconnected subset of a finite set, hence a subsingleton.

theorem Matrix.ProjectiveLift.nthRoots_finite {N : ℕ} (hN : 0 < N) : {z : ℂ | z ^ N = 1}.Finite

The N-th roots of unity in ℂ form a finite set (N > 0).

theorem Matrix.ProjectiveLift.norm_eq_one_of_star_mul_self {z : ℂ} (h : star z * z = 1) : ‖z‖ = 1

A complex number with star z * z = 1 has unit norm.

theorem Matrix.ProjectiveLift.norm_det_eq_one {N : ℕ} {U : Matrix (Fin N) (Fin N) ℂ} (hU : U ∈ unitaryGroup (Fin N) ℂ) : ‖U.det‖ = 1

The determinant of a unitary matrix has unit norm.

The trivialisation

theorem Matrix.ProjectiveLift.eq_one_of_pow_eq_one_of_nonneg {N : ℕ} (hN : 0 < N) {x : ℝ} (hx : 0 ≤ x) (h : x ^ N = 1) : x = 1

A nonnegative real with x ^ N = 1 (N > 0) is 1.

theorem Matrix.ProjectiveLift.exists_continuous_phase_trivialisation {N : ℕ} (hN : 0 < N) (U : ℝ → Matrix (Fin N) (Fin N) ℂ) (hUmem : ∀ (t : ℝ), U t ∈ unitaryGroup (Fin N) ℂ) (hUcont : Continuous U) (c : ℝ → ℝ → ℂ) (hc : ∀ (s t : ℝ), U (s + t) = c s t • (U s * U t)) : ∃ (b : ℝ → ℂ), Continuous b ∧ (∀ (t : ℝ), ‖b t‖ = 1) ∧ ∀ (s t : ℝ), c s t * b (s + t) = b s * b t

★★ A continuous projective one-parameter unitary group has a coboundary cocycle.

If U : ℝ → U(N) is continuous and satisfies U (s + t) = c s t • (U s * U t), then the phase cocycle c is trivialised by a continuous unit-modulus b, so t ↦ b t • U t is a genuine unitary group. See the module docstring for why ℝ needs no Bargmann theorem.