The Mackey formula along a continuous homomorphism

Let U be an open subgroup of finite index of a topological group G, M a G-module, and (φ, f) a compatible pair from (G, M) to (H, N): a continuous homomorphism φ : H → G and a coefficient map f : M → N with f (φ h • m) = h • f m. Pulling back a corestricted class along (φ, f) splits over the double cosets φ(H) \ G / U (NSW (1.5.6)):

(φ, f)^* ∘ cor^G_U = ∑_{φ(H) s U} cor^H_{H_s} ∘ (ψ_s, f ∘ s)^*,   H_s = φ⁻¹(sUs⁻¹),

where ψ_s : H → G is the conjugate h ↦ s⁻¹ φ(h) s of φ, which maps H_s into U, and the coefficient map is m ↦ f (s • m) (TauCeti.ContCohomology.explicitMap2_explicitCor2_eq_sum). The representatives s of the double cosets are arbitrary, and so are the continuous homomorphisms ψ_s, given with their values: for a Galois group they arise as maps along conjugate embeddings rather than as conjugates of φ.

This is the form in which corestriction is localized: for the decomposition map φ : G_{K_v} → G_K of a place v of a number field K, the double cosets φ(G_{K_v}) \ G_K / U classically index the places w above v of the fixed field F of U, and H_s is the absolute Galois group of the completion F_w.

The proof factors φ through its range D = φ(H). The subgroup Mackey formula (TauCeti.ContCohomology.explicitCor2_mackey) computes the restriction of cor^G_U to D, and the surjection H → D induces bijections H ⧸ φ⁻¹(D ⊓ sUs⁻¹) ≃ D ⧸ (D ⊓ sUs⁻¹), so pullback along it commutes with each corestriction cor^D_{D ⊓ sUs⁻¹} (TauCeti.ContCohomology.explicitCor2_pullback).

Main results

• TauCeti.ContCohomology.explicitMap2_explicitCor2_eq_sum: the Mackey formula for pullback of degree-two corestriction along a continuous homomorphism.

References

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

theorem TauCeti.ContCohomology.comp_toAddMonoidHom_subgroupComap_smul {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] {M : Type w} {N : Type z} [AddCommGroup M] [AddCommGroup N] [DistribMulAction G M] [DistribMulAction H N] (φ : H →ₜ* G) (f : M →+ N) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (U : Subgroup G) (s : G) (ψ : H →ₜ* G) (hψ : ∀ (h : H), ψ h = s⁻¹ * φ h * s) (x : ↥(Subgroup.comap (↑ψ) U)) (m : M) : (f.comp (DistribSMul.toAddMonoidHom M s)) ((ψ.subgroupComap U) x • m) = x • (f.comp (DistribSMul.toAddMonoidHom M s)) m

The conjugate of a compatible pair: if ψ h = s⁻¹ φ(h) s for all h, then ψ, restricted to the preimage of U, and the coefficient map m ↦ f (s • m) form a compatible pair.

theorem TauCeti.ContCohomology.explicitMap2_explicitCor2_eq_sum {G : Type u} {H : Type v} [Group G] [Group H] [TopologicalSpace G] [TopologicalSpace H] {M : Type w} {N : Type z} [AddCommGroup M] [AddCommGroup N] [DistribMulAction G M] [DistribMulAction H N] (φ : H →ₜ* G) (f : M →+ N) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (U : Subgroup G) [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul G M] [TopologicalSpace N] [IsTopologicalAddGroup N] [ContinuousSMul H N] [IsTopologicalGroup G] [ContinuousMul H] (hf : Continuous ⇑f) [U.FiniteIndex] (hU : IsOpen ↑U) (r : DoubleCoset.Quotient ↑(↑φ).range ↑U → G) (hr : ∀ (D : DoubleCoset.Quotient ↑(↑φ).range ↑U), DoubleCoset.mk (↑φ).range U (r D) = D) (ψ : DoubleCoset.Quotient ↑(↑φ).range ↑U → H →ₜ* G) (hψ : ∀ (D : DoubleCoset.Quotient ↑(↑φ).range ↑U) (h : H), (ψ D) h = (r D)⁻¹ * φ h * r D) (x : H2 (↥U) M) : (explicitMap2 G M H N φ f hf hequiv) ((explicitCor2 G M U hU) x) = ∑ D : DoubleCoset.Quotient ↑(↑φ).range ↑U, (explicitCor2 H N (Subgroup.comap (↑(ψ D)) U) ⋯) ((explicitMap2 (↥U) M (↥(Subgroup.comap (↑(ψ D)) U)) N ((ψ D).subgroupComap U) (f.comp (DistribSMul.toAddMonoidHom M (r D))) ⋯ ⋯) x)

The Mackey formula along a continuous homomorphism (NSW (1.5.6)): for a compatible pair (φ, f) and an open subgroup U of finite index, pulling back the corestriction of a class x ∈ H²(U, M) along (φ, f) is the sum over the double cosets φ(H) \ G / U of the corestrictions from H_s = ψ_s⁻¹(U) = φ⁻¹(sUs⁻¹) of the pullbacks of x along ψ_s and m ↦ f (s • m), for any choice of representatives s = r D and any continuous homomorphisms ψ_s with ψ_s h = s⁻¹ φ(h) s.