Corestriction in every degree

For an open subgroup U of finite index in a profinite group G and a discrete G-module M, corestriction cor : Hⁿ(U, M) ⟶ Hⁿ(G, M) is defined on Mathlib's canonical continuous cohomology in every degree n, with no cochain formula, as the composite

Hⁿ(U, M) ≅ Hⁿ(G, Coind_U^G M) ⟶ Hⁿ(G, M)

of the inverse of Shapiro's isomorphism TauCeti.ContinuousCohomology.shapiroIso and the coefficient map of the trace Coind_U^G M → M, f ↦ ∑_{gU ∈ G ⧸ U} g • f g⁻¹ (TauCeti.DiscreteCoind.trace). This is the coinduced-module construction of the transfer in Brown, Cohomology of Groups, III §9; it is the classical cohomological corestriction of Neukirch–Schmidt–Wingberg I §5, not the covariant functoriality of group homology that Mathlib's groupCohomology files call by the same name.

The identity cor ∘ res = [G : U] (NSW (1.5.7)) rests on the unit M → Coind_U^G M, m ↦ (g ↦ g • m), of coinduction (TauCeti.DiscreteCoind.unit), through two facts: restriction followed by the inverse of Shapiro's isomorphism is the coefficient map of the unit (TauCeti.ContinuousCohomology.res_comp_shapiroIso_inv), and the trace of the unit is multiplication by the index (TauCeti.DiscreteCoind.trace_unit). Corestriction is natural in the coefficient module, and in degrees 0, 1 and 2 it agrees, under the comparison isomorphisms with the explicit inhomogeneous model, with the transversal formulas TauCeti.ContCohomology.explicitCor0, TauCeti.ContCohomology.explicitCor1 and TauCeti.ContCohomology.explicitCor2.

The same construction applies to a smooth discrete representation A : TopRep R G over an arbitrary ring R: TauCeti.ContinuousCohomology.corestrictionTopRep is the inverse of the generic Shapiro isomorphism TauCeti.ContinuousCohomology.shapiroIsoTopRep followed by the coefficient map of the trace morphism TauCeti.coindTraceHom. This is the corestriction used by the projection formula for cup products over an arbitrary coefficient ring.

Main definitions

• TauCeti.ContinuousCohomology.corestriction: corestriction Hⁿ(U, M) ⟶ Hⁿ(G, M) in every degree, for an open finite-index subgroup U of a profinite group G.
• TauCeti.ContinuousCohomology.corestrictionTopRep: corestriction for smooth discrete representations over an arbitrary ring, for an open subgroup U of a profinite group G.

Main results

• TauCeti.ContinuousCohomology.shapiroMap_comp_corestriction: the Shapiro map followed by corestriction is the coefficient map of the trace; TauCeti.ContinuousCohomology.shapiroMapTopRep_comp_corestrictionTopRep is the same statement for smooth discrete representations over an arbitrary ring.
• TauCeti.ContinuousCohomology.res_comp_corestriction, TauCeti.ContinuousCohomology.corestriction_res: cor ∘ res = [G : U] • id in every degree.
• TauCeti.ContinuousCohomology.corestriction_naturality: corestriction is natural in the coefficient module.
• TauCeti.ContinuousCohomology.explicitH0Iso_corestriction, TauCeti.ContinuousCohomology.explicitH1AddEquivContinuousCohomology_corestriction, TauCeti.ContinuousCohomology.explicitH2AddEquivContinuousCohomology_corestriction: agreement with the explicit corestrictions in degrees 0, 1 and 2.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §9, the coinduced-module construction of the transfer, and (9.5).
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.7) and (1.6.4).

Corestriction

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

Corestriction in every degree, cor : Hⁿ(U, M) ⟶ Hⁿ(G, M), for an open finite-index subgroup U of a profinite group G and a discrete G-module M: the inverse of Shapiro's isomorphism Hⁿ(G, Coind_U^G M) ≅ Hⁿ(U, M) followed by the coefficient map of the trace Coind_U^G M → M, f ↦ ∑_{gU} g • f g⁻¹. This is the classical cohomological corestriction (transfer), normalized by cor ∘ res = [G : U] (res_comp_corestriction), and it is characterized by shapiroMap_comp_corestriction.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ContinuousCohomology.corestriction_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : corestriction U M hU n = CategoryTheory.CategoryStruct.comp (shapiroIso U ⋯ M n).inv (coeffMap (ofDiscreteModuleMap (DiscreteCoind.trace G U M).toAddMonoidHom.toIntLinearMap ⋯) n)

