Corestriction is invariant under conjugation

Let U be an open subgroup of finite index in a profinite group G, let g : G, and let V = gUg⁻¹. Conjugation κ : V → U, v ↦ g⁻¹ v g, together with the action of g on a discrete G-module M, is a compatible pair, and so induces a map (g)_* : Hⁿ(U, M) ⟶ Hⁿ(V, M). This file proves that corestriction does not see it, in every degree:

cor_V ∘ (g)_* = cor_U : Hⁿ(U, M) ⟶ Hⁿ(G, M).

Corestriction from a subgroup therefore depends on that subgroup only through its conjugacy class, once the subgroups in the class are identified by conjugation; for instance, corestriction along a finite field extension L/K does not depend on the embedding of L into the separable closure of K (TauCeti.galoisCor_embedding_independent).

The proof runs through Shapiro's lemma, by which corestriction is the coefficient map of the trace Coind_U^G M → M read through the Shapiro isomorphism. Conjugation by g gives a G-equivariant map of coinduced modules TauCeti.DiscreteCoind.conj : Coind_U^G M → Coind_V^G M, f ↦ (x ↦ g • f (g⁻¹ x)), which commutes with the traces (TauCeti.DiscreteCoind.trace_conj). On the Shapiro side, the two ways of passing from Hⁿ(G, Coind_U^G M) to Hⁿ(V, M) differ by the compatible pair of the inner automorphism x ↦ g⁻¹ x g of G and the action of g, which acts trivially on cohomology (TauCeti.ContinuousCohomology.map_eq_id_of_inner).

For a normal subgroup V, conjugation v ↦ g⁻¹ v g of V and the action of g form a compatible pair, which induces the endomorphism (g)_* of Hⁿ(V, M) (TauCeti.ContinuousCohomology.conjNormalMap), the conjugation through which NSW (3.3.11) describes the kernel of corestriction. Under Shapiro's map it is the coefficient map of the conjugation f ↦ (x ↦ g • f (g⁻¹ x)) of Coind_V^G M.

Main definitions

• TauCeti.ContinuousCohomology.conjNormalMap: the conjugation (g)_* on Hⁿ(V, M) for a normal subgroup V, in every degree.

Main results

• TauCeti.ContinuousCohomology.shapiroMap_comp_map_of_conj: the Shapiro maps intertwine the conjugation (g)_* with the coefficient map of the conjugation of coinduced modules.
• TauCeti.ContinuousCohomology.map_comp_corestriction_of_conj: corestriction from gUg⁻¹ after conjugation (g)_* is corestriction from U, in every degree.
• TauCeti.trivialF2Map_comp_trivialF2CorMap_of_conj: the same statement with trivial 𝔽₂ coefficients, where (g)_* is pullback along κ.
• TauCeti.ContCohomology.explicitCor2_explicitMap2_of_conj: the same statement in degree two for the explicit inhomogeneous model, with the transversal corestriction explicitCor2.
• TauCeti.ContinuousCohomology.shapiroMap_comp_conjNormalMap: for a normal subgroup, Shapiro's map intertwines (g)_* with the conjugation of Coind_V^G M.
• TauCeti.ContinuousCohomology.conjNormalMap_one, TauCeti.ContinuousCohomology.conjNormalMap_comp: g ↦ (g)_* is an action of G on Hⁿ(V, M), (1)_* = 𝟙 and (g)_* ≫ (h)_* = (h * g)_*.
• TauCeti.ContinuousCohomology.conjNormalMap_naturality: (g)_* is natural in the coefficients.
• TauCeti.ContinuousCohomology.conjNormalMap_eq_map_of_smul_eq_self: with trivial coefficients, (g)_* is the pullback along conjugation alone.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §5, for the conjugation maps g_* and their compatibility with corestriction.
• K. S. Brown, Cohomology of Groups, Chapter III, §§8–9, for conjugation on cohomology and the coinduced-module construction of the transfer.

