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.

Over a ring, the coefficient sum is a morphism from the permutation representation to the trivial representation. When X is nonempty its kernel inclusion gives the short exact sequence 0 → ker(sum) → k[X] → k → 0, whether or not it splits equivariantly.

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. Likewise its characteristic polynomial times X - 1 is the characteristic polynomial on k[X]. These constructions underlie the standard representation of the symmetric group.

Main definitions and results

• TauCeti.augmentationSubrepresentation: the kernel of the coefficient sum.
• TauCeti.permutationAugmentation: the coefficient sum as a representation morphism.
• TauCeti.permutationAugmentationSequence_shortExact: the augmentation sequence is short exact when the permutation set is nonempty.
• 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.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.augmentationProjectionOfIsUnit: the equivariant projection onto the augmentation subrepresentation along the invariant line.
• TauCeti.dualRestrict_augmentationSubrepresentation_eq_zero_iff: the linear forms vanishing on the augmentation subrepresentation are the multiples of the coefficient sum.
• TauCeti.finrank_augmentationSubrepresentation: the dimension is |X| - 1.
• TauCeti.character_augmentationSubrepresentation: the character is the free-module character minus 1.
• TauCeti.charpoly_augmentationSubrepresentation_mul_X_sub_one: the characteristic polynomial times X - 1 is the free-module characteristic polynomial.

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.

