Naturality of tensor induction in the group

Tensor induction commutes with a homomorphism that identifies the relevant coset spaces. If φ : G →* G' carries U ≤ G to U' ≤ G', restricts to ψ : U →* U', and induces an equivalence G ⧸ U ≃ G' ⧸ U', then reindexing the tensor factors along that equivalence identifies tensor induction of a pulled-back representation with the pullback of tensor induction.

The main specialization is inflation. For a normal subgroup N ≤ U, tensor induction from U to G after pulling coefficients back from the image of U in G ⧸ N agrees with tensor induction in the quotient, pulled back to G. This is the representation-level comparison needed to prove that the Evens norm commutes with inflation.

Main definitions

• Subgroup.tensorInducedMapEquiv: naturality under a homomorphism inducing an equivalence of coset spaces.
• Subgroup.tensorInducedQuotientEquiv: the specialization to a quotient by a normal subgroup.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Transactions of the American Mathematical Society 108 (1963), Sections 2--3 and 6.

noncomputable def Subgroup.tensorInducedMapEquiv {R : Type u} [CommSemiring R] {G : Type v} [Group G] {G' : Type v'} [Group G'] {U : Subgroup G} {U' : Subgroup G'} {M : Type w} [AddCommMonoid M] [Module R M] (φ : G →* G') (ψ : ↥U →* ↥U') (hψ : ∀ (u : ↥U), ↑(ψ u) = φ ↑u) (e : G ⧸ U ≃ G' ⧸ U') (he : ∀ (g : G), e ↑g = ↑(φ g)) (s : U.LeftTransversal) (ρ : Representation R (↥U') M) : (U.tensorInducedRepresentation s (MonoidHom.comp ρ ψ)).Equiv (MonoidHom.comp (U'.tensorInducedRepresentation (s.map φ e he) ρ) φ)

Reindexing tensor factors identifies tensor induction before and after a homomorphism that identifies the coset spaces.

@[simp]

theorem Subgroup.tensorInducedMapEquiv_apply_tprod {R : Type u} [CommSemiring R] {G : Type v} [Group G] {G' : Type v'} [Group G'] {U : Subgroup G} {U' : Subgroup G'} {M : Type w} [AddCommMonoid M] [Module R M] (φ : G →* G') (ψ : ↥U →* ↥U') (hψ : ∀ (u : ↥U), ↑(ψ u) = φ ↑u) (e : G ⧸ U ≃ G' ⧸ U') (he : ∀ (g : G), e ↑g = ↑(φ g)) (s : U.LeftTransversal) (ρ : Representation R (↥U') M) (m : G ⧸ U → M) : (tensorInducedMapEquiv φ ψ hψ e he s ρ) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (y : G' ⧸ U') => m (e.symm y)

The map comparison sends a pure tensor to the same tensor with its factors relabeled by the induced equivalence of coset spaces.

@[simp]

theorem Subgroup.tensorInducedMapEquiv_symm_apply_tprod {R : Type u} [CommSemiring R] {G : Type v} [Group G] {G' : Type v'} [Group G'] {U : Subgroup G} {U' : Subgroup G'} {M : Type w} [AddCommMonoid M] [Module R M] (φ : G →* G') (ψ : ↥U →* ↥U') (hψ : ∀ (u : ↥U), ↑(ψ u) = φ ↑u) (e : G ⧸ U ≃ G' ⧸ U') (he : ∀ (g : G), e ↑g = ↑(φ g)) (s : U.LeftTransversal) (ρ : Representation R (↥U') M) (m : G' ⧸ U' → M) : (tensorInducedMapEquiv φ ψ hψ e he s ρ).symm ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => m (e x)

The inverse map comparison relabels tensor factors along the inverse equivalence of coset spaces.

