The invariant term in the five-term sequence

Let N be a normal subgroup of a topological group G, and let M be a continuous G-module. Conjugation by G, together with the action on M, acts on the explicit group H¹(N, M). This file defines the subgroup fixed by that action and proves that restriction

H¹(G, M) → H¹(N, M)

lands in it. Thus restriction acquires the codomain needed for the third arrow of the inflation-restriction-transgression five-term sequence.

Although the invariant subgroup is defined by quantifying over G, it is the G ⧸ N-invariant subgroup: elements of N act trivially on H¹(N, M). For a cocycle c on G, invariance of its restriction is witnessed before quotienting by the identity

g • c(g⁻¹ng) - c(n) = n • c(g) - c(g).

The right-hand side is the coboundary of c(g). This is the low-degree cochain calculation underlying the conjugation-invariance of restriction.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.7).
• J.-P. Serre, Galois Cohomology, Chapter I, §5.

def TauCeti.ContCohomology.H1ConjInvariants (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] : AddSubgroup (H1 (↥N) M)

The subgroup of H¹(N, M) fixed by conjugation by G and the corresponding action on coefficients. Since elements of N act trivially, this is equivalently the invariant subgroup for the induced G ⧸ N-action.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.mem_H1ConjInvariants_iff (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] {x : H1 (↥N) M} : x ∈ H1ConjInvariants G M N ↔ ∀ (g : G), (explicitConj1 N g) x = x

A class belongs to H1ConjInvariants exactly when every conjugation map fixes it.

theorem TauCeti.ContCohomology.exists_smul_conj_sub_eq_d0_of_mem_H1ConjInvariants {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {N : Subgroup G} [N.Normal] {c : ↥(Z1 (↥N) M)} (hc : ↑c ∈ H1ConjInvariants G M N) (g : G) : ∃ (m : M), ∀ (n : ↥N), g • ↑c ((N.inverseConjugationHom g) n) - ↑c n = (d0 (↥N) M) m n

A conjugation-invariant class in H¹(N, M) is represented by cocycles whose conjugates are cohomologous to them: for each g, conjugating by g changes a representative by a coboundary.

theorem TauCeti.ContCohomology.smul_inverseConjugation_apply_sub_eq_d0 (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (N : Subgroup G) (c : ↥(Z1 G M)) (g : G) (n : ↥N) : g • ↑c (g⁻¹ * ↑n * g) - ↑c ↑n = (d0 (↥N) M) (↑c g) n

Conjugating the restriction of a continuous 1-cocycle changes it by the coboundary of its value at the conjugating element. This is the representative-level identity behind explicitRes1_mem_conjInvariants.

theorem TauCeti.ContCohomology.explicitRes1_mem_conjInvariants (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] (x : H1 G M) : (explicitRes1 G M N) x ∈ H1ConjInvariants G M N

Restriction of a first cohomology class to a normal subgroup is invariant under conjugation.

On a cocycle representative c, conjugation changes the restricted cocycle by the coboundary of c g.

noncomputable def TauCeti.ContCohomology.explicitResConj1 (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] : H1 G M →+ ↥(H1ConjInvariants G M N)

Restriction in degree one, with codomain restricted to the conjugation-invariant subgroup. This is the third arrow in the inflation-restriction-transgression five-term sequence.

Equations

• TauCeti.ContCohomology.explicitResConj1 G M N = (TauCeti.ContCohomology.explicitRes1 G M N).codRestrict (TauCeti.ContCohomology.H1ConjInvariants G M N) ⋯

@[simp]

theorem TauCeti.ContCohomology.coe_explicitResConj1 (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] (x : H1 G M) : ↑((explicitResConj1 G M N) x) = (explicitRes1 G M N) x

The invariant-valued restriction map has the usual restriction map as its underlying value.

theorem TauCeti.ContCohomology.explicitInfResConj_exact (G : Type uG) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] [ContinuousSMul (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)] : (explicitInfl1 G M N).range = (explicitResConj1 G M N).ker

The inflation-restriction sequence remains exact when restriction is given its natural conjugation-invariant codomain.