@[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

noncomputable def TauCeti.permutationAugmentation (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : Rep.ofMulAction k G X ⟶ Rep.trivial k G k

The coefficient sum as a morphism from the permutation representation to the trivial representation on the scalars.

@[simp]

theorem TauCeti.permutationAugmentation_apply (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] (v : MonoidAlgebra k X) : (Rep.Hom.hom (permutationAugmentation k G X)) v = (MonoidAlgebra.basis X k).sumCoords v

The permutation augmentation evaluates to the sum of the coefficients.

theorem TauCeti.forget₂_map_permutationAugmentation (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : (CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).map (permutationAugmentation k G X) = CategoryTheory.CategoryStruct.comp (MonoidAlgebra.coeffLinearEquiv k).toModuleIso.hom (ModuleCat.ofHom (Finsupp.linearCombination k fun (x : X) => 1))

Read on coefficients, the permutation augmentation sums the coefficients.

instance TauCeti.permutationAugmentation_epi (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] [Nonempty X] : CategoryTheory.Epi (permutationAugmentation k G X)

For a nonempty permutation set, augmentation is surjective.

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.

instance TauCeti.instFiniteSubtypeMonoidAlgebraMemSubmoduleToSubmoduleAugmentationSubrepresentationOfFinite {k : Type u_1} [Ring k] {G : Type u_2} {X : Type u_3} [Monoid G] [MulAction G X] [Finite X] : Module.Finite k ↥(augmentationSubrepresentation k G X).toSubmodule

The augmentation subrepresentation on a finite set is finitely generated over any ring.

Linear forms on the augmentation subrepresentation

@[simp]

theorem TauCeti.dualRestrict_augmentationSubrepresentation_sumCoords {k : Type u_1} [CommRing k] {G : Type u_2} {X : Type u_3} [Monoid G] [MulAction G X] : (augmentationSubrepresentation k G X).toSubmodule.dualRestrict (MonoidAlgebra.basis X k).sumCoords = 0

The coefficient sum vanishes on the augmentation subrepresentation.

theorem TauCeti.dualRestrict_augmentationSubrepresentation_eq_zero_iff {k : Type u_1} [CommRing k] {G : Type u_2} {X : Type u_3} [Monoid G] [MulAction G X] {φ : Module.Dual k (MonoidAlgebra k X)} : (augmentationSubrepresentation k G X).toSubmodule.dualRestrict φ = 0 ↔ φ ∈ k ∙ (MonoidAlgebra.basis X k).sumCoords

A linear form on k[X] vanishes on the augmentation subrepresentation exactly when it is a multiple of the coefficient sum. No hypothesis on k or X is needed.

The augmentation sequence

noncomputable def TauCeti.permutationAugmentationSequence (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : CategoryTheory.ShortComplex (Rep k G)

The permutation augmentation sequence ker(sum) → k[X] → k.

theorem TauCeti.permutationAugmentationSequence_def (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : permutationAugmentationSequence k G X = { X₁ := Rep.of (augmentationSubrepresentation k G X).toRepresentation, X₂ := Rep.of (Representation.ofMulAction k G X), X₃ := Rep.trivial k G k, f := Rep.ofHom (augmentationSubrepresentation k G X).subtype, g := permutationAugmentation k G X, zero := ⋯ }

The permutation augmentation sequence consists of the inclusion and coefficient sum.

@[simp]

theorem TauCeti.permutationAugmentationSequence_X₁ (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : (permutationAugmentationSequence k G X).X₁ = Rep.of (augmentationSubrepresentation k G X).toRepresentation

The first term of the permutation augmentation sequence is the augmentation subrepresentation.

@[simp]

theorem TauCeti.permutationAugmentationSequence_X₂ (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : (permutationAugmentationSequence k G X).X₂ = Rep.ofMulAction k G X

The middle term of the permutation augmentation sequence is the permutation representation.

@[simp]

theorem TauCeti.permutationAugmentationSequence_X₃ (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : (permutationAugmentationSequence k G X).X₃ = Rep.trivial k G k

The last term of the permutation augmentation sequence is the trivial representation on k.

@[simp]

theorem TauCeti.permutationAugmentationSequence_f (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : (permutationAugmentationSequence k G X).f ≍ Rep.ofHom (augmentationSubrepresentation k G X).subtype

The first map of the permutation augmentation sequence is the kernel inclusion.

@[simp]

theorem TauCeti.permutationAugmentationSequence_g (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] : (permutationAugmentationSequence k G X).g ≍ permutationAugmentation k G X

The second map of the permutation augmentation sequence is the coefficient sum.

theorem TauCeti.permutationAugmentationSequence_shortExact (k : Type u) [Ring k] (G : Type u_1) (X : Type u) [Monoid G] [MulAction G X] [Nonempty X] : (permutationAugmentationSequence k G X).ShortExact

The augmentation sequence on a nonempty permutation set is short exact. It need not split equivariantly when the cardinality of the set is not invertible.

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.

@[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.

@[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.

@[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.

@[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.

noncomputable def TauCeti.augmentationProjectionOfIsUnit (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)) : MonoidAlgebra k X →ₗ[k] ↥(augmentationSubrepresentation k G X).toSubmodule

When |X| is a unit in a ring, the projection of k[X] onto the augmentation subrepresentation along the invariant line: the second component of the splitting TauCeti.ofMulActionEquivProdAugmentation. Unlike TauCeti.augmentationProjection, which projects along the line of a chosen basis vector, it is equivariant.

theorem TauCeti.augmentationProjectionOfIsUnit_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 : MonoidAlgebra k X) : (augmentationProjectionOfIsUnit k G X h) v = ((ofMulActionEquivProdAugmentation k G X h) v).2

The equivariant projection is the augmentation component of the splitting.

@[simp]

theorem TauCeti.coe_augmentationProjectionOfIsUnit_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 : MonoidAlgebra k X) : ↑((augmentationProjectionOfIsUnit k G X h) v) = v - ((MonoidAlgebra.basis X k).sumCoords v * Ring.inverse ↑(Fintype.card X)) • permutationSum k X

The projection onto the augmentation subrepresentation subtracts the average coefficient from every coordinate.

@[simp]

theorem TauCeti.augmentationProjectionOfIsUnit_coe (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 : ↥(augmentationSubrepresentation k G X).toSubmodule) : (augmentationProjectionOfIsUnit k G X h) ↑v = v

The projection onto the augmentation subrepresentation is a retraction of its inclusion.

theorem TauCeti.isIntertwiningMap_augmentationProjectionOfIsUnit (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).IsIntertwiningMap (augmentationSubrepresentation k G X).toRepresentation (augmentationProjectionOfIsUnit k G X h)

The projection onto the augmentation subrepresentation is equivariant.

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.

theorem TauCeti.charpoly_augmentationSubrepresentation_mul_X_sub_one {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 g).charpoly * (Polynomial.X - 1) = ((Representation.ofMulAction k G X) g).charpoly

The characteristic polynomial of the augmentation subrepresentation times X - 1 is the characteristic polynomial of g on k[X]. The factor X - 1 is the characteristic polynomial of the trivial one-dimensional quotient of k[X] by the augmentation subrepresentation, so, as for the character, no hypothesis on |X| in k is needed.

@[simp]

theorem MulActionHom.toRepRes_comp_permutationAugmentation {k : Type u} [Ring k] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] {X Y : Type u} [MulAction G X] [MulAction H Y] {φ : G →* H} (f : X →ₑ[⇑φ] Y) : CategoryTheory.CategoryStruct.comp f.toRepRes ((Rep.resFunctor φ).map (TauCeti.permutationAugmentation k H Y)) = TauCeti.permutationAugmentation k G X

Linear extension of an equivariant map preserves the coefficient-sum augmentation.

@[simp]

theorem MulActionHom.toRepRes_comp_permutationAugmentation_assoc {k : Type u} [Ring k] {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] {X Y : Type u} [MulAction G X] [MulAction H Y] {φ : G →* H} (f : X →ₑ[⇑φ] Y) {Z : Rep k G} (h : Rep.of (MonoidHom.comp (Representation.trivial k H k) φ) ⟶ Z) : CategoryTheory.CategoryStruct.comp f.toRepRes (CategoryTheory.CategoryStruct.comp (Rep.resMap φ (TauCeti.permutationAugmentation k H Y)) h) = CategoryTheory.CategoryStruct.comp (TauCeti.permutationAugmentation k G X) h

Linear extension of an equivariant map preserves the coefficient-sum augmentation.