Corestriction and conjugation

theorem TauCeti.ContinuousCohomology.shapiroMap_comp_map_of_conj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U V : Subgroup G) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (g : G) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = g⁻¹ * ↑v * g) (f : TopRep.res (↑κ) (ofDiscreteModule ℤ (↥U) M) ⟶ ofDiscreteModule ℤ (↥V) M) (hf : ∀ (m : M), (TopRep.Hom.hom f) m = g • m) (hVU : V ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) (n : ℕ) : CategoryTheory.CategoryStruct.comp (shapiroMap U M n) (ContinuousCohomology.map κ f n) = CategoryTheory.CategoryStruct.comp (coeffMap (ofDiscreteModuleMap (DiscreteCoind.conj U V M g hVU).toAddMonoidHom.toIntLinearMap ⋯) n) (shapiroMap V M n)

The Shapiro map intertwines conjugation: Shapiro's map for U followed by the conjugation (g)_* is the coefficient map of the conjugation Coind_U^G M → Coind_V^G M followed by Shapiro's map for V. Both are compatible-pair maps from Hⁿ(G, Coind_U^G M) to Hⁿ(V, M); they differ by the pair of the inner automorphism x ↦ g⁻¹ x g of G and the action of g, which induces the identity. Compactness ensures that the right-translation action on the discrete coinduced module is continuous.

theorem TauCeti.ContinuousCohomology.map_comp_corestriction_of_conj {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] (g : G) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = g⁻¹ * ↑v * g) (f : TopRep.res (↑κ) (ofDiscreteModule ℤ (↥U) M) ⟶ ofDiscreteModule ℤ (↥V) M) (hf : ∀ (m : M), (TopRep.Hom.hom f) m = g • m) (hVU : V = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) (hU : IsOpen ↑U) [U.FiniteIndex] (hV : IsOpen ↑V) [V.FiniteIndex] (n : ℕ) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map κ f n) (corestriction V M hV n) = corestriction U M hU n

Corestriction is invariant under conjugation, in every degree: for g : G, an open subgroup U of finite index and V = gUg⁻¹, corestriction from V after the conjugation (g)_* : Hⁿ(U, M) ⟶ Hⁿ(V, M) is corestriction from U. Here (g)_* is the map of the compatible pair of κ : V → U, v ↦ g⁻¹ v g, and the action of g on M; both are taken as hypotheses on their values, so that the statement applies to any presentation of the pair.

