Conjugation on explicit first continuous cohomology

If N is a normal subgroup of a group G with separately continuous multiplication, conjugation by g on N, together with the action of g on coefficients, is a compatible pair. This file packages the resulting map on the explicit quotient H¹(N, M). The theorem explicitMap1_eq_of_conj identifies the maps on H¹ of compatible pairs differing by conjugation and the corresponding coefficient action. The subgroup map uses inverse conjugation h ↦ g⁻¹ h g, so that its coefficient component is the left action m ↦ g • m.

The construction is functorial in g, hence gives the expected G-action. When g belongs to N, the induced map is the identity: the conjugate of a cocycle minus the original is the principal cocycle attached to c g. The file records the algebraic degree-one and degree-two components of the corresponding bar homotopy and specializes their identities to continuous cocycles, including the degree-two cocycle identity that expresses the conjugation difference as a coboundary.

A continuous N-equivariant coefficient map f with f (g • m) = k • g • f m intertwines the two conjugation actions of g up to the same factor k (explicitCoeff1_smul_of_map_smul). This is how a cyclotomic twist of the coefficients appears in the Galois action on H¹.

theorem TauCeti.ContCohomology.explicitMap1_eq_of_conj (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (H : Type uH) [Monoid H] [TopologicalSpace H] (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ ψ : H →ₜ* G) (f q : M →+ N) (hf : Continuous ⇑f) (hφ : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (g : G) (hconj : ∀ (h : H), ψ h = g⁻¹ * φ h * g) (hqf : ∀ (m : M), q m = f (g • m)) : explicitMap1 G M H N ψ q ⋯ ⋯ = explicitMap1 G M H N φ f hf hφ

Conjugating the group map of a compatible pair and composing its coefficient map with the same group element's action leaves the map on explicit H¹ unchanged. This is the compatible-pair form of the conjugation invariance in Neukirch, Schmidt and Wingberg, Cohomology of Number Fields, Chapter I, §5.

def TauCeti.ContCohomology.inverseConjugationHomotopy1 {K : Type uK} {A : Type uA} (g : K) (c : K → A) : A

The degree-one component of the bar homotopy for inverse conjugation.

@[simp]

theorem TauCeti.ContCohomology.inverseConjugationHomotopy1_apply {K : Type uK} {A : Type uA} (g : K) (c : K → A) : inverseConjugationHomotopy1 g c = c g

The defining formula for the degree-one inverse-conjugation homotopy component.

def TauCeti.ContCohomology.inverseConjugationHomotopy2 {K : Type uK} [Group K] {A : Type uA} [Sub A] (g : K) (c : K × K → A) : K → A

The degree-two component of the bar homotopy for inverse conjugation.

@[simp]

theorem TauCeti.ContCohomology.inverseConjugationHomotopy2_apply {K : Type uK} [Group K] {A : Type uA} [Sub A] (g : K) (c : K × K → A) (n : K) : inverseConjugationHomotopy2 g c n = c (g, g⁻¹ * n * g) - c (n, g)

The defining formula for the degree-two inverse-conjugation homotopy component.

theorem TauCeti.ContCohomology.continuous_inverseConjugationHomotopy2 {K : Type uK} [Group K] [TopologicalSpace K] [SeparatelyContinuousMul K] {A : Type uA} [Sub A] [TopologicalSpace A] [ContinuousSub A] (g : K) {c : K × K → A} (hc : Continuous c) : Continuous (inverseConjugationHomotopy2 g c)

The degree-two inverse-conjugation homotopy preserves continuity.

theorem TauCeti.ContCohomology.inverseConjugationCochainHomotopy1 {K : Type uK} [Group K] {A : Type uA} [AddCommGroup A] [DistribSMul K A] (g : K) (c : K → A) : (cochainsMap1 (↑(MulAut.conj g⁻¹)) (DistribSMul.toAddMonoidHom A g)) c - c = (d0 K A) (inverseConjugationHomotopy1 g c) + inverseConjugationHomotopy2 g ((d1 K A) c)

The degree-one algebraic cochain-homotopy identity for inverse conjugation.

theorem TauCeti.ContCohomology.inverseConjugationCochainHomotopy2_of_isCocycle {K : Type uK} [Group K] {A : Type uA} [AddCommGroup A] [DistribSMul K A] (g : K) (c : K × K → A) (hc : groupCohomology.IsCocycle₂ c) : (cochainsMap2 (↑(MulAut.conj g⁻¹)) (DistribSMul.toAddMonoidHom A g)) c - c = (d1 K A) (inverseConjugationHomotopy2 g c)

The degree-two component of the bar homotopy for an algebraic inverse conjugation, for a degree-two cocycle.

noncomputable def TauCeti.ContCohomology.explicitConj1 {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] (g : G) : H1 (↥N) M →+ H1 (↥N) M

Conjugation by g, with the coefficient action of g, on explicit H¹.

@[instance_reducible]

noncomputable instance TauCeti.ContCohomology.instSMulH1SubtypeMemSubgroupOfNormal {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] : SMul G (H1 (↥N) M)

The conjugation/coefficient action on explicit first cohomology, defined by explicitConj1.

@[simp]

theorem TauCeti.ContCohomology.explicitConj1_apply_eq_smul {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] (g : G) (x : H1 (↥N) M) : (explicitConj1 N g) x = g • x

The installed scalar action is the map explicitConj1.

@[simp]

theorem TauCeti.ContCohomology.smul_mk {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] (g : G) (c : ↥(Z1 (↥N) M)) : g • ↑c = ↑((cocyclesMap1 (↥N) M (↥N) M (N.inverseConjugationHom g) (DistribSMul.toAddMonoidHom M g) ⋯ ⋯) c)

The representative formula for explicitConj1.

theorem TauCeti.ContCohomology.inverseConjugationHomotopy1_spec {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousConstSMul G M] (N : Subgroup G) [N.Normal] (g : ↥N) (c : ↥(Z1 (↥N) M)) : (d0 (↥N) M) (inverseConjugationHomotopy1 g ↑c) = ↑((cocyclesMap1 (↥N) M (↥N) M (N.inverseConjugationHom ↑g) (DistribSMul.toAddMonoidHom M ↑g) ⋯ ⋯) c) - ↑c

The degree-one bar-homotopy identity for inverse conjugation on continuous cocycles.

theorem TauCeti.ContCohomology.inverseConjugationHomotopy2_spec {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] (g : ↥N) (c : ↥(Z2 (↥N) M)) : (cochainsMap2 (↑(N.inverseConjugationHom ↑g)) (DistribSMul.toAddMonoidHom M ↑g)) ↑c - ↑c = (d1 (↥N) M) (inverseConjugationHomotopy2 g ↑c)

The degree-two bar-homotopy identity for inverse conjugation on continuous cocycles.

@[simp]

theorem TauCeti.ContCohomology.explicitConj1_one {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] : explicitConj1 N 1 = AddMonoidHom.id (H1 (↥N) M)

Conjugation by the identity gives the identity map on explicit H¹.

@[simp]

theorem TauCeti.ContCohomology.explicitConj1_mul {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] (g h : G) : explicitConj1 N (g * h) = (explicitConj1 N g).comp (explicitConj1 N h)

Successive conjugations compose in the order dictated by the left G-action.

@[instance_reducible]

noncomputable instance TauCeti.ContCohomology.instMulActionH1SubtypeMemSubgroupOfNormal {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] : MulAction G (H1 (↥N) M)

The conjugation/coefficient action on explicit first cohomology satisfies the group action laws.

theorem TauCeti.ContCohomology.explicitConj1_eq_id_of_mem {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] (g : ↥N) : explicitConj1 N ↑g = AddMonoidHom.id (H1 (↥N) M)

An element of the subgroup acts trivially on its explicit first cohomology.

This is the inner-automorphism triviality of Milne, Arithmetic Duality Theorems, Proposition 0.15.

@[simp]

theorem TauCeti.ContCohomology.smul_eq_self_of_mem {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (N : Subgroup G) [N.Normal] (g : ↥N) (x : H1 (↥N) M) : ↑g • x = x

An element of the subgroup acts trivially on explicit first cohomology.

theorem TauCeti.ContCohomology.explicitCoeff1_smul_of_map_smul {G : Type uG} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] {M' : Type uA} [AddCommGroup M'] [TopologicalSpace M'] [IsTopologicalAddGroup M'] [DistribMulAction G M'] [ContinuousSMul G M'] (N : Subgroup G) [N.Normal] (f : M →+[↥N] M') (hf : Continuous ⇑f) (g : G) (k : ℕ) (hg : ∀ (m : M), f (g • m) = k • g • f m) (x : H1 (↥N) M) : (explicitCoeff1 (↥N) M f hf) (g • x) = k • g • (explicitCoeff1 (↥N) M f hf) x

Coefficient maps intertwine conjugation up to a twist. If a continuous N-equivariant coefficient map f : M → M' satisfies f (g • m) = k • g • f m, then the map it induces on H¹(N, -) satisfies the same relation with the conjugation action of g. For k = 1 this says that a G-equivariant coefficient map induces a G-equivariant map on H¹(N, -).