Naturality of the monomial homomorphism

Let φ : G →* G' be a group homomorphism, U ≤ G and U' ≤ G' subgroups, and e : G ⧸ U ≃ G' ⧸ U' a bijection of coset spaces induced by φ, so that e ⟦g⟧ = ⟦φ g⟧. Such an e exists exactly when U = U'.comap φ and every coset of U' meets the range of φ; then φ restricts to a homomorphism ψ : U →* U'. The image φ '' s of a left transversal s of U is a left transversal s' of U' (Subgroup.LeftTransversal.map, in TauCeti/GroupTheory/TransversalWord.lean), whose representative of e x is the image of the representative of x. The monomial homomorphisms of s and s' are related by

Φ_{s'} (φ g) = congr e (map ψ (Φ_s g)),

that is, φ applied to the transversal words in every coordinate, followed by relabeling the coordinates along e (Subgroup.monomialHom_map).

The case that motivates this file is inflation: for a normal subgroup N contained in U, the quotient map G → G ⧸ N induces the bijection G ⧸ U ≃ (G ⧸ N) ⧸ U.map (mk' N) of QuotientGroup.quotientEquivQuotientMapOfLE, so the monomial homomorphism of the image of U in G ⧸ N, evaluated on the class of g, is the image of the monomial homomorphism of U at g (Subgroup.monomialHom_quotient). This is the group-level identity behind the compatibility of Evens' multiplicative transfer with inflation.

Main results

• Subgroup.monomialHom_map: naturality of the monomial homomorphism along φ.
• Subgroup.monomialHom_quotient: the inflation case.

References

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

theorem Subgroup.monomialHom_map {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {U : Subgroup G} {U' : Subgroup G'} (φ : G →* G') (ψ : ↥U →* ↥U') (hψ : ∀ (u : ↥U), ↑(ψ u) = φ ↑u) (e : G ⧸ U ≃ G' ⧸ U') (he : ∀ (g : G), e ↑g = ↑(φ g)) (s : U.LeftTransversal) (g : G) : (U'.monomialHom (s.map φ e he)) (φ g) = (TauCeti.WreathProduct.congr e) ((TauCeti.WreathProduct.map ψ) ((U.monomialHom s) g))

Naturality of the monomial homomorphism. Let φ : G →* G' induce the bijection e of coset spaces and restrict to ψ : U →* U'. The monomial homomorphism of the image transversal s.map φ e he at φ g is the monomial homomorphism of s at g with ψ applied to its coordinates and the coordinates relabeled along e.

theorem Subgroup.monomialHom_quotient {G : Type u_1} [Group G] {U : Subgroup G} (N : Subgroup G) [N.Normal] (hNU : N ≤ U) (s : U.LeftTransversal) (g : G) : ((map (QuotientGroup.mk' N) U).monomialHom (s.map (QuotientGroup.mk' N) (QuotientGroup.quotientEquivQuotientMapOfLE hNU) ⋯)) ↑g = (TauCeti.WreathProduct.congr (QuotientGroup.quotientEquivQuotientMapOfLE hNU)) ((TauCeti.WreathProduct.map ((QuotientGroup.mk' N).subgroupMap U)) ((U.monomialHom s) g))

The monomial homomorphism and inflation. For a normal subgroup N contained in U, the monomial homomorphism of the image of U in G ⧸ N, for the image of a transversal s of U and evaluated on the class of g, is the monomial homomorphism of s at g reduced modulo N in every coordinate, with the cosets of U relabeled as those of its image by QuotientGroup.quotientEquivQuotientMapOfLE.