The invariant form on a permutation representation

A permutation representation k[X] of a group G on a G-set X carries a canonical bilinear form, the one for which the standard basis single x 1 is orthonormal: the pairing of v and w is the sum of v x * w x over the (finite) support of v. Because the action of a group element permutes the standard basis, this permutation form is invariant, and the orthogonal complement of an invariant submodule is again invariant.

Over a linearly ordered commutative semiring with ExistsAddOfLE the form is positive definite, so its restriction to any submodule is nondegenerate. The ExistsAddOfLE assumption says that a ≤ b implies b = a + c for some c; it holds for ordered rings and for ℕ. Over an ordered field, when X is finite, the orthogonal complement of a subrepresentation is a genuine complement. This exhibits a canonical invariant complement of a subrepresentation of a permutation representation: one that needs no averaging operator and no hypothesis on G, and whose orthogonality relation is a tool in its own right. An ordered field has characteristic zero, so the complementation statements say nothing about positive characteristic; what they drop relative to Maschke's theorem is finiteness of G and invertibility of |G|.

Main definitions

• TauCeti.permutationForm: the bilinear form on k[X] making the standard basis orthonormal.
• TauCeti.orthogonalSubrepresentation: the orthogonal complement of a subrepresentation of a permutation representation, as a subrepresentation.

Main results

• TauCeti.permutationForm_single_single: the standard basis is orthonormal.
• TauCeti.permutationForm_isSymm and TauCeti.permutationForm_nondegenerate: the form is symmetric and nondegenerate over any commutative semiring.
• TauCeti.permutationForm_ofMulAction_invariant: the action of a group element preserves the form, and TauCeti.permutationForm_ofMulAction_left moves that action across the form by inverting it.
• TauCeti.orthogonal_mem_invtSubmodule: the orthogonal complement of an invariant submodule of a permutation representation is invariant.
• TauCeti.permutationForm_self_pos and TauCeti.permutationForm_restrict_nondegenerate: over a linearly ordered commutative semiring with ExistsAddOfLE the form is positive definite, hence nondegenerate on every submodule.
• TauCeti.isCompl_orthogonalSubrepresentation: over an ordered field, and for a finite G-set, a subrepresentation is complemented by its orthogonal complement.

Implementation notes

The form is defined on MonoidAlgebra k X rather than on X →₀ k because that is the module Mathlib's Representation.ofMulAction acts on. Here X carries no multiplication and the monoid-algebra product plays no role; only the free module on X and its standard basis do. For a finite X the form is the one with identity Gram matrix, which under the identification of k[X] with X → k is Mathlib's Matrix.toBilin' 1; the definition below is stated with Finsupp.sum so that it needs no finiteness and no DecidableEq X.

Positive definiteness, not invertibility of |G|, is what drives the complementation statements, which is why they ask for an ordered field rather than for a finite group. In particular nothing below reproves Maschke's theorem: the content is that the complement can be taken orthogonal, so that a submodule and its complement are separated by an explicit pairing.

The orthogonal-complement half of this file is the bilinear-form transcription of an existing TauCeti development: ofMulAction_mem_orthogonal, orthogonal_mem_invtSubmodule, orthogonalSubrepresentation, toSubmodule_orthogonalSubrepresentation and isCompl_orthogonalSubrepresentation follow, statement for statement and proof for proof, their namesakes in TauCeti.RepresentationTheory.Continuous.InvariantComplement, with IsUnitary.inner_map_right replaced by permutationForm_ofMulAction_left and Submodule.isCompl_orthogonal by LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate. The two cannot be unified: that file works over an inner-product space, which is unavailable over ℚ.

References

• TauCeti.RepresentationTheory.Continuous.InvariantComplement, the unitary orthogonal-complement API this file adapts to a bilinear form, as described in the implementation notes above.
• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 1, where this form is introduced on the permutation module of a Young subgroup and used for the submodule theorem.
• Schur-Weyl roadmap, Layer 3, which asks for the tabloid bilinear form and its orthogonality API.