theorem TauCeti.ContinuousCohomology.map_comp_corestriction_of_conj_assoc {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] (g : G) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = g⁻¹ * ↑v * g) (f : TopRep.res (↑κ) (ofDiscreteModule ℤ (↥U) M) ⟶ ofDiscreteModule ℤ (↥V) M) (hf : ∀ (m : M), (TopRep.Hom.hom f) m = g • m) (hVU : V = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) (hU : IsOpen ↑U) [U.FiniteIndex] (hV : IsOpen ↑V) [V.FiniteIndex] (n : ℕ) {Z : TopModuleCat ℤ} (h : continuousCohomology n (ofDiscreteModule ℤ G M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map κ f n) (CategoryTheory.CategoryStruct.comp (corestriction V M hV n) h) = CategoryTheory.CategoryStruct.comp (corestriction U M hU n) h

Corestriction is invariant under conjugation, in every degree: for g : G, an open subgroup U of finite index and V = gUg⁻¹, corestriction from V after the conjugation (g)_* : Hⁿ(U, M) ⟶ Hⁿ(V, M) is corestriction from U. Here (g)_* is the map of the compatible pair of κ : V → U, v ↦ g⁻¹ v g, and the action of g on M; both are taken as hypotheses on their values, so that the statement applies to any presentation of the pair.

Conjugation on the cohomology of a normal subgroup

noncomputable def TauCeti.ContinuousCohomology.conjNormalPair {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (g : G) : TopRep.res (↑↑(ContinuousAut.conjNormal g⁻¹)) (ofDiscreteModule ℤ (↥V) M) ⟶ ofDiscreteModule ℤ (↥V) M

The compatible pair of conjugation v ↦ g⁻¹ v g of the normal subgroup V (TauCeti.ContinuousAut.conjNormal g⁻¹) and the action of g on M, which induces conjNormalMap.

Equations

• TauCeti.ContinuousCohomology.conjNormalPair V M g = TauCeti.ofDiscreteModulePair (↑↑(TauCeti.ContinuousAut.conjNormal g⁻¹)) (DistribSMul.toAddMonoidHom M g).toIntLinearMap ⋯

@[simp]

theorem TauCeti.ContinuousCohomology.conjNormalPair_hom_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (g : G) (m : M) : (TopRep.Hom.hom (conjNormalPair V M g)) m = g • m

The compatible pair conjNormalPair V M g acts on M as g.

noncomputable def TauCeti.ContinuousCohomology.conjNormalMap {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (g : G) (n : ℕ) : continuousCohomology n (ofDiscreteModule ℤ (↥V) M) ⟶ continuousCohomology n (ofDiscreteModule ℤ (↥V) M)

Conjugation on the cohomology of a normal subgroup, (g)_* : Hⁿ(V, M) ⟶ Hⁿ(V, M) in every degree: the map of the compatible pair of v ↦ g⁻¹ v g and the action of g on M.

Equations

• TauCeti.ContinuousCohomology.conjNormalMap V M g n = ContinuousCohomology.map (↑(TauCeti.ContinuousAut.conjNormal g⁻¹)) (TauCeti.ContinuousCohomology.conjNormalPair V M g) n

theorem TauCeti.ContinuousCohomology.conjNormalMap_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (g : G) (n : ℕ) : conjNormalMap V M g n = ContinuousCohomology.map (↑(ContinuousAut.conjNormal g⁻¹)) (conjNormalPair V M g) n

The defining equation of conjNormalMap: the map of the compatible pair conjNormalPair.

@[simp]

theorem TauCeti.ContinuousCohomology.conjNormalMap_one {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (n : ℕ) : conjNormalMap V M 1 n = CategoryTheory.CategoryStruct.id (continuousCohomology n (ofDiscreteModule ℤ (↥V) M))

Conjugation by 1 is the identity of Hⁿ(V, M).

theorem TauCeti.ContinuousCohomology.conjNormalMap_comp {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (g h : G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (conjNormalMap V M g n) (conjNormalMap V M h n) = conjNormalMap V M (h * g) n

Conjugation is multiplicative: conjugation by g followed by conjugation by h is conjugation by h * g.

theorem TauCeti.ContinuousCohomology.conjNormalMap_comp_assoc {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (g h : G) (n : ℕ) {Z : TopModuleCat ℤ} (h✝ : continuousCohomology n (ofDiscreteModule ℤ (↥V) M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (conjNormalMap V M g n) (CategoryTheory.CategoryStruct.comp (conjNormalMap V M h n) h✝) = CategoryTheory.CategoryStruct.comp (conjNormalMap V M (h * g) n) h✝

Conjugation is multiplicative: conjugation by g followed by conjugation by h is conjugation by h * g.

theorem TauCeti.ContinuousCohomology.shapiroMap_comp_conjNormalMap {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [CompactSpace G] (g : G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (shapiroMap V M n) (conjNormalMap V M g n) = CategoryTheory.CategoryStruct.comp (coeffMap (ofDiscreteModuleMap (DiscreteCoind.conj V V M g ⋯).toAddMonoidHom.toIntLinearMap ⋯) n) (shapiroMap V M n)

Shapiro's map intertwines conjugation: for a normal subgroup V, Shapiro's map followed by (g)_* is the coefficient map of the conjugation of Coind_V^G M by g, followed by Shapiro's map.

theorem TauCeti.ContinuousCohomology.conjNormalMap_naturality {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (N : Type u) [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] (f : M →+[G] N) (g : G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (conjNormalMap V M g n) (coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) n) = CategoryTheory.CategoryStruct.comp (coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) n) (conjNormalMap V N g n)

Conjugation is natural in the coefficients: for a G-equivariant map f : M → N, the coefficient map of f on Hⁿ(V, -) commutes with (g)_*.

theorem TauCeti.ContinuousCohomology.conjNormalMap_eq_map_of_smul_eq_self {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (htriv : ∀ (g : G) (m : M), g • m = m) (g : G) (n : ℕ) : conjNormalMap V M g n = ContinuousCohomology.map (↑(ContinuousAut.conjNormal g⁻¹)) (ofDiscreteModulePair (↑↑(ContinuousAut.conjNormal g⁻¹)) (AddMonoidHom.id M).toIntLinearMap ⋯) n

Conjugation with trivial coefficients is the pullback along v ↦ g⁻¹ v g alone: when G acts trivially on M, (g)_* is the map of the compatible pair of this conjugation and the identity of M.

Trivial 𝔽₂ coefficients

theorem TauCeti.trivialF2Map_comp_trivialF2CorMap_of_conj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U V : Subgroup G} (hU : IsOpen ↑U) [U.FiniteIndex] (hV : IsOpen ↑V) [V.FiniteIndex] (g : G) (hVU : V = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = g⁻¹ * ↑v * g) (n : ℕ) : CategoryTheory.CategoryStruct.comp (trivialF2Map κ n) (trivialF2CorMap G V hV n) = trivialF2CorMap G U hU n

Corestriction with trivial 𝔽₂ coefficients is invariant under conjugation, in every degree: for g : G, an open subgroup U of finite index and V = gUg⁻¹, pullback along any continuous κ : V → U with κ v = g⁻¹ v g followed by corestriction from V is corestriction from U.

theorem TauCeti.trivialF2Map_comp_trivialF2CorMap_of_conj_assoc {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U V : Subgroup G} (hU : IsOpen ↑U) [U.FiniteIndex] (hV : IsOpen ↑V) [V.FiniteIndex] (g : G) (hVU : V = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = g⁻¹ * ↑v * g) (n : ℕ) {Z : TopModuleCat ℤ} (h : continuousCohomology n (trivialF2 G) ⟶ Z) : CategoryTheory.CategoryStruct.comp (trivialF2Map κ n) (CategoryTheory.CategoryStruct.comp (trivialF2CorMap G V hV n) h) = CategoryTheory.CategoryStruct.comp (trivialF2CorMap G U hU n) h

Corestriction with trivial 𝔽₂ coefficients is invariant under conjugation, in every degree: for g : G, an open subgroup U of finite index and V = gUg⁻¹, pullback along any continuous κ : V → U with κ v = g⁻¹ v g followed by corestriction from V is corestriction from U.

Degree two in the explicit model

theorem TauCeti.ContCohomology.explicitCor2_explicitMap2_of_conj {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] (g : G) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = g⁻¹ * ↑v * g) (f : M →+ M) (hf : ∀ (m : M), f m = g • m) (hVU : V = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) (hU : IsOpen ↑U) [U.FiniteIndex] (hV : IsOpen ↑V) [V.FiniteIndex] (x : H2 (↥U) M) : (explicitCor2 G M V hV) ((explicitMap2 (↥U) M (↥V) M κ f ⋯ ⋯) x) = (explicitCor2 G M U hU) x

Degree-two corestriction is invariant under conjugation, in the explicit inhomogeneous model: for g : G, an open subgroup U of finite index and V = gUg⁻¹, the explicit corestriction from V after the conjugation (g)_* : H²(U, M) → H²(V, M) is the explicit corestriction from U. As in TauCeti.ContinuousCohomology.map_comp_corestriction_of_conj, (g)_* is the map of the compatible pair of κ : V → U, v ↦ g⁻¹ v g, and the action f of g on M, both given through their values.