Continuity of transfer

For an open finite-index subgroup U ≤ G, Mathlib's MonoidHom.transfer sends a continuous homomorphism U →* A to a continuous homomorphism G →* A, where A is commutative. The formula transfer_eq_prod_lWord computes this transfer using the same transversal words as continuous cohomological corestriction. It is valid for every transversal, without topology; continuity then follows from continuous_lWord.

Only separate continuity of multiplication on G and continuity of multiplication on A are needed. Neither compactness of G nor discreteness of A is required.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §9.
• Neukirch--Schmidt--Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.9).

The algebraic transfer is Mathlib's MonoidHom.transfer; the transversal computation uses MonoidHom.transfer_eq_prod_of_bijective.

theorem TauCeti.continuous_transfer {G : Type u_1} {A : Type u_2} [Group G] [CommGroup A] {U : Subgroup G} [U.FiniteIndex] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace A] [ContinuousMul A] (hU : IsOpen ↑U) {φ : ↥U →* A} (hφ : Continuous ⇑φ) : Continuous ⇑φ.transfer

Transfer from an open finite-index subgroup preserves continuity. The commutative target need not be discrete, and the ambient group need not be compact.