The defining equation of corestriction: the inverse of Shapiro's isomorphism followed by the coefficient map of the trace Coind_U^G M → M.

@[simp]

theorem TauCeti.ContinuousCohomology.shapiroMap_comp_corestriction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : CategoryTheory.CategoryStruct.comp (shapiroMap U M n) (corestriction U M hU n) = coeffMap (ofDiscreteModuleMap (DiscreteCoind.trace G U M).toAddMonoidHom.toIntLinearMap ⋯) n

The Shapiro map followed by corestriction is the coefficient map of the trace. This is the characteristic property of corestriction: it is the unique map Hⁿ(U, M) ⟶ Hⁿ(G, M) whose composite with the Shapiro isomorphism is the coefficient map of Coind_U^G M → M.

@[simp]

theorem TauCeti.ContinuousCohomology.shapiroMap_comp_corestriction_assoc {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) {Z : TopModuleCat ℤ} (h : continuousCohomology n (ofDiscreteModule ℤ G M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (shapiroMap U M n) (CategoryTheory.CategoryStruct.comp (corestriction U M hU n) h) = CategoryTheory.CategoryStruct.comp (coeffMap (ofDiscreteModuleMap (DiscreteCoind.trace G U M).toAddMonoidHom.toIntLinearMap ⋯) n) h

The Shapiro map followed by corestriction is the coefficient map of the trace. This is the characteristic property of corestriction: it is the unique map Hⁿ(U, M) ⟶ Hⁿ(G, M) whose composite with the Shapiro isomorphism is the coefficient map of Coind_U^G M → M.

theorem TauCeti.ContinuousCohomology.res_comp_corestriction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : CategoryTheory.CategoryStruct.comp (res U (ofDiscreteModule ℤ G M) n) (corestriction U M hU n) = U.index • CategoryTheory.CategoryStruct.id (continuousCohomology n (ofDiscreteModule ℤ G M))

cor ∘ res = [G : U] in every degree (NSW (1.5.7)): restriction to an open finite-index subgroup U followed by corestriction is multiplication by the index [G : U] on Hⁿ(G, M).

@[simp]

theorem TauCeti.ContinuousCohomology.corestriction_res {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) (x : ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (corestriction U M hU n)) ((CategoryTheory.ConcreteCategory.hom (res U (ofDiscreteModule ℤ G M) n)) x) = U.index • x

cor (res x) = [G : U] • x for every class x ∈ Hⁿ(G, M) (NSW (1.5.7)).

Naturality in the coefficients

theorem TauCeti.ContinuousCohomology.corestriction_naturality {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] {N : Type u} [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (n : ℕ) : CategoryTheory.CategoryStruct.comp (corestriction U M hU n) (coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) n) = CategoryTheory.CategoryStruct.comp (coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) n) (corestriction U N hU n)

Corestriction is natural in the coefficient module: for a G-equivariant homomorphism f : M → N of discrete G-modules, corestriction followed by the coefficient map of f over G is the coefficient map of f over U followed by corestriction.

theorem TauCeti.ContinuousCohomology.corestriction_naturality_assoc {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] {N : Type u} [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (n : ℕ) {Z : TopModuleCat ℤ} (h : continuousCohomology n (ofDiscreteModule ℤ G N) ⟶ Z) : CategoryTheory.CategoryStruct.comp (corestriction U M hU n) (CategoryTheory.CategoryStruct.comp (coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) n) h) = CategoryTheory.CategoryStruct.comp (coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) n) (CategoryTheory.CategoryStruct.comp (corestriction U N hU n) h)

Corestriction is natural in the coefficient module: for a G-equivariant homomorphism f : M → N of discrete G-modules, corestriction followed by the coefficient map of f over G is the coefficient map of f over U followed by corestriction.

Agreement with the explicit corestrictions

theorem TauCeti.ContinuousCohomology.explicitH0Iso_corestriction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] (x : ↥(ContCohomology.H0 (↥U) M)) : (CategoryTheory.ConcreteCategory.hom (corestriction U M hU 0)) ((CategoryTheory.ConcreteCategory.hom (ContCohomology.explicitH0IsoContinuousCohomology (↥U) M).hom) x) = (CategoryTheory.ConcreteCategory.hom (ContCohomology.explicitH0IsoContinuousCohomology G M).hom) ((ContCohomology.explicitCor0 G M U) x)

