Changing the transversal in the monomial embedding

The monomial embedding of a group into the wreath product of a subgroup depends on a choice of representatives for the left cosets. Two choices give conjugate embeddings. The conjugating element belongs to the base group: at a coset x it is the difference between the two chosen representatives at x.

This relation is the algebraic input for independence of the transversal in tensor induction and in the Evens norm. It uses no topology or finite-index assumption. The coordinate identity is TauCeti.transversalDiff_mul_lWord.

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.monomialChangeTransversal {G : Type u_1} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) : TauCeti.WreathProduct (↥U) (G ⧸ U)

The base-group element comparing the monomial embeddings obtained from two left transversals. Its coordinate at x is r_s(x)⁻¹ r_t(x) in U.

@[simp]

theorem Subgroup.monomialChangeTransversal_left {G : Type u_1} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) (x : G ⧸ U) : (U.monomialChangeTransversal s t).left x = ⟨TauCeti.transversalDiff U (U.leftTransversalRep s) (U.leftTransversalRep t) x, ⋯⟩

The base coordinate of the change-of-transversal element is the difference of the two chosen representatives.

@[simp]

theorem Subgroup.monomialChangeTransversal_right {G : Type u_1} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) : (U.monomialChangeTransversal s t).right = 1

Changing a transversal does not alter the permutation coordinate of the comparing element.

@[simp]

theorem Subgroup.monomialChangeTransversal_self {G : Type u_1} [Group G] (U : Subgroup G) (s : U.LeftTransversal) : U.monomialChangeTransversal s s = 1

Comparing a transversal with itself gives the identity element.

theorem Subgroup.monomialChangeTransversal_mul {G : Type u_1} [Group G] (U : Subgroup G) (s t v : U.LeftTransversal) : U.monomialChangeTransversal s t * U.monomialChangeTransversal t v = U.monomialChangeTransversal s v

Changes of transversal compose in the same order as the chosen representatives.

theorem Subgroup.monomialChangeTransversal_mul_monomialHom {G : Type u_1} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) (g : G) : U.monomialChangeTransversal s t * (U.monomialHom t) g = (U.monomialHom s) g * U.monomialChangeTransversal s t

The two monomial embeddings are intertwined by their base-group comparison element.

theorem Subgroup.monomialHom_changeTransversal {G : Type u_1} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) (g : G) : (U.monomialHom t) g = (U.monomialChangeTransversal s t)⁻¹ * (U.monomialHom s) g * U.monomialChangeTransversal s t

The monomial embeddings for two transversals are conjugate by an element of the base group.

theorem Subgroup.monomialFinHom_changeTransversal {G : Type u_1} [Group G] (U : Subgroup G) (s t : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) (g : G) : (U.monomialFinHom t e) g = ((TauCeti.WreathProduct.congr e) (U.monomialChangeTransversal s t))⁻¹ * (U.monomialFinHom s e) g * (TauCeti.WreathProduct.congr e) (U.monomialChangeTransversal s t)

Relabeling the cosets by Fin U.index carries the same conjugacy to the finite-coordinate monomial embeddings.