Descent along a normal subgroup of index prime to the coefficients

Let N be an open normal subgroup of finite index in a topological group G, and let M be a continuous G-module killed by an integer e prime to the index [G : N]. Then restriction identifies the low-degree cohomology of G with the invariants of the conjugation action on that of N:

H⁰(G, M) ≃ H⁰(N, M)^{G/N},    H¹(G, M) ≃ H¹(N, M)^{G/N}.

In degree zero this is the equality M^G = (M^N)^G and needs no hypothesis on the index (TauCeti.ContCohomology.explicitRes0_injective, TauCeti.ContCohomology.mem_range_explicitRes0_iff). In degree one it rests on two composites of restriction and the corestriction TauCeti.ContCohomology.explicitCor1:

• cor ∘ res = [G : N] on H¹(G, M) (TauCeti.ContCohomology.explicitCor1_comp_res1, for any open subgroup of finite index);
• res ∘ cor = ∑_{gN ∈ G/N} g on H¹(N, M), g acting by the conjugation TauCeti.ContCohomology.explicitConj1 (explicitRes1_explicitCor1_of_normal), hence res ∘ cor = [G : N] on the invariants TauCeti.ContCohomology.H1ConjInvariants.

On cochains the second identity holds exactly, for every transversal: when N is normal, the transversal word of an element n ∈ N at the coset u is the conjugate (t u)⁻¹ n (t u) (TauCeti.lWord_of_mem_of_normal), so the corestriction cochain restricted to N is the sum of the conjugates of the cocycle (cochainsCor1_apply_of_mem).

As e kills both H¹(G, M) and H¹(N, M), multiplication by [G : N] is bijective on them (TauCeti.nsmul_right_bijective_of_coprime). So restriction is injective on H¹(G, M) (explicitRes1_injective_of_coprime, for any open subgroup of finite index), and the corestriction divided by [G : N] is a section of it on the invariants, so restriction onto the invariants is bijective (explicitResConj1_bijective_of_coprime).

Main results

• TauCeti.ContCohomology.explicitRes1_explicitCor1_of_normal: res ∘ cor = ∑_{gN} g on H¹(N, M) for a normal subgroup N.
• TauCeti.ContCohomology.explicitRes1_explicitCor1_of_mem_H1ConjInvariants: res (cor x) = [G : N] • x on the conjugation invariants.
• TauCeti.ContCohomology.explicitRes1_injective_of_coprime: restriction to an open subgroup of finite index prime to an exponent of M is injective on H¹.
• TauCeti.ContCohomology.explicitResConj1_bijective_of_coprime: restriction H¹(G, M) → H¹(N, M)^{G/N} is bijective for an open normal subgroup of index prime to an exponent of M.
• TauCeti.h1CoprimeDescentEquiv: for ZMod n-module coefficients, the same restriction is a linear equivalence.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.7), (1.6.2) and the proof of (7.3.1).
• J.-P. Serre, Galois Cohomology, Chapter I, §2.4.

Degree zero

