Continuity of the monomial homomorphism

For an open subgroup the transversal-dependent monomial homomorphism is continuous in the coordinate topology of the permutation wreath product when multiplication on the source is separately continuous. The finite-coordinate form is continuous after a chosen relabeling of the cosets by Fin U.index. The public continuous maps are Subgroup.monomialContinuousHom and Subgroup.monomialFinContinuousHom, used as U.monomialContinuousHom hU s.

theorem Subgroup.continuous_monomialHom {G : Type u} [Group G] (U : Subgroup G) [TopologicalSpace G] [SeparatelyContinuousMul G] (hU : IsOpen ↑U) (s : U.LeftTransversal) : Continuous ⇑(U.monomialHom s)

The monomial homomorphism is continuous when U is open and multiplication on G is separately continuous.

noncomputable def Subgroup.monomialContinuousHom {G : Type u} [Group G] (U : Subgroup G) [TopologicalSpace G] [SeparatelyContinuousMul G] (hU : IsOpen ↑U) (s : U.LeftTransversal) : G →ₜ* TauCeti.WreathProduct (↥U) (G ⧸ U)

The continuous monomial homomorphism for an open subgroup and a chosen transversal.

Equations

• U.monomialContinuousHom hU s = { toMonoidHom := U.monomialHom s, continuous_toFun := ⋯ }

@[simp]

theorem Subgroup.monomialContinuousHom_apply {G : Type u} [Group G] (U : Subgroup G) [TopologicalSpace G] [SeparatelyContinuousMul G] (hU : IsOpen ↑U) (s : U.LeftTransversal) (g : G) : (U.monomialContinuousHom hU s) g = (U.monomialHom s) g

The continuous monomial homomorphism has the same underlying homomorphism.

theorem Subgroup.continuous_monomialFinHom {G : Type u} [Group G] (U : Subgroup G) [TopologicalSpace G] [SeparatelyContinuousMul G] (hU : IsOpen ↑U) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) : Continuous ⇑(U.monomialFinHom s e)

The finite-coordinate monomial homomorphism is continuous for an open subgroup.

noncomputable def Subgroup.monomialFinContinuousHom {G : Type u} [Group G] (U : Subgroup G) [TopologicalSpace G] [SeparatelyContinuousMul G] (hU : IsOpen ↑U) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) : G →ₜ* TauCeti.WreathProduct (↥U) (Fin U.index)

The finite-coordinate continuous monomial homomorphism for an open subgroup.

Equations

• U.monomialFinContinuousHom hU s e = { toMonoidHom := U.monomialFinHom s e, continuous_toFun := ⋯ }

@[simp]

theorem Subgroup.monomialFinContinuousHom_apply {G : Type u} [Group G] (U : Subgroup G) [TopologicalSpace G] [SeparatelyContinuousMul G] (hU : IsOpen ↑U) (s : U.LeftTransversal) (e : G ⧸ U ≃ Fin U.index) (g : G) : (U.monomialFinContinuousHom hU s e) g = (U.monomialFinHom s e) g

The finite-coordinate continuous map has the finite-coordinate monomial homomorphism as its underlying map.