The monomial homomorphism of a subgroup transversal

A transversal for U ≤ G embeds G in the permutation wreath product with base group U and coordinates indexed by G ⧸ U. Its permutation part is left translation on cosets; its coordinate at x is the transversal word r(x)⁻¹ g r(g⁻¹ • x), where r = U.leftTransversalRep s for s : U.LeftTransversal. Mathlib's bundled transversal supplies the representatives and their section property; the monomial maps consume that same choice. The cocycle law gives the homomorphism, and both the coset-indexed and finite-coordinate forms are injective. The public maps live in the Subgroup namespace and are called as U.monomialHom s and U.monomialFinHom s e, where e labels the cosets by Fin U.index. Continuity for an open subgroup is proved in TauCeti.Topology.Algebra.Group.WreathProduct.Monomial.

This is the monomial construction used in Evens' multiplicative transfer; see L. Evens, "A generalization of the transfer map in the cohomology of groups", Trans. AMS 108 (1963), §§2–3.

noncomputable def Subgroup.monomialHom {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) : G →* TauCeti.WreathProduct (↥U) (G ⧸ U)

The monomial homomorphism associated to a bundled transversal s of U. Its permutation part is left translation on G ⧸ U; the coordinate at x is the element r(x)⁻¹ g r(g⁻¹ • x) of U, where r = U.leftTransversalRep s.

Equations

• U.monomialHom s = { toFun := fun (g : G) => ⟨fun (x : G ⧸ U) => ⟨TauCeti.lWord U (U.leftTransversalRep s) x g, ⋯⟩, (MulAction.toPermHom G (G ⧸ U)) g⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Subgroup.monomialHom_left {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (g : G) (x : G ⧸ U) : ((U.monomialHom s) g).left x = ⟨TauCeti.lWord U (U.leftTransversalRep s) x g, ⋯⟩

The coordinate of the monomial homomorphism is the transversal word as an element of U.

@[simp]

theorem Subgroup.monomialHom_right {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (g : G) (x : G ⧸ U) : ((U.monomialHom s) g).right x = g • x

The permutation part of the monomial homomorphism translates left cosets.

@[simp]

theorem Subgroup.monomialHom_right_inv {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (g : G) (x : G ⧸ U) : ((U.monomialHom s) g).right⁻¹ x = g⁻¹ • x

The inverse permutation coordinate translates a coset by the inverse group element.

theorem Subgroup.monomialHom_injective {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) : Function.Injective ⇑(U.monomialHom s)

The monomial homomorphism associated to a subgroup transversal is injective.

noncomputable def Subgroup.monomialFinHom {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) : G →* TauCeti.WreathProduct (↥U) (Fin U.index)

Relabel the cosets by Fin (G : U) using a chosen bijection e. The coordinate at i is the transversal word at e.symm i. For a finite-index subgroup, one possible e is Finite.equivFinOfCardEq U.index_eq_card.symm.

Equations

• U.monomialFinHom s e = (TauCeti.WreathProduct.congr e).toMonoidHom.comp (U.monomialHom s)

theorem Subgroup.monomialFinHom_apply {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) (g : G) : (U.monomialFinHom s e) g = (TauCeti.WreathProduct.congr e) ((U.monomialHom s) g)

The finite-coordinate homomorphism is the relabeling of the coset-indexed map.

@[simp]

theorem Subgroup.monomialFinHom_left {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) (g : G) (i : Fin U.index) : ((U.monomialFinHom s e) g).left i = ⟨TauCeti.lWord U (U.leftTransversalRep s) (e.symm i) g, ⋯⟩

A finite coordinate is the transversal word at the corresponding coset, as an element of U.

@[simp]

theorem Subgroup.monomialFinHom_right {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) (g : G) (i : Fin U.index) : ((U.monomialFinHom s e) g).right i = e (g • e.symm i)

The finite permutation coordinate translates the corresponding coset.

@[simp]

theorem Subgroup.monomialFinHom_right_inv {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) (g : G) (i : Fin U.index) : ((U.monomialFinHom s e) g).right⁻¹ i = e (g⁻¹ • e.symm i)

The inverse finite permutation coordinate translates the named coset by the inverse group element.

theorem Subgroup.monomialFinHom_injective {G : Type u} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) : Function.Injective ⇑(U.monomialFinHom s e)

The finite-coordinate monomial homomorphism is injective.