The permutation form

noncomputable def TauCeti.permutationForm (k : Type u_1) [CommSemiring k] (X : Type u_2) : LinearMap.BilinForm k (MonoidAlgebra k X)

The permutation form on k[X]: the bilinear form for which the standard basis of k[X] is orthonormal. On a pair of elements it is the sum of the products of matching coefficients.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.permutationForm_apply {k : Type u_1} [CommSemiring k] {X : Type u_2} (v w : MonoidAlgebra k X) : ((permutationForm k X) v) w = v.coeff.sum fun (x : X) (a : k) => a * w.coeff x

The permutation form pairs two elements by summing the products of matching coefficients over the support of the left argument.

@[simp]

theorem TauCeti.permutationForm_single_left {k : Type u_1} [CommSemiring k] {X : Type u_2} (x : X) (a : k) (w : MonoidAlgebra k X) : ((permutationForm k X) (MonoidAlgebra.single x a)) w = a * w.coeff x

Pairing with a standard basis vector reads off a coefficient.

theorem TauCeti.permutationForm_comm {k : Type u_1} [CommSemiring k] {X : Type u_2} (v w : MonoidAlgebra k X) : ((permutationForm k X) v) w = ((permutationForm k X) w) v

The permutation form is symmetric: both sides are the sum of v x * w x over the union of the two supports.

theorem TauCeti.permutationForm_isSymm {k : Type u_1} [CommSemiring k] {X : Type u_2} : (permutationForm k X).IsSymm

The permutation form is symmetric.

theorem TauCeti.permutationForm_isRefl {k : Type u_1} [CommSemiring k] {X : Type u_2} : (permutationForm k X).IsRefl

The permutation form is reflexive, so its orthogonal complement has no chirality.

@[simp]

theorem TauCeti.permutationForm_single_right {k : Type u_1} [CommSemiring k] {X : Type u_2} (v : MonoidAlgebra k X) (x : X) (a : k) : ((permutationForm k X) v) (MonoidAlgebra.single x a) = v.coeff x * a

Pairing with a standard basis vector on the right reads off a coefficient.

theorem TauCeti.permutationForm_single_single {k : Type u_1} [CommSemiring k] {X : Type u_2} (x y : X) [Decidable (x = y)] (a b : k) : ((permutationForm k X) (MonoidAlgebra.single x a)) (MonoidAlgebra.single y b) = if x = y then a * b else 0

The standard basis of k[X] is orthonormal for the permutation form.

theorem TauCeti.permutationForm_separatingLeft {k : Type u_1} [CommSemiring k] {X : Type u_2} : LinearMap.SeparatingLeft (permutationForm k X)

An element pairing to zero with everything on the right is zero: it is enough to pair it with the standard basis vectors.

theorem TauCeti.permutationForm_nondegenerate {k : Type u_1} [CommSemiring k] {X : Type u_2} : (permutationForm k X).Nondegenerate

The permutation form is nondegenerate: an element pairing to zero with every standard basis vector has all coefficients zero.

Positive definiteness over an ordered semiring

theorem TauCeti.permutationForm_self_pos {k : Type u_1} [CommSemiring k] [LinearOrder k] [IsStrictOrderedRing k] [ExistsAddOfLE k] {X : Type u_2} {v : MonoidAlgebra k X} (hv : v ≠ 0) : 0 < ((permutationForm k X) v) v

Over a linearly ordered commutative semiring with ExistsAddOfLE, the permutation form is positive definite.

@[simp]

theorem TauCeti.permutationForm_self_eq_zero_iff {k : Type u_1} [CommSemiring k] [LinearOrder k] [IsStrictOrderedRing k] [ExistsAddOfLE k] {X : Type u_2} {v : MonoidAlgebra k X} : ((permutationForm k X) v) v = 0 ↔ v = 0

Over a linearly ordered commutative semiring with ExistsAddOfLE, an element is isotropic for the permutation form only if it is zero.