theorem Subgroup.tensorInducedMapEquiv_naturality {R : Type u} [CommSemiring R] {G : Type v} [Group G] {G' : Type v'} [Group G'] {U : Subgroup G} {U' : Subgroup G'} {M : Type w} [AddCommMonoid M] [Module R M] (φ : G →* G') (ψ : ↥U →* ↥U') (hψ : ∀ (u : ↥U), ↑(ψ u) = φ ↑u) (e : G ⧸ U ≃ G' ⧸ U') (he : ∀ (g : G), e ↑g = ↑(φ g)) (s : U.LeftTransversal) {N : Type u_1} [AddCommMonoid N] [Module R N] {ρ : Representation R (↥U') M} {τ : Representation R (↥U') N} (f : ρ.IntertwiningMap τ) : (PiTensorProduct.map fun (x : G' ⧸ U') => f.toLinearMap) ∘ₗ ↑(tensorInducedMapEquiv φ ψ hψ e he s ρ).toLinearEquiv = ↑(tensorInducedMapEquiv φ ψ hψ e he s τ).toLinearEquiv ∘ₗ PiTensorProduct.map fun (x : G ⧸ U) => f.toLinearMap

The tensor-induction comparison is natural in the coefficient representation.

noncomputable def Subgroup.tensorInducedQuotientEquiv {R : Type u} [CommSemiring R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommMonoid M] [Module R M] (N : Subgroup G) [N.Normal] (hNU : N ≤ U) (s : U.LeftTransversal) (ρ : Representation R (↥(map (QuotientGroup.mk' N) U)) M) : (U.tensorInducedRepresentation s (MonoidHom.comp ρ ((QuotientGroup.mk' N).subgroupMap U))).Equiv (MonoidHom.comp ((map (QuotientGroup.mk' N) U).tensorInducedRepresentation (s.map (QuotientGroup.mk' N) (QuotientGroup.quotientEquivQuotientMapOfLE hNU) ⋯) ρ) (QuotientGroup.mk' N))

Tensor induction commutes with inflation through a quotient by a normal subgroup contained in the subgroup of induction.

@[simp]

theorem Subgroup.tensorInducedQuotientEquiv_apply_tprod {R : Type u} [CommSemiring R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommMonoid M] [Module R M] (N : Subgroup G) [N.Normal] (hNU : N ≤ U) (s : U.LeftTransversal) (ρ : Representation R (↥(map (QuotientGroup.mk' N) U)) M) (m : G ⧸ U → M) : (tensorInducedQuotientEquiv N hNU s ρ) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (y : (G ⧸ N) ⧸ map (QuotientGroup.mk' N) U) => m ((QuotientGroup.quotientEquivQuotientMapOfLE hNU).symm y)

On pure tensors, the quotient comparison relabels a coset of U by its image in the quotient.

@[simp]

theorem Subgroup.tensorInducedQuotientEquiv_symm_apply_tprod {R : Type u} [CommSemiring R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommMonoid M] [Module R M] (N : Subgroup G) [N.Normal] (hNU : N ≤ U) (s : U.LeftTransversal) (ρ : Representation R (↥(map (QuotientGroup.mk' N) U)) M) (m : (G ⧸ N) ⧸ map (QuotientGroup.mk' N) U → M) : (tensorInducedQuotientEquiv N hNU s ρ).symm ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => m ((QuotientGroup.quotientEquivQuotientMapOfLE hNU) x)

The inverse quotient comparison replaces a quotient coset by its preimage coset in G.

theorem Subgroup.tensorInducedQuotientEquiv_naturality {R : Type u} [CommSemiring R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommMonoid M] [Module R M] (N : Subgroup G) [N.Normal] (hNU : N ≤ U) (s : U.LeftTransversal) {P : Type u_1} [AddCommMonoid P] [Module R P] {ρ : Representation R (↥(map (QuotientGroup.mk' N) U)) M} {τ : Representation R (↥(map (QuotientGroup.mk' N) U)) P} (f : ρ.IntertwiningMap τ) : (PiTensorProduct.map fun (x : (G ⧸ N) ⧸ map (QuotientGroup.mk' N) U) => f.toLinearMap) ∘ₗ ↑(tensorInducedQuotientEquiv N hNU s ρ).toLinearEquiv = ↑(tensorInducedQuotientEquiv N hNU s τ).toLinearEquiv ∘ₗ PiTensorProduct.map fun (x : G ⧸ U) => f.toLinearMap

The quotient comparison commutes with equivariant maps of coefficient representations.