Tensor induction of representations

Let a group D act linearly on an R-module M, and let ι be an index type. The permutation wreath product (ι → D) ⋊ Equiv.Perm ι acts on the indexed tensor power ⨂[R] i : ι, M: its base coordinate at i acts on the i-th tensor factor, and its top permutation reindexes the factors. On pure tensors the action is

(a, σ) • (⨂ₜ i, m i) = ⨂ₜ i, a i • m (σ⁻¹ i).

This construction is functorial in the D-representation. Composing it with the monomial homomorphism attached to a transversal of U ≤ G gives tensor induction from U to G. The underlying representations and intertwining maps work over every commutative semiring. The bundled Rep functors use a commutative ring, because the empty indexed tensor product need not be an additive group over a semiring. Characteristic two is needed only later, when tensor induction is applied to the sign-free Evens norm.

An endomorphism of M commuting with D, applied in one tensor factor at a time and summed (the slot sum of TauCeti.PiTensorProduct.slotSum), commutes with the wreath-product action, because the slot sum does not depend on how the factors are indexed. Likewise a grading of M preserved by D gives a total-degree grading of the tensor power preserved by the wreath product. These are the differential and the grading of the tensor induction of a complex.

Main definitions

• Representation.wreathTensor: the wreath-product representation on an indexed tensor power.
• Rep.wreathTensorFunctor: its functorial form on representation categories.
• Subgroup.tensorInducedRepresentation: tensor induction along a chosen transversal.
• Subgroup.tensorInductionFunctor: tensor induction along a subgroup with a chosen transversal.
• Representation.IntertwiningMap.tensorInducedSlotSum: the slot sum of an intertwining endomorphism, as an intertwining endomorphism of tensor induction.

Main results

• Representation.slotSum_comp_wreathTensor: the slot sum of an endomorphism commuting with the action commutes with the wreath-product action.
• Representation.isHomogeneous_wreathTensor: the wreath-product action preserves the total degree of a tensor power of a graded module whose grading the action preserves.

References

• L. Evens, "A generalization of the transfer map in the cohomology of groups", Transactions of the American Mathematical Society 108 (1963), §§2–5.

noncomputable def Representation.wreathTensor {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] (ρ : Representation R D M) (ι : Type x) : Representation R (TauCeti.WreathProduct D ι) (PiTensorProduct R fun (x : ι) => M)

The representation of the permutation wreath product on an indexed tensor power. The base group acts coordinatewise and the top symmetric group permutes the tensor factors.

@[simp]

theorem Representation.wreathTensor_apply_tprod {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] (ρ : Representation R D M) (ι : Type x) (a : TauCeti.WreathProduct D ι) (m : ι → M) : ((ρ.wreathTensor ι) a) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (i : ι) => (ρ (a.left i)) (m ((_root_.Equiv.symm a.right) i))

The wreath-product action on a pure tensor applies the base coordinate after reindexing by the inverse of the top permutation.

theorem Representation.wreathTensor_inl_apply_tprod {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] (ρ : Representation R D M) (ι : Type x) (a : ι → D) (m : ι → M) : ((ρ.wreathTensor ι) (SemidirectProduct.inl a)) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (i : ι) => (ρ (a i)) (m i)

The base subgroup of the wreath product acts independently in each tensor factor.

This derived normal form is an explicit rewrite lemma rather than a simp lemma, since wreathTensor_apply_tprod already simplifies its left-hand side.

theorem Representation.wreathTensor_inr_apply_tprod {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] (ρ : Representation R D M) (ι : Type x) (σ : Equiv.Perm ι) (m : ι → M) : ((ρ.wreathTensor ι) (SemidirectProduct.inr σ)) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (i : ι) => m ((_root_.Equiv.symm σ) i)

The top symmetric subgroup of the wreath product acts by reindexing tensor factors.

This derived normal form is an explicit rewrite lemma rather than a simp lemma, since wreathTensor_apply_tprod already proves it by simplification.

theorem Representation.wreathTensor_apply {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] (ρ : Representation R D M) (ι : Type x) (a : TauCeti.WreathProduct D ι) : (ρ.wreathTensor ι) a = (PiTensorProduct.map fun (i : ι) => ρ (a.left i)) ∘ₗ ↑(PiTensorProduct.reindex R (fun (x : ι) => M) a.right)

The wreath-product action is reindexing by the top permutation followed by the base coordinates in every tensor factor.

theorem Representation.slotSum_comp_wreathTensor {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] {ι : Type x} [Fintype ι] [DecidableEq ι] (ρ : Representation R D M) {f : Module.End R M} (hf : ∀ (g : D), f ∘ₗ ρ g = ρ g ∘ₗ f) (a : TauCeti.WreathProduct D ι) : (TauCeti.PiTensorProduct.slotSum ι fun (x : ι) => f) ∘ₗ (ρ.wreathTensor ι) a = (ρ.wreathTensor ι) a ∘ₗ TauCeti.PiTensorProduct.slotSum ι fun (x : ι) => f

