§4.2, p. 37 — an n × n matrix commutes with the cyclic shift S if and only if it is circulant

Proved

GeomDL.Grids.commute_shift_iff_circulant

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

circulant-matrixequivariancegeometric-deep-learningp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1shift-operator

Let $n \ge 1$ , let $R$ be a commutative ring, and let $S$ be the right shift on $\mathbb Z_n$ , i.e. the circulant matrix of $(0, 1, 0, \dots, 0)$ . For every $n \times n$ matrix $M$ with entries in $R$ , indexed by $\mathbb Z_n$ ,

M S = S M \iff M = C(\theta) \text{ for some } \theta = (\theta_0, \dots, \theta_{n-1}) \in R^n ,

where $C(\theta) = (\theta_{u - v \bmod n})_{u,v}$ is the circulant matrix of $\theta$ .

The direction " $\Leftarrow$ " is the commutativity of circulant matrices, which gives the shift equivariance of convolution. The direction " $\Rightarrow$ " says that the linear shift-equivariant maps are exactly the convolutions, which lets one define convolution as a translation-equivariant linear operation.

Formalization Note The page states this claim tentatively ("the opposite direction appears to be true as well"); it is a true theorem and is stated here without hedging. It holds over any commutative ring and for every $n \ge 1$ (for $n = 1$ both sides hold for every matrix).

Preamble

import Mathlib
import Definitions.Def_GeomDL_Grids_Defs

open Matrix

Formal statement

namespace GeomDL.Grids
/-- Bronstein et al. §4.2, p. 37: "a matrix is circulant iff it commutes with shift".
An `n × n` matrix `M` over a commutative ring commutes with the right shift `S` if and only
if `M = C(θ)` for some vector `θ`. -/
theorem commute_shift_iff_circulant {R : Type*} [CommRing R] {n : ℕ} [NeZero n]
    (M : Matrix (ZMod n) (ZMod n) R) :
    M * shift R n = shift R n * M ↔ ∃ θ : ZMod n → R, M = circulant θ := by sorry
end GeomDL.Grids

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.2, p. 37, "a matrix is circulant iff it commutes with shift"

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph