The augmentation subrepresentation of a free-module action

For a monoid action on X, the augmentation subrepresentation of k[X] consists of the vectors whose coefficients sum to zero. For a group action on finite X, the sum of the standard basis vectors spans an invariant subrepresentation, called the invariant line. Both constructions are defined over any semiring. If X is nonempty, the invariant line is equivalent to the trivial representation on k: every coordinate of a vector in the line is its scalar coefficient.

For finite X over a ring satisfying the strong rank condition, the augmentation subrepresentation has rank |X| - 1. Over any ring where |X| is a unit, the invariant line complements it. The equivalence TauCeti.ofMulActionEquivProdAugmentation expresses this splitting: its first component is the average of the coefficients, and its second subtracts that multiple of the sum of the standard basis. For empty X, both subrepresentations are zero and are still complementary.

Over a field, the character of the augmentation subrepresentation is the character of the induced free-module action minus the trivial character, provided X is finite and nonempty. The identity holds even when the characteristic divides |X|, so the invariant line is not a complement. These constructions underlie the standard representation of the symmetric group.

Main definitions and results

• TauCeti.augmentationSubrepresentation: the kernel of the coefficient sum.
• TauCeti.permutationSum and TauCeti.invariantLine: the sum of the standard basis and its span.
• TauCeti.invariantLineEquivTrivial: the invariant line as the trivial representation on k.
• TauCeti.MonoidAlgebra.ker_sumCoords_basis_eq_span: the augmentation kernel is spanned by differences of standard basis vectors from a fixed one.
• TauCeti.isCompl_invariantLine_augmentationSubrepresentation_iff: the two subrepresentations are complementary exactly when X is empty or its cardinality is a unit in the coefficient ring.
• TauCeti.ofMulActionEquivProdAugmentation: the explicit splitting as trivial plus augmentation.
• TauCeti.finrank_augmentationSubrepresentation: the dimension is |X| - 1.
• TauCeti.character_augmentationSubrepresentation: the character is the free-module character minus 1.

Implementation notes

The augmentation is Module.Basis.sumCoords for MonoidAlgebra.basis X k. This linear map requires no multiplication on X, unlike the ring homomorphism augmenting a monoid algebra. The two maps agree when X is a monoid: both send single x a to a.

References

• J.-P. Serre, Linear Representations of Finite Groups, §2.3.

The augmentation subrepresentation

@[simp]

theorem TauCeti.sumCoords_basis_ofMulAction (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Monoid G] [MulAction G X] (g : G) (v : MonoidAlgebra k X) : (MonoidAlgebra.basis X k).sumCoords (((Representation.ofMulAction k G X) g) v) = (MonoidAlgebra.basis X k).sumCoords v

The coefficient sum is invariant under the induced action on the free module.

noncomputable def TauCeti.augmentationSubrepresentation (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Monoid G] [MulAction G X] : Subrepresentation (Representation.ofMulAction k G X)

The augmentation subrepresentation of k[X]: the elements whose coefficients sum to zero.

Equations

• TauCeti.augmentationSubrepresentation k G X = { toSubmodule := (MonoidAlgebra.basis X k).sumCoords.ker, apply_mem_toSubmodule := ⋯ }

@[simp]

theorem TauCeti.toSubmodule_augmentationSubrepresentation (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Monoid G] [MulAction G X] : (augmentationSubrepresentation k G X).toSubmodule = (MonoidAlgebra.basis X k).sumCoords.ker

@[simp]

theorem TauCeti.mem_augmentationSubrepresentation_iff {k : Type u_1} [Semiring k] {G : Type u_2} {X : Type u_3} [Monoid G] [MulAction G X] {v : MonoidAlgebra k X} : v ∈ augmentationSubrepresentation k G X ↔ (MonoidAlgebra.basis X k).sumCoords v = 0

theorem TauCeti.single_sub_single_mem_augmentationSubrepresentation {k : Type u_1} [Ring k] {G : Type u_2} {X : Type u_3} [Monoid G] [MulAction G X] (x y : X) : MonoidAlgebra.single x 1 - MonoidAlgebra.single y 1 ∈ augmentationSubrepresentation k G X

A difference of two standard basis vectors has vanishing augmentation.

The invariant line

noncomputable def TauCeti.permutationSum (k : Type u_1) [Semiring k] (X : Type u_2) [Fintype X] : MonoidAlgebra k X

The sum of the standard basis of k[X], for a finite index type.

Equations

• TauCeti.permutationSum k X = ∑ x : X, MonoidAlgebra.single x 1

@[simp]

theorem TauCeti.coeff_permutationSum {k : Type u_1} [Semiring k] {X : Type u_2} [Fintype X] (x : X) : (permutationSum k X).coeff x = 1

theorem TauCeti.sumCoords_basis_permutationSum {k : Type u_1} [Semiring k] {X : Type u_2} [Fintype X] : (MonoidAlgebra.basis X k).sumCoords (permutationSum k X) = ↑(Fintype.card X)

The augmentation of the sum of the standard basis is the cardinality of the index type.

Deliberately not @[simp]: simp already proves this from TauCeti.coeff_permutationSum and the generic basis API, so tagging it would be a simpNF violation.

theorem TauCeti.permutationSum_ne_zero {k : Type u_1} [Semiring k] {X : Type u_2} [Fintype X] [Nonempty X] [Nontrivial k] : permutationSum k X ≠ 0

For nonempty X and nontrivial coefficients, the sum of the standard basis is nonzero.

@[simp]

theorem TauCeti.ofMulAction_permutationSum (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] (g : G) : ((Representation.ofMulAction k G X) g) (permutationSum k X) = permutationSum k X

The sum of the standard basis is fixed by the group action.

noncomputable def TauCeti.invariantLine (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] : Subrepresentation (Representation.ofMulAction k G X)

The invariant line of k[X]: the line spanned by the sum of the standard basis, as a subrepresentation.

Equations

• TauCeti.invariantLine k G X = { toSubmodule := k ∙ TauCeti.permutationSum k X, apply_mem_toSubmodule := ⋯ }

@[simp]

theorem TauCeti.toSubmodule_invariantLine (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] : (invariantLine k G X).toSubmodule = k ∙ permutationSum k X

@[simp]

theorem TauCeti.toRepresentation_invariantLine (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] : (invariantLine k G X).toRepresentation = Representation.trivial k G ↥(invariantLine k G X).toSubmodule

The group acts trivially on the invariant line.

@[simp]

theorem TauCeti.mem_invariantLine_iff {k : Type u_1} [Semiring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] [Fintype X] {v : MonoidAlgebra k X} : v ∈ invariantLine k G X ↔ ∃ (c : k), c • permutationSum k X = v

The elements of the invariant line are exactly the multiples of the sum of the standard basis.

The invariant line as the trivial representation

noncomputable def TauCeti.invariantLineEquivTrivial (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] [Nonempty X] : (invariantLine k G X).toRepresentation.Equiv (Representation.trivial k G k)

For a nonempty index type, the invariant line is the trivial representation on the scalars. The inverse sends a scalar to that multiple of the sum of the standard basis.

Equations

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

@[simp]

theorem TauCeti.coe_invariantLineEquivTrivial_symm_apply (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] [Nonempty X] (c : k) : ↑((invariantLineEquivTrivial k G X).symm c) = c • permutationSum k X

The scalar c names the multiple c • permutationSum k X of the sum of the standard basis.

@[simp]

theorem TauCeti.invariantLineEquivTrivial_apply_smul (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] [Nonempty X] (v : ↥(invariantLine k G X).toSubmodule) : (invariantLineEquivTrivial k G X) v • permutationSum k X = ↑v

Conversely, the scalar naming a vector of the invariant line is its coordinate along the sum of the standard basis: that multiple of the sum is the vector again.

@[simp]

theorem TauCeti.coeff_eq_invariantLineEquivTrivial (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] [Nonempty X] (v : ↥(invariantLine k G X).toSubmodule) (x : X) : (↑v).coeff x = (invariantLineEquivTrivial k G X) v

Every coordinate of a vector in the invariant line is its corresponding scalar.

@[simp]

theorem TauCeti.finrank_invariantLine (k : Type u_1) [Semiring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] [Nonempty X] [StrongRankCondition k] : Module.finrank k ↥(invariantLine k G X).toSubmodule = 1

The invariant line has rank one over a semiring satisfying the strong rank condition.

The dimension of the augmentation subrepresentation

@[simp]

theorem TauCeti.finrank_augmentationSubrepresentation {k : Type u_1} [Ring k] [StrongRankCondition k] {G : Type u_2} {X : Type u_3} [Monoid G] [MulAction G X] [Fintype X] : Module.finrank k ↥(augmentationSubrepresentation k G X).toSubmodule = Fintype.card X - 1

The augmentation subrepresentation has dimension one less than the cardinality of X. For an empty X both sides are zero, the subtraction being truncated.

The splitting

theorem TauCeti.isCompl_invariantLine_augmentationSubrepresentation {k : Type u_1} [Ring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] [Fintype X] (h : IsEmpty X ∨ IsUnit ↑(Fintype.card X)) : IsCompl (invariantLine k G X) (augmentationSubrepresentation k G X)

The invariant line and augmentation subrepresentation are complementary when the index set is empty or its cardinality is a unit in the coefficient ring.

theorem TauCeti.isCompl_invariantLine_augmentationSubrepresentation_iff {k : Type u_1} [Ring k] {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] [Fintype X] : IsCompl (invariantLine k G X) (augmentationSubrepresentation k G X) ↔ IsEmpty X ∨ IsUnit ↑(Fintype.card X)

The invariant line complements the augmentation subrepresentation exactly when the index set is empty or its cardinality is a unit in the coefficient ring.

The splitting as trivial plus augmentation

noncomputable def TauCeti.ofMulActionEquivProdAugmentation (k : Type u_1) [Ring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] (h : IsUnit ↑(Fintype.card X)) : (Representation.ofMulAction k G X).Equiv ((Representation.trivial k G k).prod (augmentationSubrepresentation k G X).toRepresentation)

When |X| is a unit in a ring, the permutation representation splits as the trivial representation on the scalars and the augmentation subrepresentation. The scalar component multiplies the sum of the standard basis.

Equations

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

@[simp]

theorem TauCeti.ofMulActionEquivProdAugmentation_symm_apply (k : Type u_1) [Ring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] (h : IsUnit ↑(Fintype.card X)) (v : k × ↥(augmentationSubrepresentation k G X).toSubmodule) : (ofMulActionEquivProdAugmentation k G X h).symm v = v.1 • permutationSum k X + ↑v.2

The splitting adds a multiple of the sum of the standard basis to a vector of the augmentation subrepresentation.

@[simp]

theorem TauCeti.ofMulActionEquivProdAugmentation_apply_fst (k : Type u_1) [Ring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] (h : IsUnit ↑(Fintype.card X)) (v : MonoidAlgebra k X) : ((ofMulActionEquivProdAugmentation k G X h) v).1 = (MonoidAlgebra.basis X k).sumCoords v * Ring.inverse ↑(Fintype.card X)

The scalar component is the coefficient sum times the ring inverse of the cardinality.

@[simp]

theorem TauCeti.coe_ofMulActionEquivProdAugmentation_apply_snd (k : Type u_1) [Ring k] (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] [Fintype X] (h : IsUnit ↑(Fintype.card X)) (v : MonoidAlgebra k X) : ↑((ofMulActionEquivProdAugmentation k G X h) v).2 = v - ((MonoidAlgebra.basis X k).sumCoords v * Ring.inverse ↑(Fintype.card X)) • permutationSum k X

The augmentation component subtracts the average coefficient from every coordinate.

The character of the augmentation subrepresentation

@[simp]

theorem TauCeti.character_augmentationSubrepresentation {k : Type u_1} [Field k] {G : Type u_2} {X : Type u_3} [Monoid G] [MulAction G X] [Finite X] [Nonempty X] (g : G) : (augmentationSubrepresentation k G X).toRepresentation.character g = (Representation.ofMulAction k G X).character g - 1

The character of the augmentation subrepresentation is the character of k[X] less 1. The subtracted 1 is the trivial quotient k[X] / ker(augmentation) ≃ k, so nothing about |X| in k is needed: the identity holds in every characteristic, including the one dividing |X|, where the invariant line is not a complement.

For a monoid action the subtracted 1 is the trivial quotient: the character of k[X] counts fixed points, so the character here is the number of fixed points less one.