The Mackey double-coset formula in every degree

Let U be an open subgroup and V a closed subgroup of a profinite group G, and M a discrete G-module. The Mackey double-coset formula (NSW (1.5.6)) computes restriction to V of the corestriction from U on Mathlib's canonical continuous cohomology, in every degree n:

res^G_V ∘ cor^G_U = ∑_{VsU ∈ V \ G / U} cor^V_{V ⊓ sUs⁻¹} ∘ (s)_* ∘ res^U_{U ⊓ s⁻¹Vs},

for any choice r of representatives s = r D of the double cosets. As in degrees 0, 1, 2 (TauCeti.ContCohomology.explicitCor0_mackey and its companions), the composite (s)_* ∘ res^U_{U ⊓ s⁻¹Vs} is the single compatible-pair map along Subgroup.continuousMackeyToH : V ⊓ sUs⁻¹ → U, y ↦ s⁻¹ y s, with coefficient map m ↦ s • m, and the summand TauCeti.ContinuousCohomology.mackeyTerm follows it with the all-degree corestriction from the Mackey subgroup V ⊓ sUs⁻¹, which is open in the profinite group V.

There is no cochain formula in arbitrary degree; the formula is read off from coinduced modules. Corestriction is the inverse of Shapiro's isomorphism followed by the coefficient map of the trace Coind_U^G M → M, so after Shapiro's isomorphism for U both sides become coefficient maps Hⁿ(G, Coind_U^G M) ⟶ Hⁿ(G, Coind_V^G M) followed by the Shapiro map of V:

• on the left, by TauCeti.ContinuousCohomology.coeffMap_unit_comp_shapiroMap, the coefficient map of the trace followed by the unit M → Coind_V^G M;
• on the right, the coefficient map of Φ ↦ (x ↦ ∑_w w s • Φ (s⁻¹ w⁻¹ x)), the sum over V ⧸ (V ⊓ sUs⁻¹): conjugation of coinduced modules (TauCeti.ContinuousCohomology.shapiroMap_comp_map_of_conj, which rests on inner automorphisms acting trivially), transitivity of the Shapiro map (TauCeti.ContinuousCohomology.shapiroMap_trans) and its naturality move the summand there.

The two module maps agree by the double-coset splitting of G ⧸ U (TauCeti.mackeyQuotientEquiv), the trace being computed along the adapted transversal Subgroup.mackeyTransversal. This follows the coinduced-module treatment of the transfer in Brown, Cohomology of Groups, III §9.

Main definitions

• TauCeti.ContinuousCohomology.mackeyTerm: the summand cor^V_{V ⊓ sUs⁻¹} ∘ (s)_* ∘ res attached to s, in every degree.

Main results

• TauCeti.ContinuousCohomology.corestriction_mackey: the Mackey double-coset formula in every degree, for any choice of double-coset representatives.
• TauCeti.ContinuousCohomology.mackeyTerm_eq_of_mk_eq: each summand depends only on the double coset of its representative.

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.

noncomputable def TauCeti.ContinuousCohomology.mackeyTerm {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U V : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hU : IsOpen ↑U) (hV : IsClosed ↑V) [U.FiniteIndex] (s : G) (n : ℕ) : continuousCohomology n (ofDiscreteModule ℤ (↥U) M) ⟶ continuousCohomology n (ofDiscreteModule ℤ (↥V) M)

One summand of the Mackey double-coset formula, cor^V_{V ⊓ sUs⁻¹} ∘ (s)_* ∘ res, in every degree: the map of the compatible pair of V ⊓ sUs⁻¹ → U, y ↦ s⁻¹ y s, and of the action of s on M, followed by corestriction from the Mackey subgroup V ⊓ sUs⁻¹ up to V. The subgroup U is open and V is closed in the profinite group G, so that V is profinite and the Mackey subgroup is open in V.

theorem TauCeti.ContinuousCohomology.mackeyTerm_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U V : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hU : IsOpen ↑U) (hV : IsClosed ↑V) [U.FiniteIndex] (s : G) (n : ℕ) : mackeyTerm U V M hU hV s n = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map (U.continuousMackeyToH V s) (ofDiscreteModulePair (↑(U.continuousMackeyToH V s)) (DistribSMul.toAddMonoidHom M s).toIntLinearMap ⋯) n) (corestriction ((mackeySubgroup s U V).subgroupOf V) M ⋯ n)

The defining equation of mackeyTerm: the map of the compatible pair of conjugation by s and the action of s, followed by corestriction from the Mackey subgroup up to V.

theorem TauCeti.ContinuousCohomology.corestriction_mackey {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U V : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hU : IsOpen ↑U) (hV : IsClosed ↑V) [U.FiniteIndex] (r : DoubleCoset.Quotient ↑V ↑U → G) (hr : ∀ (D : DoubleCoset.Quotient ↑V ↑U), DoubleCoset.mk V U (r D) = D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (corestriction U M hU n) (res V (ofDiscreteModule ℤ G M) n) = ∑ D : DoubleCoset.Quotient ↑V ↑U, mackeyTerm U V M hU hV (r D) n

The Mackey double-coset formula in every degree (NSW (1.5.6)). For an open subgroup U of finite index and a closed subgroup V of a profinite group G, and a discrete G-module M, restriction to V of the corestriction from U is the sum over the double cosets V \ G / U of the summands cor^V_{V ⊓ sUs⁻¹} ∘ (s)_* ∘ res, for any choice r of representatives s = r D of the double cosets:

res^G_V ∘ cor^G_U = ∑_{VsU ∈ V \ G / U} cor^V_{V ⊓ sUs⁻¹} ∘ (s)_* ∘ res^U_{U ⊓ s⁻¹Vs}.

theorem TauCeti.ContinuousCohomology.mackeyTerm_eq_of_mk_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U V : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hU : IsOpen ↑U) (hV : IsClosed ↑V) [U.FiniteIndex] {s s' : G} (h : DoubleCoset.mk V U s = DoubleCoset.mk V U s') (n : ℕ) : mackeyTerm U V M hU hV s n = mackeyTerm U V M hU hV s' n

Each summand of the Mackey formula depends only on the double coset VsU of s, in every degree.