Tensor induction is independent of the transversal

The tensor-induced representations attached to two left transversals of a subgroup are isomorphic. The isomorphism acts on the tensor power by the base-group element comparing their monomial embeddings. On a pure tensor, it applies the difference of the two chosen representatives at each coset to the corresponding factor. These comparisons are the identity for an unchanged transversal, compose through an intermediate transversal, and are natural in the representation being tensor-induced. When the action preserves a grading of the module, they preserve and detect the total degree of the tensor power.

The construction is algebraic and needs neither finite index nor topology. Its factorwise formula supplies the comparison of continuous tensor-induced actions for open subgroups.

References

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

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

The tensor-power linear equivalence induced by changing the transversal. It acts by the comparison element in the base group of the wreath product.

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

The change-of-transversal linear equivalence acts by the wreath tensor representation of the comparison element.

@[simp]

theorem Subgroup.tensorInducedChangeTransversalLinearEquiv_apply_tprod {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) (m : G ⧸ U → M) : (U.tensorInducedChangeTransversalLinearEquiv s t ρ) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => (ρ ((U.monomialChangeTransversal s t).left x)) (m x)

On a pure tensor, the comparison applies the transversal difference in each coordinate.

@[simp]

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

Comparing a transversal with itself gives the identity linear equivalence.

theorem Subgroup.tensorInducedChangeTransversalLinearEquiv_trans {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) (v : U.LeftTransversal) : U.tensorInducedChangeTransversalLinearEquiv t v ρ ≪≫ₗ U.tensorInducedChangeTransversalLinearEquiv s t ρ = U.tensorInducedChangeTransversalLinearEquiv s v ρ

Change-of-transversal linear equivalences compose according to the intermediate transversal.

@[simp]

theorem Subgroup.tensorInducedChangeTransversalLinearEquiv_symm {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) : (U.tensorInducedChangeTransversalLinearEquiv s t ρ).symm = U.tensorInducedChangeTransversalLinearEquiv t s ρ

Reversing the two transversals gives the inverse linear equivalence.

theorem Subgroup.tensorInducedChangeTransversalLinearEquiv_mem_totalDegreePiece_iff {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) [Fintype (G ⧸ U)] {A : Type u_1} [AddCommMonoid A] {ℳ : A → Submodule R M} (hρ : ∀ (u : ↥U), TauCeti.LinearMap.IsHomogeneous (ρ u) ℳ ℳ 0) (n : A) (z : PiTensorProduct R fun (x : G ⧸ U) => M) : (U.tensorInducedChangeTransversalLinearEquiv s t ρ) z ∈ TauCeti.PiTensorProduct.totalDegreePiece (G ⧸ U) (fun (x : G ⧸ U) => ℳ) n ↔ z ∈ TauCeti.PiTensorProduct.totalDegreePiece (G ⧸ U) (fun (x : G ⧸ U) => ℳ) n

If the action of U preserves the degrees of a grading of M, then changing the transversal preserves and detects the total degree of the tensor power.

noncomputable def Subgroup.tensorInducedChangeTransversal {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) : (U.tensorInducedRepresentation t ρ).Equiv (U.tensorInducedRepresentation s ρ)

Changing the transversal yields an equivalence of tensor-induced representations.

theorem Subgroup.tensorInducedChangeTransversal_toLinearEquiv {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) : (U.tensorInducedChangeTransversal s t ρ).toLinearEquiv = U.tensorInducedChangeTransversalLinearEquiv s t ρ

The underlying linear equivalence of the representation comparison is the named change-of-transversal linear equivalence.

theorem Subgroup.tensorInducedChangeTransversal_apply {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) (z : PiTensorProduct R fun (x : G ⧸ U) => M) : (U.tensorInducedChangeTransversal s t ρ) z = (U.tensorInducedChangeTransversalLinearEquiv s t ρ) z

The representation equivalence has the named factorwise linear equivalence as its underlying map.

@[simp]

theorem Subgroup.tensorInducedChangeTransversal_apply_tprod {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) (m : G ⧸ U → M) : (U.tensorInducedChangeTransversal s t ρ) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => (ρ ((U.monomialChangeTransversal s t).left x)) (m x)

On a pure tensor, changing the transversal applies the difference of representatives to each factor at its coset.

@[simp]

theorem Subgroup.tensorInducedChangeTransversal_self {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) : U.tensorInducedChangeTransversal s s ρ = Representation.Equiv.refl (U.tensorInducedRepresentation s ρ)

The representation equivalence associated to an unchanged transversal is the identity.

theorem Subgroup.tensorInducedChangeTransversal_trans {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) (v : U.LeftTransversal) : (U.tensorInducedChangeTransversal t v ρ).trans (U.tensorInducedChangeTransversal s t ρ) = U.tensorInducedChangeTransversal s v ρ

Change-of-transversal representation equivalences compose through an intermediate transversal.

@[simp]

theorem Subgroup.tensorInducedChangeTransversal_symm {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) : (U.tensorInducedChangeTransversal s t ρ).symm = U.tensorInducedChangeTransversal t s ρ

Swapping the transversals gives the inverse representation equivalence.

theorem Subgroup.tensorInducedChangeTransversal_naturality {R : Type u} [CommSemiring R] {G : Type v} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) {M : Type w} [AddCommMonoid M] [Module R M] (ρ : Representation R (↥U) M) {N : Type u_1} [AddCommMonoid N] [Module R N] {τ : Representation R (↥U) N} (f : ρ.IntertwiningMap τ) : (f.tensorInduced s).comp ↑(U.tensorInducedChangeTransversal s t ρ) = (↑(U.tensorInducedChangeTransversal s t τ)).comp (f.tensorInduced t)

Change of transversal commutes with tensor induction of an intertwining map.