Conjugation on explicit first continuous cohomology

If N is a normal subgroup of a topological group G, 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 map is written with the 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 difference of a cocycle and its conjugate 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.inverseConjugationHom_smul {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] (g : G) (n : ↥N) (m : M) : (DistribSMul.toAddMonoidHom M g) ((N.inverseConjugationHom g) n • m) = n • (DistribSMul.toAddMonoidHom M g) m

The conjugation compatible-pair identity on coefficients.

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.

Equations

• TauCeti.ContCohomology.inverseConjugationHomotopy1 g c = c g

@[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.

Equations

• TauCeti.ContCohomology.inverseConjugationHomotopy2 g c n = c (g, g⁻¹ * n * g) - c (n, g)

@[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.inverseConjugationCochainHomotopy1 {K : Type uK} [Group K] {A : Type uA} [AddCommGroup A] [DistribMulAction 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] [DistribMulAction 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] [IsTopologicalGroup 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¹.

Equations

• TauCeti.ContCohomology.explicitConj1 N g = TauCeti.ContCohomology.explicitMap1 (↥N) M (↥N) M (N.inverseConjugationHom g) (DistribSMul.toAddMonoidHom M g) ⋯ ⋯

@[instance_reducible]

noncomputable instance TauCeti.ContCohomology.instSMulH1SubtypeMemSubgroupOfNormal {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] : SMul G (H1 (↥N) M)

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

Equations

• TauCeti.ContCohomology.instSMulH1SubtypeMemSubgroupOfNormal N = { smul := fun (g : G) => ⇑(TauCeti.ContCohomology.explicitConj1 N g) }

@[simp]

theorem TauCeti.ContCohomology.explicitConj1_apply_eq_smul {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] (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] [IsTopologicalGroup 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] [IsTopologicalGroup G] {M : Type uM} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul 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] [IsTopologicalGroup 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] [IsTopologicalGroup 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] [IsTopologicalGroup 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] [IsTopologicalGroup 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.

Equations

• TauCeti.ContCohomology.instMulActionH1SubtypeMemSubgroupOfNormal N = { toSMul := TauCeti.ContCohomology.instSMulH1SubtypeMemSubgroupOfNormal N, mul_smul := ⋯, one_smul := ⋯ }

theorem TauCeti.ContCohomology.explicitConj1_eq_id_of_mem {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] (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] [IsTopologicalGroup 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] [IsTopologicalGroup 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, -).