§3.5, p. 27 — an element-wise nonlinearity after an equivariant map is equivariant, U = σ ∘ B

Proved

GeomDL.Blueprint.pointwise_comp_equivariant

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

equivariancegeometric-deep-learningp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let a group $\mathfrak G$ act on a domain $\Omega$ and on signals by $(\mathfrak g . x)(u) = x(\mathfrak g^{-1}u)$ . Let $B : X(\Omega, C) \to X(\Omega, C')$ be $\mathfrak G$ -equivariant, $B(\mathfrak g . x) = \mathfrak g . B(x)$ , and let $\sigma : C' \to C''$ be an arbitrary map, applied element-wise as $(\boldsymbol\sigma(x))(u) = \sigma(x(u))$ . Then

U := \boldsymbol\sigma \circ B : X(\Omega, C) \to X(\Omega, C''), \qquad U(\mathfrak g . x) = \mathfrak g . U(x)

for all $\mathfrak g \in \mathfrak G$ and $x \in X(\Omega, C)$ .

Nonlinearities applied element-wise preserve equivariance; this is how the blueprint gets expressive equivariant layers.

Formalization Note $C$ , $C'$ , $C''$ are arbitrary types; no linear structure is used.

Preamble

import Mathlib
import Definitions.Def_GeomDL_Blueprint_Defs

Formal statement

namespace GeomDL.Blueprint

/-- Bronstein et al., §3.5, p. 27: if `B : X(Ω, C) → X(Ω, C′)` is `G`-equivariant and
`σ : C′ → C″` is an arbitrary (non-linear) map, then `U := σ ∘ B : X(Ω, C) → X(Ω, C″)` is
`G`-equivariant, where `σ` acts element-wise, `(σ(x))(u) := σ(x(u))`. -/
theorem pointwise_comp_equivariant {G Ω C C' C'' : Type*} [Group G] [MulAction G Ω]
    (B : (Ω → C) → (Ω → C')) (σ : C' → C'') (hB : IsEquivariant (G := G) B) :
    IsEquivariant (G := G) (pointwise (Ω := Ω) σ ∘ B) := by sorry

end GeomDL.Blueprint

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §3.5, p. 27, "Indeed, if B : X(Ω, C) → X(Ω, C′) is G-equivariant ..."

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