theorem TauCeti.ContCohomology.explicitRes0_injective (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (N : Subgroup G) : Function.Injective ⇑(explicitRes0 G M N)

Restriction in degree zero is injective: it does not change the underlying element.

theorem TauCeti.ContCohomology.mem_range_explicitRes0_iff (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (N : Subgroup G) (x : ↥(H0 (↥N) M)) : x ∈ (explicitRes0 G M N).range ↔ ∀ (g : G), g • ↑x = ↑x

Restriction in degree zero onto the invariants. An N-invariant element is the restriction of a G-invariant one exactly when G fixes it, so H⁰(G, M) → H⁰(N, M)^G is bijective, with no hypothesis on N.

The restriction of a corestriction to a normal subgroup

theorem TauCeti.ContCohomology.cochainsCor1_apply_of_mem (G : Type u) [Group G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] [N.FiniteIndex] (t : G ⧸ N → G) (ht : ∀ (u : G ⧸ N), ↑(t u) = u) (f : ↥N → M) {γ : G} (hγ : γ ∈ N) : (cochainsCor1 G M N t ht) f γ = ∑ u : G ⧸ N, t u • f ⟨(t u)⁻¹ * γ * t u, ⋯⟩

The corestriction cochain on a normal subgroup is a sum of conjugates. For N normal and γ ∈ N, the degree-one corestriction cochain of f : N → M over the transversal t takes the value ∑ u, t u • f ((t u)⁻¹ γ (t u)) at γ.

theorem TauCeti.ContCohomology.explicitRes1_explicitCor1_of_normal (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] [N.FiniteIndex] (hN : IsOpen ↑N) (t : G ⧸ N → G) (ht : ∀ (u : G ⧸ N), ↑(t u) = u) (x : H1 (↥N) M) : (explicitRes1 G M N) ((explicitCor1 G M N hN) x) = ∑ u : G ⧸ N, t u • x

res ∘ cor = ∑_{gN} g on H¹(N, M) for an open normal subgroup N of finite index (NSW (1.5.6) for a normal subgroup): restricting the corestriction of a class is the sum of its conjugates t u • x (TauCeti.ContCohomology.explicitConj1) over any transversal t of G ⧸ N.

theorem TauCeti.ContCohomology.explicitRes1_explicitCor1_of_mem_H1ConjInvariants (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] [N.FiniteIndex] (hN : IsOpen ↑N) {x : H1 (↥N) M} (hx : x ∈ H1ConjInvariants G M N) : (explicitRes1 G M N) ((explicitCor1 G M N hN) x) = N.index • x

res ∘ cor = [G : N] on the conjugation invariants of H¹(N, M), for an open normal subgroup N of finite index.

theorem TauCeti.ContCohomology.explicitRes1_injective_of_coprime {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (U : Subgroup G) [U.FiniteIndex] (hU : IsOpen ↑U) {e : ℕ} (he : ∀ (y : M), e • y = 0) (hcop : U.index.Coprime e) : Function.Injective ⇑(explicitRes1 G M U)

Restriction is injective on H¹ for an index prime to the coefficients. If an integer e prime to the index of the open subgroup U of finite index kills M, then H¹(G, M) → H¹(U, M) is injective, because cor ∘ res = [G : U] is invertible on H¹(G, M).

theorem TauCeti.ContCohomology.explicitResConj1_bijective_of_coprime {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] [N.FiniteIndex] (hN : IsOpen ↑N) {e : ℕ} (he : ∀ (y : M), e • y = 0) (hcop : N.index.Coprime e) : Function.Bijective ⇑(explicitResConj1 G M N)

Restriction onto the conjugation invariants is bijective for an index prime to the coefficients (NSW, proof of (7.3.1)). If N is an open normal subgroup of finite index and an integer e prime to [G : N] kills M, then restriction H¹(G, M) → H¹(N, M)^{G/N} is bijective: cor ∘ res = [G : N] and res ∘ cor = [G : N] on the invariants, and [G : N] is invertible modulo e.

noncomputable def TauCeti.h1CoprimeDescentEquiv {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type v} [AddCommGroup A] [Module (ZMod n) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [N.FiniteIndex] (hopen : IsOpen ↑N) (hcop : N.index.Coprime n) : ContCohomology.H1 G A ≃ₗ[ZMod n] ↥((AddSubgroup.toZModSubmodule n) (ContCohomology.H1ConjInvariants G A N))

Coprime restriction as a linear equivalence onto the conjugation invariants. If N is open and normal of finite index prime to n, restriction identifies H¹(G, A) with the G/N-invariant part of H¹(N, A).

@[simp]

theorem TauCeti.h1CoprimeDescentEquiv_apply {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type v} [AddCommGroup A] [Module (ZMod n) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [N.FiniteIndex] (hopen : IsOpen ↑N) (hcop : N.index.Coprime n) (x : ContCohomology.H1 G A) : ↑((h1CoprimeDescentEquiv hopen hcop) x) = ↑((ContCohomology.explicitResConj1 G A N) x)

The forward map of h1CoprimeDescentEquiv is restriction to the conjugation invariants.