theorem TauCeti.permutationForm_restrict_nondegenerate {k : Type u_1} [CommSemiring k] [LinearOrder k] [IsStrictOrderedRing k] [ExistsAddOfLE k] {X : Type u_2} (W : Submodule k (MonoidAlgebra k X)) : ((permutationForm k X).restrict W).Nondegenerate

A positive definite form stays nondegenerate on every submodule, which is what makes the orthogonal complement below a genuine complement.

Invariance under a permutation action

@[simp]

theorem TauCeti.permutationForm_ofMulAction_invariant {k : Type u_1} [CommSemiring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] (g : G) (v w : MonoidAlgebra k X) : ((permutationForm k X) (((Representation.ofMulAction k G X) g) v)) (((Representation.ofMulAction k G X) g) w) = ((permutationForm k X) v) w

The action of a group element permutes the standard basis of k[X], so it preserves the permutation form.

theorem TauCeti.permutationForm_ofMulAction_left {k : Type u_1} [CommSemiring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] (g : G) (v w : MonoidAlgebra k X) : ((permutationForm k X) (((Representation.ofMulAction k G X) g) v)) w = ((permutationForm k X) v) (((Representation.ofMulAction k G X) g⁻¹) w)

Moving the action of a group element across the permutation form replaces it by its inverse. This is the shape in which invariance is used to compare a submodule with an orthogonal complement.

theorem TauCeti.ofMulAction_mem_orthogonal {k : Type u_1} [CommSemiring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] {W : Submodule k (MonoidAlgebra k X)} (hW : ∀ (g : G), ∀ v ∈ W, ((Representation.ofMulAction k G X) g) v ∈ W) (g : G) {v : MonoidAlgebra k X} (hv : v ∈ (permutationForm k X).orthogonal W) : ((Representation.ofMulAction k G X) g) v ∈ (permutationForm k X).orthogonal W

The action carries the orthogonal complement of an invariant submodule into itself.

theorem TauCeti.orthogonal_mem_invtSubmodule {k : Type u_1} [CommSemiring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] {W : Submodule k (MonoidAlgebra k X)} (hW : W ∈ (Representation.ofMulAction k G X).invtSubmodule) : (permutationForm k X).orthogonal W ∈ (Representation.ofMulAction k G X).invtSubmodule

Invariant orthogonal complements. The orthogonal complement of an invariant submodule of a permutation representation is again invariant.

noncomputable def TauCeti.orthogonalSubrepresentation {k : Type u_1} [CommSemiring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] (σ : Subrepresentation (Representation.ofMulAction k G X)) : Subrepresentation (Representation.ofMulAction k G X)

The orthogonal complement of a subrepresentation of a permutation representation, as a subrepresentation.

Equations

• TauCeti.orthogonalSubrepresentation σ = { toSubmodule := (TauCeti.permutationForm k X).orthogonal σ.toSubmodule, apply_mem_toSubmodule := ⋯ }

@[simp]

theorem TauCeti.toSubmodule_orthogonalSubrepresentation {k : Type u_1} [CommSemiring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] (σ : Subrepresentation (Representation.ofMulAction k G X)) : (orthogonalSubrepresentation σ).toSubmodule = (permutationForm k X).orthogonal σ.toSubmodule

The underlying submodule of the orthogonal complement of a subrepresentation.

Complementation over an ordered field

theorem TauCeti.isCompl_orthogonalSubrepresentation {k : Type u_1} [Field k] [LinearOrder k] [IsStrictOrderedRing k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] [Finite X] (σ : Subrepresentation (Representation.ofMulAction k G X)) : IsCompl σ (orthogonalSubrepresentation σ)

Invariant complements without averaging. Over an ordered field a subrepresentation of the permutation representation on a finite G-set is complemented by its orthogonal complement. No hypothesis on G is needed: neither finiteness nor invertibility of |G|. The ordered field is of characteristic zero, so this is not a statement about positive characteristic.