In degree zero, corestriction is the explicit norm m ↦ ∑_{gU} g • m of TauCeti.ContCohomology.explicitCor0, under the comparisons of H⁰ with the canonical carrier.

theorem TauCeti.ContinuousCohomology.explicitH1AddEquivContinuousCohomology_corestriction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] (x : ContCohomology.H1 (↥U) M) : (CategoryTheory.ConcreteCategory.hom (corestriction U M hU 1)) ((ContCohomology.explicitH1AddEquivContinuousCohomology (↥U) M) x) = (ContCohomology.explicitH1AddEquivContinuousCohomology G M) ((ContCohomology.explicitCor1 G M U hU) x)

In degree one, corestriction is the explicit transversal formula of TauCeti.ContCohomology.explicitCor1, under the comparisons of H¹ with the canonical carrier.

theorem TauCeti.ContinuousCohomology.explicitH2AddEquivContinuousCohomology_corestriction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] (hU : IsOpen ↑U) [U.FiniteIndex] (x : ContCohomology.H2 (↥U) M) : (CategoryTheory.ConcreteCategory.hom (corestriction U M hU 2)) ((ContCohomology.explicitH2AddEquivContinuousCohomology (↥U) M) x) = (ContCohomology.explicitH2AddEquivContinuousCohomology G M) ((ContCohomology.explicitCor2 G M U hU) x)

In degree two, corestriction is the explicit transversal formula of TauCeti.ContCohomology.explicitCor2, under the comparisons of H² with the canonical carrier. The degree-two comparison for U needs U to be locally compact, which holds because U is closed in the compact group G.

Corestriction for smooth discrete topological representations

noncomputable def TauCeti.ContinuousCohomology.corestrictionTopRep {R : Type v} [Ring R] [TopologicalSpace R] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R G) (hU : IsOpen ↑U) (n : ℕ) : continuousCohomology n (smoothDiscreteResTopRep U A).obj ⟶ continuousCohomology n A.obj

Corestriction for a smooth discrete topological representation over an arbitrary ring: the inverse of the generic Shapiro isomorphism followed by the coefficient map of the trace. An open subgroup of the compact group G has finite index, so the trace is available.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ContinuousCohomology.corestrictionTopRep_def {R : Type v} [Ring R] [TopologicalSpace R] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : corestrictionTopRep U A hU n = CategoryTheory.CategoryStruct.comp (shapiroIsoTopRep U ⋯ (smoothDiscreteResTopRep U A) n).inv (coeffMap (coindTraceHom R G U A) n)

The defining equation of corestrictionTopRep: the inverse of the generic Shapiro isomorphism followed by the coefficient map of the trace.

@[simp]

theorem TauCeti.ContinuousCohomology.shapiroMapTopRep_comp_corestrictionTopRep {R : Type v} [Ring R] [TopologicalSpace R] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) : CategoryTheory.CategoryStruct.comp (shapiroMapTopRep U (smoothDiscreteResTopRep U A) n) (corestrictionTopRep U A hU n) = coeffMap (coindTraceHom R G U A) n

The generic Shapiro map followed by corestriction is the coefficient map of the trace, the characteristic property of corestrictionTopRep.

@[simp]

theorem TauCeti.ContinuousCohomology.shapiroMapTopRep_comp_corestrictionTopRep_assoc {R : Type v} [Ring R] [TopologicalSpace R] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) {Z : TopModuleCat R} (h : continuousCohomology n A.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp (shapiroMapTopRep U (smoothDiscreteResTopRep U A) n) (CategoryTheory.CategoryStruct.comp (corestrictionTopRep U A hU n) h) = CategoryTheory.CategoryStruct.comp (coeffMap (coindTraceHom R G U A) n) h

The generic Shapiro map followed by corestriction is the coefficient map of the trace, the characteristic property of corestrictionTopRep.

theorem TauCeti.ContinuousCohomology.corestrictionTopRep_shapiroMapTopRep_apply {R : Type v} [Ring R] [TopologicalSpace R] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R G) (hU : IsOpen ↑U) [U.FiniteIndex] (n : ℕ) (c : ↑(continuousCohomology n (coindTopRep R G U (smoothDiscreteResTopRep U A)).obj).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (corestrictionTopRep U A hU n)) ((CategoryTheory.ConcreteCategory.hom (shapiroMapTopRep U (smoothDiscreteResTopRep U A) n)) c) = (CategoryTheory.ConcreteCategory.hom (coeffMap (coindTraceHom R G U A) n)) c

Applying corestriction after the generic Shapiro map is the coefficient map of the trace.