Weyl matrices and the quantum Fourier lift

The Weyl matrices D^a S^b over ZMod d, built from a diagonal character matrix D and a cyclic shift S, multiply like monomials up to scalars, and for a primitive character they span all matrices by finite Fourier inversion. Assigning the Weyl unit of (a, b) to the exponent (a, b) ∈ ℤ ×ₗ ℤ makes the monomial-line Hahn series of QuantumSeries a division ring, which receives the Fourier lift of every matrix. Splitting matrix-valued Hahn series entrywise gives a matrix representation of this division ring over a commutative Hahn field.

Main definitions

• HahnMatrix.entry, HahnMatrix.split: entries of matrix-valued Hahn series, and the ring isomorphism onto matrices of Hahn series.
• QuantumMatrices.weyl, QuantumMatrices.weylUnit: the Weyl matrix D^a S^b and its unit.
• QuantumMatrices.fourierCoeff: the Fourier coefficient of a matrix at (a, b).
• QuantumLift.divisionSubring: the Weyl-monomial Hahn series, a division ring.
• QuantumLift.lift, QuantumLift.liftD: the Fourier lift of a matrix.
• QuantumLift.representation: the matrix representation of the division subring.

Main results

• QuantumMatrices.weyl_mul: the Weyl commutation rule.
• QuantumMatrices.fourier_reconstruction: Fourier inversion for a primitive character.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/QuantumMatrices.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

theorem Cslib.Circuits.Rational.HahnMatrix.coeff_mul_support_superset {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x y : HahnSeries Γ R) (a : Γ) (s t : Set Γ) (hs : s.IsPWO) (ht : t.IsPWO) (hxs : x.support ⊆ s) (hyt : y.support ⊆ t) : (x * y).coeff a = ∑ ij ∈ Finset.antidiagonal hs ht a, x.coeff ij.1 * y.coeff ij.2

def Cslib.Circuits.Rational.HahnMatrix.entry {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Ring R] {ι : Type u_3} (x : HahnSeries Γ (Matrix ι ι R)) (i j : ι) : HahnSeries Γ R

Extract one matrix entry from every Hahn-series coefficient.

@[simp]

theorem Cslib.Circuits.Rational.HahnMatrix.entry_coeff {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Ring R] {ι : Type u_3} (x : HahnSeries Γ (Matrix ι ι R)) (i j : ι) (a : Γ) : (entry x i j).coeff a = x.coeff a i j

theorem Cslib.Circuits.Rational.HahnMatrix.entry_support {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Ring R] {ι : Type u_3} (x : HahnSeries Γ (Matrix ι ι R)) (i j : ι) : (entry x i j).support ⊆ x.support

def Cslib.Circuits.Rational.HahnMatrix.split {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : HahnSeries Γ (Matrix ι ι R) →+* Matrix ι ι (HahnSeries Γ R)

Identify a matrix-valued Hahn series with a matrix of scalar Hahn series.

theorem Cslib.Circuits.Rational.HahnMatrix.split_injective {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {ι : Type u_3} [Fintype ι] [DecidableEq ι] : Function.Injective ⇑split

def Cslib.Circuits.Rational.QuantumMatrices.weyl {K : Type u_1} [Field K] {d : ℕ} (χ : AddChar (ZMod d) K) (a b : ZMod d) : Matrix (ZMod d) (ZMod d) K

The Weyl monomial D^a S^b.

@[simp]

theorem Cslib.Circuits.Rational.QuantumMatrices.weyl_zero {K : Type u_1} [Field K] {d : ℕ} (χ : AddChar (ZMod d) K) : weyl χ 0 0 = 1

theorem Cslib.Circuits.Rational.QuantumMatrices.weyl_mul {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b c e : ZMod d) : weyl χ a b * weyl χ c e = χ (-c * b) • weyl χ (a + c) (b + e)

theorem Cslib.Circuits.Rational.QuantumMatrices.weyl_inverse_right {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : weyl χ a b * χ (-a * b) • weyl χ (-a) (-b) = 1

theorem Cslib.Circuits.Rational.QuantumMatrices.weyl_inverse_left {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : χ (-a * b) • weyl χ (-a) (-b) * weyl χ a b = 1

def Cslib.Circuits.Rational.QuantumMatrices.weylUnit {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : (Matrix (ZMod d) (ZMod d) K)ˣ

A Weyl matrix with its explicit two-sided inverse.

@[simp]

theorem Cslib.Circuits.Rational.QuantumMatrices.weylUnit_val {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : ↑(weylUnit χ a b) = weyl χ a b

@[simp]

theorem Cslib.Circuits.Rational.QuantumMatrices.weylUnit_zero {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : weylUnit χ 0 0 = 1

def Cslib.Circuits.Rational.QuantumMatrices.fourierCoeff {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) (a b : ZMod d) : K

The coefficient of a Weyl matrix in the finite Fourier expansion.

theorem Cslib.Circuits.Rational.QuantumMatrices.fourier_reconstruction {K : Type u_1} [Field K] [CharZero K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (hχ : χ.IsPrimitive) (R : Matrix (ZMod d) (ZMod d) K) : ∑ a : ZMod d, ∑ b : ZMod d, fourierCoeff χ R a b • weyl χ a b = R

Fourier inversion on each cyclic matrix diagonal.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.QuantumLift.Exponents : Type

Lexicographically ordered pairs of integer exponents.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.QuantumLift.Ambient {K : Type u_1} [Field K] {d : ℕ} : Type u_1

Hahn series with matrix coefficients and two integer exponents.

def Cslib.Circuits.Rational.QuantumLift.monomialUnit {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (g : Exponents) : (Matrix (ZMod d) (ZMod d) K)ˣ

The Weyl unit assigned to an exponent pair.

theorem Cslib.Circuits.Rational.QuantumLift.monomialUnit_zero {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : monomialUnit χ 0 = 1

theorem Cslib.Circuits.Rational.QuantumLift.monomialUnit_mul {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (g h : Exponents) : ∃ (c : K), ↑(monomialUnit χ g) * ↑(monomialUnit χ h) = c • ↑(monomialUnit χ (g + h))

@[reducible, inline]

abbrev Cslib.Circuits.Rational.QuantumLift.divisionSubring {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : Subring (HahnSeries Exponents (Matrix (ZMod d) (ZMod d) K))

The Hahn-series subring whose coefficients lie on the Weyl monomial lines.

@[instance_reducible]

noncomputable instance Cslib.Circuits.Rational.QuantumLift.instDivisionRingSubtypeHahnSeriesExponentsMatrixZModMemSubringDivisionSubring {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : DivisionRing ↥(divisionSubring χ)

The division ring structure of divisionSubring.

noncomputable def Cslib.Circuits.Rational.QuantumLift.lift {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) : Ambient

The Fourier lift as a finite Hahn series.

theorem Cslib.Circuits.Rational.QuantumLift.lift_mem {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) : lift χ R ∈ divisionSubring χ

noncomputable def Cslib.Circuits.Rational.QuantumLift.liftD {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) : ↥(divisionSubring χ)

The finite Fourier lift as an element of the division subring.

noncomputable def Cslib.Circuits.Rational.QuantumLift.representation {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : ↥(divisionSubring χ) →+* Matrix (ZMod d) (ZMod d) (HahnSeries Exponents K)

The representation used in the rank-gap argument. Its coefficient field is a commutative Hahn field; all inversion takes place inside the division subring, never by adjoining arbitrary matrix-field scalars.