Diagonal invariant tensors in tensor induction

An invariant vector of a subgroup representation gives an invariant vector of its tensor induction: put the same vector in every coset factor. The monomial action fixes this tensor because its subgroup coordinates fix the vector and its permutation only reorders identical factors. The resulting function is natural in intertwining maps and agrees under the existing change-of-transversal and change-of-group comparisons. For finitely many cosets it is homogeneous of degree the number of cosets, and for one coset it recovers the original vector.

Applied to an invariant element of a coinduced resolution term, this is the diagonal tensor used on representatives in the multiplicative transfer. This file concerns invariant vectors; preservation of differentials and descent to cohomology are separate assertions.

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.tensorInducedDiagonal {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] (ρ : Representation R (↥U) M) (s : U.LeftTransversal) : ↥ρ.invariants → ↥(U.tensorInducedRepresentation s ρ).invariants

Put an invariant vector in every coset factor of tensor induction. This is a function between invariant submodules; it need not be additive.

@[simp]

theorem Representation.coe_tensorInducedDiagonal {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] (ρ : Representation R (↥U) M) (s : U.LeftTransversal) (x : ↥ρ.invariants) : ↑(ρ.tensorInducedDiagonal s x) = (PiTensorProduct.tprod R) fun (x_1 : G ⧸ U) => ↑x

The underlying tensor of the invariant diagonal has the same vector in every factor.

@[simp]

theorem Representation.tensorInducedDiagonal_zero {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] (ρ : Representation R (↥U) M) (s : U.LeftTransversal) : ρ.tensorInducedDiagonal s 0 = 0

The invariant diagonal sends zero to zero. A coset family is always nonempty.

@[simp]

theorem Representation.tensorInducedDiagonal_smul {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] (ρ : Representation R (↥U) M) (s : U.LeftTransversal) [Fintype (G ⧸ U)] (r : R) (x : ↥ρ.invariants) : ρ.tensorInducedDiagonal s (r • x) = r ^ Fintype.card (G ⧸ U) • ρ.tensorInducedDiagonal s x

Scaling an invariant vector scales its diagonal tensor by the scalar raised to the number of cosets. The caller's finite enumeration of the cosets is retained.

theorem Representation.tensorInducedChangeTransversal_tensorInducedDiagonal {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] (ρ : Representation R (↥U) M) (s t : U.LeftTransversal) (x : ↥ρ.invariants) : (U.tensorInducedChangeTransversal s t ρ) ↑(ρ.tensorInducedDiagonal t x) = ↑(ρ.tensorInducedDiagonal s x)

The change-of-transversal comparison fixes the invariant diagonal tensor.

theorem Representation.tensorInducedMapEquiv_tensorInducedDiagonal {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] {G' : Type y} [Group G'] {U' : Subgroup G'} (ρ : Representation R (↥U') M) (φ : G →* G') (ψ : ↥U →* ↥U') (hψ : ∀ (u : ↥U), ↑(ψ u) = φ ↑u) (e : G ⧸ U ≃ G' ⧸ U') (he : ∀ (g : G), e ↑g = ↑(φ g)) (s : U.LeftTransversal) (x : ↥ρ.invariants) : (Subgroup.tensorInducedMapEquiv φ ψ hψ e he s ρ) ↑(tensorInducedDiagonal (MonoidHom.comp ρ ψ) s ⟨↑x, ⋯⟩) = ↑(ρ.tensorInducedDiagonal (s.map φ e he) x)

The change-of-group comparison for tensor induction carries the diagonal of a restricted invariant vector to the diagonal of the original vector. This is the representative-level naturality used by the inflation law for the multiplicative transfer.

theorem Representation.tensorInducedMapEquiv_symm_tensorInducedDiagonal {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] {G' : Type y} [Group G'] {U' : Subgroup G'} (ρ : Representation R (↥U') M) (φ : G →* G') (ψ : ↥U →* ↥U') (hψ : ∀ (u : ↥U), ↑(ψ u) = φ ↑u) (e : G ⧸ U ≃ G' ⧸ U') (he : ∀ (g : G), e ↑g = ↑(φ g)) (s : U.LeftTransversal) (x : ↥ρ.invariants) : (Subgroup.tensorInducedMapEquiv φ ψ hψ e he s ρ).symm ↑(ρ.tensorInducedDiagonal (s.map φ e he) x) = ↑(tensorInducedDiagonal (MonoidHom.comp ρ ψ) s ⟨↑x, ⋯⟩)

The inverse change-of-group comparison carries the target diagonal back to the diagonal of the restricted invariant vector.

theorem Representation.tensorInducedQuotientEquiv_tensorInducedDiagonal {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] {N : Subgroup G} [N.Normal] (ρ : Representation R (↥(Subgroup.map (QuotientGroup.mk' N) U)) M) (hNU : N ≤ U) (s : U.LeftTransversal) (x : ↥ρ.invariants) : (Subgroup.tensorInducedQuotientEquiv N hNU s ρ) ↑(tensorInducedDiagonal (MonoidHom.comp ρ ((QuotientGroup.mk' N).subgroupMap U)) s ⟨↑x, ⋯⟩) = ↑(ρ.tensorInducedDiagonal (s.map (QuotientGroup.mk' N) (QuotientGroup.quotientEquivQuotientMapOfLE hNU) ⋯) x)

For a quotient by a normal subgroup contained in U, the tensor-induction comparison carries the diagonal of an inflated invariant vector to the diagonal in the quotient.

theorem Representation.tensorInducedQuotientEquiv_symm_tensorInducedDiagonal {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] {N : Subgroup G} [N.Normal] (ρ : Representation R (↥(Subgroup.map (QuotientGroup.mk' N) U)) M) (hNU : N ≤ U) (s : U.LeftTransversal) (x : ↥ρ.invariants) : (Subgroup.tensorInducedQuotientEquiv N hNU s ρ).symm ↑(ρ.tensorInducedDiagonal (s.map (QuotientGroup.mk' N) (QuotientGroup.quotientEquivQuotientMapOfLE hNU) ⋯) x) = ↑(tensorInducedDiagonal (MonoidHom.comp ρ ((QuotientGroup.mk' N).subgroupMap U)) s ⟨↑x, ⋯⟩)

The inverse quotient comparison carries the quotient diagonal back to the diagonal of the inflated invariant vector.

theorem Representation.IntertwiningMap.tensorInduced_tensorInducedDiagonal {R : Type u} [CommRing R] {G : Type v} [Group G] {U : Subgroup G} {M : Type w} [AddCommGroup M] [Module R M] {N : Type y} [AddCommGroup N] [Module R N] {ρ : Representation R (↥U) M} {τ : Representation R (↥U) N} (f : ρ.IntertwiningMap τ) (s : U.LeftTransversal) (x : ↥ρ.invariants) : (f.tensorInduced s) ↑(ρ.tensorInducedDiagonal s x) = ↑(τ.tensorInducedDiagonal s ⟨f ↑x, ⋯⟩)

Tensor induction of an intertwining map carries the invariant diagonal to the diagonal of its image. The image is read in the target's invariant submodule.

For the trivial subgroup of C₂, the diagonal has two tensor factors. On the trivial module 𝔽₂², the vectors (1, 0) and (0, 1) witness its failure of additivity. The tensor functional multiplying the first coordinate of one factor by the second of the other reads their separate diagonals as zero and the diagonal of their sum as one.