The slot sum of an endomorphism commuting with the action of D commutes with the wreath-product action: it commutes with the base coordinates factor by factor, and the slot sum does not depend on how the tensor factors are indexed.

theorem Representation.isHomogeneous_wreathTensor {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] {ι : Type x} [Fintype ι] {A : Type u_1} [AddCommMonoid A] {ℳ : A → Submodule R M} (ρ : Representation R D M) (hρ : ∀ (g : D), TauCeti.LinearMap.IsHomogeneous (ρ g) ℳ ℳ 0) (a : TauCeti.WreathProduct D ι) : TauCeti.LinearMap.IsHomogeneous ((ρ.wreathTensor ι) a) (TauCeti.PiTensorProduct.totalDegreePiece ι fun (x : ι) => ℳ) (TauCeti.PiTensorProduct.totalDegreePiece ι fun (x : ι) => ℳ) 0

If every element of D acts by a map preserving the degrees of a grading of M, then the wreath-product action preserves the total degree of the tensor power.

noncomputable def Representation.IntertwiningMap.wreathTensor {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] {N : Type y} [AddCommMonoid N] [Module R N] {ρ : Representation R D M} {τ : Representation R D N} (f : ρ.IntertwiningMap τ) (ι : Type x) : (ρ.wreathTensor ι).IntertwiningMap (τ.wreathTensor ι)

Applying an intertwining map in every tensor factor intertwines the corresponding wreath-product representations.

@[simp]

theorem Representation.IntertwiningMap.wreathTensor_apply_tprod {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] {N : Type y} [AddCommMonoid N] [Module R N] {ρ : Representation R D M} {τ : Representation R D N} (f : ρ.IntertwiningMap τ) (ι : Type x) (m : ι → M) : (f.wreathTensor ι) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (i : ι) => f (m i)

The tensor of an intertwining map acts factorwise on pure tensors.

@[simp]

theorem Representation.IntertwiningMap.wreathTensor_toLinearMap {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] {N : Type y} [AddCommMonoid N] [Module R N] {ρ : Representation R D M} {τ : Representation R D N} (f : ρ.IntertwiningMap τ) (ι : Type x) : (f.wreathTensor ι).toLinearMap = PiTensorProduct.map fun (x : ι) => f.toLinearMap

The underlying linear map applies the intertwining map in every tensor factor.

@[simp]

theorem Representation.IntertwiningMap.wreathTensor_id {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] {ρ : Representation R D M} (ι : Type x) : (id ρ).wreathTensor ι = id (ρ.wreathTensor ι)

Tensoring the identity intertwining map gives the identity map.

@[simp]

theorem Representation.IntertwiningMap.wreathTensor_comp {R : Type u} {D : Type v} {M : Type w} [CommSemiring R] [Group D] [AddCommMonoid M] [Module R M] {N : Type y} [AddCommMonoid N] [Module R N] {ρ : Representation R D M} {τ : Representation R D N} {P : Type z} [AddCommMonoid P] [Module R P] {υ : Representation R D P} (g : τ.IntertwiningMap υ) (f : ρ.IntertwiningMap τ) (ι : Type x) : (g.comp f).wreathTensor ι = (g.wreathTensor ι).comp (f.wreathTensor ι)

Tensoring a composite of intertwining maps gives the composite of their tensors.

noncomputable def Rep.wreathTensorMap (R : Type u) (D : Type v) (ι : Type x) [CommRing R] [Group D] {A B : Rep R D} (f : A ⟶ B) : of (A.ρ.wreathTensor ι) ⟶ of (B.ρ.wreathTensor ι)

Apply an intertwining map in every factor of a wreath-product tensor representation.

@[simp]

theorem Rep.wreathTensorMap_hom_apply_tprod (R : Type u) (D : Type v) (ι : Type x) [CommRing R] [Group D] {A B : Rep R D} (f : A ⟶ B) (m : ι → ↑A) : (Hom.hom (wreathTensorMap R D ι f)) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (i : ι) => (Hom.hom f) (m i)

Tensoring a representation morphism applies it in every factor of a pure tensor.

@[simp]

theorem Rep.wreathTensorMap_id (R : Type u) (D : Type v) (ι : Type x) [CommRing R] [Group D] (A : Rep R D) : wreathTensorMap R D ι (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (of (A.ρ.wreathTensor ι))

Tensoring an identity morphism gives the identity morphism.

@[simp]

theorem Rep.wreathTensorMap_comp (R : Type u) (D : Type v) (ι : Type x) [CommRing R] [Group D] {A B C : Rep R D} (f : A ⟶ B) (g : B ⟶ C) : wreathTensorMap R D ι (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (wreathTensorMap R D ι f) (wreathTensorMap R D ι g)

Tensoring representation morphisms preserves composition.

noncomputable def Rep.wreathTensorFunctor (R : Type u) (D : Type v) (ι : Type x) [CommRing R] [Group D] : CategoryTheory.Functor (Rep R D) (Rep R (TauCeti.WreathProduct D ι))

Tensor power with its wreath-product action, functorial in the representation of the base group.

@[simp]

theorem Rep.wreathTensorFunctor_obj (R : Type u) (D : Type v) (ι : Type x) [CommRing R] [Group D] (A : Rep R D) : (wreathTensorFunctor R D ι).obj A = of (A.ρ.wreathTensor ι)

The wreath tensor functor sends a representation to its indexed tensor power with the wreath-product action.

@[simp]

theorem Rep.wreathTensorFunctor_map (R : Type u) (D : Type v) (ι : Type x) [CommRing R] [Group D] {A B : Rep R D} (f : A ⟶ B) : (wreathTensorFunctor R D ι).map f = wreathTensorMap R D ι f

The wreath tensor functor applies a representation morphism in every tensor factor.

noncomputable def Subgroup.tensorInducedRepresentation {R : Type u} {G : Type v} [CommSemiring R] [Group G] (U : Subgroup G) (s : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) : Representation R G (PiTensorProduct R fun (x : G ⧸ U) => M)

The representation obtained by tensor induction from a subgroup with a chosen transversal.

theorem Subgroup.tensorInducedRepresentation_apply {R : Type u} {G : Type v} [CommSemiring R] [Group G] (U : Subgroup G) (s : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) (g : G) (z : PiTensorProduct R fun (x : G ⧸ U) => M) : ((U.tensorInducedRepresentation s ρ) g) z = ((ρ.wreathTensor (G ⧸ U)) ((U.monomialHom s) g)) z

The tensor-induced action is the wreath tensor action pulled back along the monomial homomorphism.

@[simp]

theorem Subgroup.tensorInducedRepresentation_apply_tprod {R : Type u} {G : Type v} [CommSemiring R] [Group G] (U : Subgroup G) (s : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) (g : G) (m : G ⧸ U → M) : ((U.tensorInducedRepresentation s ρ) g) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => (ρ (((U.monomialHom s) g).left x)) (m (g⁻¹ • x))

The action of tensor induction on a pure tensor. The factor at the coset x is acted on by the transversal word at x, while the tensor coordinates are translated by g⁻¹.

theorem Subgroup.map₂_tensorInducedRepresentation {R : Type u} {G : Type v} [CommSemiring R] [Group G] (U : Subgroup G) (s : U.LeftTransversal) {M : Type w} {N : Type x} {P : Type y} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] {ρ : Representation R (↥U) M} {τ : Representation R (↥U) N} {σ : Representation R (↥U) P} (f : M →ₗ[R] N →ₗ[R] P) (hf : ∀ (u : ↥U) (m : M) (n : N), (f ((ρ u) m)) ((τ u) n) = (σ u) ((f m) n)) (g : G) (a : PiTensorProduct R fun (x : G ⧸ U) => M) (b : PiTensorProduct R fun (x : G ⧸ U) => N) : ((PiTensorProduct.map₂ fun (x : G ⧸ U) => f) (((U.tensorInducedRepresentation s ρ) g) a)) (((U.tensorInducedRepresentation s τ) g) b) = ((U.tensorInducedRepresentation s σ) g) (((PiTensorProduct.map₂ fun (x : G ⧸ U) => f) a) b)

Tensor induction preserves equivariant pairings: the factorwise pairing PiTensorProduct.map₂ of a U-equivariant bilinear map is equivariant for the tensor-induced actions of G.

noncomputable def Subgroup.tensorInductionFunctor {R : Type u} {G : Type v} [CommRing R] [Group G] (U : Subgroup G) (s : U.LeftTransversal) : CategoryTheory.Functor (Rep R ↥U) (Rep R G)

Tensor induction from a subgroup: tensor the representation over the left cosets and restrict the resulting wreath-product representation along the monomial homomorphism associated to a chosen transversal.

@[simp]

theorem Subgroup.tensorInductionFunctor_obj {R : Type u} {G : Type v} [CommRing R] [Group G] (U : Subgroup G) (s : U.LeftTransversal) (A : Rep R ↥U) : (U.tensorInductionFunctor s).obj A = Rep.of (U.tensorInducedRepresentation s A.ρ)

On objects, tensor induction is the tensor-power representation restricted along the monomial homomorphism determined by the transversal.

@[simp]

theorem Subgroup.tensorInductionFunctor_map_hom_apply_tprod {R : Type u} {G : Type v} [CommRing R] [Group G] (U : Subgroup G) (s : U.LeftTransversal) {A B : Rep R ↥U} (f : A ⟶ B) (m : G ⧸ U → ↑A) : (Rep.Hom.hom ((U.tensorInductionFunctor s).map f)) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => (Rep.Hom.hom f) (m x)

On morphisms, tensor induction applies the representation morphism in every factor of a pure tensor.

noncomputable def Representation.IntertwiningMap.tensorInduced {R : Type u} {G : Type v} [CommSemiring R] [Group G] {U : Subgroup G} {M : Type w} {N : Type y} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R (↥U) M} {τ : Representation R (↥U) N} (f : ρ.IntertwiningMap τ) (s : U.LeftTransversal) : (U.tensorInducedRepresentation s ρ).IntertwiningMap (U.tensorInducedRepresentation s τ)

