Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Equivariant Record Symmetry No-Go

Abstract

Equivariant Hermitian idempotents are trivial under irreducible symmetry.

Theorem 1.1 (Idempotent no-go).

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/RecordSymmetryNoGo.equivariant_selfAdjoint_idempotent_eq_zero_or_one (✓ std3). ∎

Citation. Pavel Etingof, Oleg Golberg, Sebastian Hensel, Tiankai Liu, Alex Schwendner, Dmitry Vaintrob, Elena Yudovina (2009). Introduction to representation theory. URL: https://arxiv.org/abs/0901.0827.

Commentary.

Schur scalarity followed by the scalar equation r squared equals r gives the two values.

Theorem 1.2 (Reverse obstruction).

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/RecordSymmetryNoGo.nontrivial_equivariant_selfAdjoint_idempotent_implies_reducible (✓ std3). ∎

Citation. Pavel Etingof, Oleg Golberg, Sebastian Hensel, Tiankai Liu, Alex Schwendner, Dmitry Vaintrob, Elena Yudovina (2009). Introduction to representation theory. URL: https://arxiv.org/abs/0901.0827.

Commentary.

This is the contrapositive of the idempotent no-go.

Theorem 1.3 (Two-record consequence).

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/RecordSymmetryNoGo.two_nonzero_orthogonal_equivariant_records_imply_reducible (✓ std3). ∎

Citation. Pavel Etingof, Oleg Golberg, Sebastian Hensel, Tiankai Liu, Alex Schwendner, Dmitry Vaintrob, Elena Yudovina (2009). Introduction to representation theory. URL: https://arxiv.org/abs/0901.0827.

Commentary.

The first projection must be identity under irreducibility, and orthogonality then kills the second.

References