Physlib

PhyslibAlpha.AlgebraicFramework.Representation.Schur

Schur's lemma and multiplicity-free covariant channels

There is a recurring pattern in representation theory: once a `G`-invariant object (a representation space, an operator space, a channel's domain) is decomposed into blocks E=⨁iWiE = \bigoplus_i W_i that are individually `G`-invariant and "Schur" (no non-scalar `G`-equivariant self-map), *every* `G`-equivariant endomorphism of the whole space is pinned down block-by-block to a single real scalar per block — instead of classifying arbitrary linear maps on a high-dimensional space, one classifies a handful of numbers. For the qubit, this is exactly why a rotationally covariant channel on the Hermitian 2×22\times2 matrices reduces from "an arbitrary linear self-map of a four-real-dimensional space" to "one real number λ\lambda": the space splits as the scalar sector (spin 00) plus the Pauli-vector sector (spin 11), each Schur.

This file formalizes the reusable core of that argument, deliberately *not* mathlib's representation-theoretic Schur's lemma (see the note below on why): a bare `Prop`-valued Schur hypothesis on a submodule, and the classification theorem for a finite direct sum of Schur blocks.

Why not mathlib's `Representation`/`FDRep` Schur's lemma

`Mathlib.RepresentationTheory.Irreducible` has `Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed`, the sharpest form of Schur's lemma mathlib has (the endomorphism ring of an irreducible representation is exactly the base field), and `Mathlib.CategoryTheory.Preadditive.Schur` / `Mathlib.RepresentationTheory.FDRep` have the abstract Krull–Schmidt-flavoured Hom-space version. Both require the base field to be algebraically closed (`IsAlgClosed k`) — true for `ℂ`, false for `ℝ`. Over `ℝ` this hypothesis genuinely fails in general (a real irreducible representation can have endomorphism ring `ℝ`, `ℂ`, or the quaternions `ℍ`, e.g. the standard real representation of the circle group on `ℝ²` is irreducible with endomorphism ring `ℂ`, not `ℝ` — rotation-by-90° is a non-scalar equivariant endomorphism). The qubit's Pauli-vector sector genuinely is a "real type" representation (endomorphism ring `ℝ`), but this is *extra* representation-theoretic input beyond generic Schur, not something `IsAlgClosed`-Schur gives for free over `ℝ`. Moreover this codebase's `E`/`Symmetry E` (`OrderUnit/Symmetry.lean`) is a bare order-unit module with a group of order-automorphisms, not mathlib's `Representation k G V` structure (a genuine `k[G]`-module) — bridging the two would cost more than it buys. So the Schur hypothesis below is taken as an explicit, minimal `Prop` on a `Submodule`, to be discharged per-block by whatever means are available (cited from elsewhere or proved directly), rather than derived from a general representation-theoretic classification result.

Main definitions

- `IsSchurBlock smul W` : the Schur hypothesis for a submodule `W`, relative to an action `smul : G → E → E` — every linear self-map of `E` that is equivariant on `W` and preserves `W` acts as a single scalar on all of `W`.

Main results

- `exists_scalar_of_isSchurBlock` : the multiplicity-free classification theorem — given a finite family of Schur blocks decomposing `E` as an internal direct sum, each individually `G`-invariant, every `G`-equivariant linear endomorphism of `E` that preserves every block acts on each block `W i` as `c i • id` for some real scalar `c i`. - `UnitalPositiveLinearMap.IsCovariant.exists_scalar_of_isSchurBlock` : the same theorem phrased for a covariant channel `φ : E →ₚ₁[ℝ] E` (`Measurement/Covariance.lean`), the form that plugs directly into this codebase's existing covariance notion.

The Schur hypothesis on a single block

The multiplicity-free classification theorem

Connecting to covariant channels

`Measurement/Covariance.lean` phrases covariance for a channel `φ : E →ₚ₁[ℝ] E` intertwining a symmetry action `ρ : G →* Symmetry E` with itself, via `UnitalPositiveLinearMap.IsCovariant`. The underlying linear map of such a channel is exactly a `G`-equivariant endomorphism of `E` for the action `g • x := (ρ g).1 x`, so the classification theorem above applies directly.

3 declarations

definition

WW is a Schur block for the action of GG

Let EE be a real vector space and W⊆EW \subseteq E be a submodule. Given an action smul:G×E→E\text{smul} : G \times E \to E of a group GG on EE (denoted by g⋅xg \cdot x), we say that WW is a **Schur block** if every linear endomorphism f:E→Ef: E \to E that satisfies the following two conditions: 1. ff is GG-equivariant on WW: for all g∈Gg \in G and x∈Wx \in W, f(g⋅x)=g⋅f(x)f(g \cdot x) = g \cdot f(x); 2. ff preserves WW: for all x∈Wx \in W, f(x)∈Wf(x) \in W; acts as a scalar on WW. That is, there exists a real scalar c∈Rc \in \mathbb{R} such that f(x)=cxf(x) = c x for all x∈Wx \in W. This property captures the abstract requirement that every GG-equivariant self-map of an irreducible real representation is a scalar, which is used as a hypothesis for decomposing operators block-by-block.

theorem

Multiplicity-free classification of GG-equivariant endomorphisms on Schur blocks

Let EE be a real vector space and GG be a group with an action on EE denoted by g⋅xg \cdot x. Suppose EE is the internal direct sum of a family of submodules {Wi}i∈ι\{W_i\}_{i \in \iota}, denoted E=⨁i∈ιWiE = \bigoplus_{i \in \iota} W_i. Assume the following conditions hold: 1. Each submodule WiW_i is invariant under the action of GG (i.e., for all g∈Gg \in G and x∈Wix \in W_i, g⋅x∈Wig \cdot x \in W_i). 2. Each WiW_i satisfies the Schur hypothesis (is a "Schur block"), meaning any GG-equivariant linear endomorphism of EE that preserves WiW_i acts as a scalar on WiW_i. Then, for any GG-equivariant linear endomorphism f:E→Ef: E \to E that preserves each block WiW_i (i.e., f(Wi)⊆Wif(W_i) \subseteq W_i for all i∈ιi \in \iota), there exists a family of real scalars {ci}i∈ι\{c_i\}_{i \in \iota} such that for every ii and every x∈Wix \in W_i, the action of ff is given by scalar multiplication: f(x)=cixf(x) = c_i x.

theorem

A covariant channel ϕ\phi preserving Schur blocks WiW_i acts as ϕ∣Wi=ciid\phi|_{W_i} = c_i \text{id}

Let EE be a real vector space and GG be a group acting on EE via a symmetry representation ρ:G→Symmetry(E)\rho : G \to \text{Symmetry}(E). Let ϕ:E→E\phi : E \to E be a covariant channel (a unital positive linear map) that intertwines the action of GG, such that ϕ(ρ(g)x)=ρ(g)ϕ(x)\phi(\rho(g)x) = \rho(g)\phi(x) for all g∈Gg \in G and x∈Ex \in E. Suppose EE is decomposed into an internal direct sum of submodules WiW_i (where ii ranges over an index set II), denoted E=⨁i∈IWiE = \bigoplus_{i \in I} W_i, such that: 1. Each submodule WiW_i is invariant under the action of GG, i.e., ρ(g)x∈Wi\rho(g)x \in W_i for all g∈Gg \in G and x∈Wix \in W_i. 2. Each WiW_i is a **Schur block**, meaning that any GG-equivariant linear endomorphism of EE that preserves WiW_i acts as a scalar on WiW_i. 3. The map ϕ\phi preserves each block, i.e., ϕ(x)∈Wi\phi(x) \in W_i for all x∈Wix \in W_i. Then there exists a family of real scalars {ci}i∈I\{c_i\}_{i \in I} such that for every block ii and every x∈Wix \in W_i, the map acts as ϕ(x)=cix\phi(x) = c_i x.