The dynamical Lie algebra

The dynamical Lie algebra (DLA) of a parameterized quantum circuit with generators {H₁, …, H_K} is the Lie closure g = ⟨i H₁, …, i H_K⟩_Lie — the smallest Lie subalgebra (under the matrix commutator ⁅A, B⁆ = A B − B A) containing the (skew-Hermitian) generators. Its dimension governs circuit expressibility, overparametrization, and barren-plateau trainability.

Here the ambient Lie algebra is gl(N, ℂ) = Matrix (Fin N) (Fin N) ℂ with its commutator bracket (LieAlgebra.ofAssociativeAlgebra). The DLA is defined for an arbitrary set of matrix generators via LieSubalgebra.lieSpan; the physical generators i • Hₖ are skew-Hermitian, so the resulting algebra lies inside u(N).

Sources: Ragone et al. (2023), A Lie Algebraic Theory of Barren Plateaus (definition Eq. (5)); Allcock et al. (2024), On the dynamical Lie algebras of QAOA.

Main definitions / results

• LeanPool.LeanQuantumAlg.dynamicalLieAlgebra — the Lie subalgebra generated by the generator set (the Lie closure).
• LeanPool.LeanQuantumAlg.generators_subset_dynamicalLieAlgebra — the generators lie in it.
• LeanPool.LeanQuantumAlg.dynamicalLieAlgebra_le_iff / dynamicalLieAlgebra_minimal — its universal property: it is the smallest Lie subalgebra containing the generators.

def QuantumAlg.dynamicalLieAlgebra {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) : LieSubalgebra ℂ (Matrix (Fin N) (Fin N) ℂ)

The dynamical Lie algebra generated by a set of matrix generators: the smallest Lie subalgebra of gl(N, ℂ) (with the commutator bracket) containing them — the Lie closure under nested commutators.

Equations

• QuantumAlg.dynamicalLieAlgebra gens = LieSubalgebra.lieSpan ℂ (Matrix (Fin N) (Fin N) ℂ) gens

theorem QuantumAlg.generators_subset_dynamicalLieAlgebra {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) : gens ⊆ ↑(dynamicalLieAlgebra gens)

The generators belong to their dynamical Lie algebra.

theorem QuantumAlg.dynamicalLieAlgebra_le_iff {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) (K : LieSubalgebra ℂ (Matrix (Fin N) (Fin N) ℂ)) : dynamicalLieAlgebra gens ≤ K ↔ gens ⊆ ↑K

Universal property. The dynamical Lie algebra is contained in a Lie subalgebra K exactly when all generators are.

theorem QuantumAlg.dynamicalLieAlgebra_minimal {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) {K : LieSubalgebra ℂ (Matrix (Fin N) (Fin N) ℂ)} (h : gens ⊆ ↑K) : dynamicalLieAlgebra gens ≤ K

Minimality. The dynamical Lie algebra is the smallest Lie subalgebra containing the generators.

Controllability

def QuantumAlg.IsControllable {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) : Prop

Algebraic controllability criterion. The system is controllable when its dynamical Lie algebra is all of gl(N, ℂ). For unitary dynamics the reachable set is the connected Lie group exp(g), which is the whole group exactly when g is the full algebra; we record the Lie-algebraic criterion (g = ⊤). Identifying the reachable set with exp(g) at the Lie-group level is left to future work.

Equations

• QuantumAlg.IsControllable gens = (QuantumAlg.dynamicalLieAlgebra gens = ⊤)

theorem QuantumAlg.isControllable_iff_forall_mem {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) : IsControllable gens ↔ ∀ (A : Matrix (Fin N) (Fin N) ℂ), A ∈ dynamicalLieAlgebra gens

Controllability is equivalent to every matrix lying in the Lie closure of the generators.

theorem QuantumAlg.IsControllable.mono {N : ℕ} {gens gens' : Set (Matrix (Fin N) (Fin N) ℂ)} (hsub : gens ⊆ gens') (hc : IsControllable gens) : IsControllable gens'

Enlarging the generator set preserves controllability.

Classification: the abelian (mutually commuting) case

theorem QuantumAlg.dynamicalLieAlgebra_lie_eq_zero_of_comm {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (hcomm : ∀ a ∈ gens, ∀ b ∈ gens, ⁅a, b⁆ = 0) {x y : Matrix (Fin N) (Fin N) ℂ} (hx : x ∈ dynamicalLieAlgebra gens) (hy : y ∈ dynamicalLieAlgebra gens) : ⁅x, y⁆ = 0

Abelian case of the Pauli-Lie-algebra classification. If the generators pairwise commute, the dynamical Lie algebra is abelian: the commutator vanishes on all of it. This is the free/trivial end of the structural classification of Pauli-generated Lie algebras (Aguilar et al. 2024).

theorem QuantumAlg.DynamicalLieAlgebra.main {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) {K : LieSubalgebra ℂ (Matrix (Fin N) (Fin N) ℂ)} (h : gens ⊆ ↑K) : dynamicalLieAlgebra gens ≤ K

Main theorem: the DLA is the smallest Lie subalgebra containing the generators.

theorem QuantumAlg.DynamicalLieAlgebra.main_generators_subset {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) : gens ⊆ ↑(dynamicalLieAlgebra gens)

Public supporting theorem: generators belong to their DLA.

theorem QuantumAlg.DynamicalLieAlgebra.main_le_iff {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) (K : LieSubalgebra ℂ (Matrix (Fin N) (Fin N) ℂ)) : dynamicalLieAlgebra gens ≤ K ↔ gens ⊆ ↑K

Public supporting theorem: the universal property of the DLA.

theorem QuantumAlg.DynamicalLieAlgebra.main_abelian_of_commuting_generators {N : ℕ} {gens : Set (Matrix (Fin N) (Fin N) ℂ)} (hcomm : ∀ a ∈ gens, ∀ b ∈ gens, ⁅a, b⁆ = 0) {x y : Matrix (Fin N) (Fin N) ℂ} (hx : x ∈ dynamicalLieAlgebra gens) (hy : y ∈ dynamicalLieAlgebra gens) : ⁅x, y⁆ = 0

Public supporting theorem: commuting generators produce an abelian DLA.

theorem QuantumAlg.DLAReachability.main {N : ℕ} (gens : Set (Matrix (Fin N) (Fin N) ℂ)) : IsControllable gens ↔ ∀ (A : Matrix (Fin N) (Fin N) ℂ), A ∈ dynamicalLieAlgebra gens

Main theorem: controllability is membership of every matrix in the DLA.

theorem QuantumAlg.DLAReachability.main_mono {N : ℕ} {gens gens' : Set (Matrix (Fin N) (Fin N) ℂ)} (hsub : gens ⊆ gens') (hc : IsControllable gens) : IsControllable gens'

Public supporting theorem: enlarging generators preserves controllability.