Tensoring an intertwining map in every factor intertwines tensor induction along the same transversal.

@[simp]

theorem Representation.IntertwiningMap.tensorInduced_toLinearMap {R : Type u} {G : Type v} [CommSemiring R] [Group G] {U : Subgroup G} {M : Type w} {N : Type y} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R (↥U) M} {τ : Representation R (↥U) N} (f : ρ.IntertwiningMap τ) (s : U.LeftTransversal) : (f.tensorInduced s).toLinearMap = PiTensorProduct.map fun (x : G ⧸ U) => f.toLinearMap

The underlying linear map of tensor induction applies the intertwining map in each factor.

@[simp]

theorem Representation.IntertwiningMap.tensorInduced_apply_tprod {R : Type u} {G : Type v} [CommSemiring R] [Group G] {U : Subgroup G} {M : Type w} {N : Type y} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R (↥U) M} {τ : Representation R (↥U) N} (f : ρ.IntertwiningMap τ) (s : U.LeftTransversal) (m : G ⧸ U → M) : (f.tensorInduced s) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (i : G ⧸ U) => f (m i)

The tensor-induced intertwining map acts factorwise on pure tensors.

@[simp]

theorem Representation.IntertwiningMap.tensorInduced_id {R : Type u} {G : Type v} [CommSemiring R] [Group G] {U : Subgroup G} {M : Type w} [AddCommMonoid M] [Module R M] {ρ : Representation R (↥U) M} (s : U.LeftTransversal) : (id ρ).tensorInduced s = id (U.tensorInducedRepresentation s ρ)

Tensor induction of the identity intertwining map is the identity map.

@[simp]

theorem Representation.IntertwiningMap.tensorInduced_comp {R : Type u} {G : Type v} [CommSemiring R] [Group G] {U : Subgroup G} {M : Type w} {N : Type y} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R (↥U) M} {τ : Representation R (↥U) N} {P : Type z} [AddCommMonoid P] [Module R P] {υ : Representation R (↥U) P} (g : τ.IntertwiningMap υ) (f : ρ.IntertwiningMap τ) (s : U.LeftTransversal) : (g.comp f).tensorInduced s = (g.tensorInduced s).comp (f.tensorInduced s)

Tensor induction of a composite intertwining map is the composite of the induced maps.

noncomputable def Representation.IntertwiningMap.tensorInducedSlotSum {R : Type u} {G : Type v} [CommSemiring R] [Group G] {U : Subgroup G} {M : Type w} [AddCommMonoid M] [Module R M] {ρ : Representation R (↥U) M} [Fintype (G ⧸ U)] [DecidableEq (G ⧸ U)] (f : ρ.IntertwiningMap ρ) (s : U.LeftTransversal) : (U.tensorInducedRepresentation s ρ).IntertwiningMap (U.tensorInducedRepresentation s ρ)

The slot sum of an intertwining endomorphism, which applies it in one coset factor at a time, is an intertwining endomorphism of tensor induction. In characteristic two it is the differential of the tensor induction of a complex.

@[simp]

theorem Representation.IntertwiningMap.tensorInducedSlotSum_toLinearMap {R : Type u} {G : Type v} [CommSemiring R] [Group G] {U : Subgroup G} {M : Type w} [AddCommMonoid M] [Module R M] {ρ : Representation R (↥U) M} [Fintype (G ⧸ U)] [DecidableEq (G ⧸ U)] (f : ρ.IntertwiningMap ρ) (s : U.LeftTransversal) : (f.tensorInducedSlotSum s).toLinearMap = TauCeti.PiTensorProduct.slotSum (G ⧸ U) fun (x : G ⧸ U) => f.toLinearMap

The underlying linear map of the tensor-induced slot sum is the slot sum.