Continuous nonabelian first cohomology

Let a group G with a topology act on a group A with a topology by group automorphisms (MulDistribMulAction G A); A need not be commutative. A continuous 1-cocycle is a continuous map f : G → A with

f (g * h) = f g * g • f h,

and two cocycles f, f' are cohomologous when f' g = a⁻¹ * f g * g • a for one a : A and all g. The quotient is the pointed set H¹(G, A), whose base point is the class of the trivial cocycle. For a commutative A the cocycles and the relation are the classical ones of abelian first cohomology, written multiplicatively; for a general A the quotient carries no group structure, and only its base point is distinguished.

This is the cohomology that classifies forms and twists: for a Galois extension with group G and an object whose automorphism group is A, the twists of the object are classified by H¹(G, A) (Serre, Galois Cohomology, III.1). For the twists of an elliptic curve, G is an absolute Galois group and A the automorphism group of the curve over a separable closure, with the discrete topology.

The functoriality is that of compatible pairs: a continuous homomorphism ψ : G' →ₜ* G and a continuous homomorphism φ : A →ₜ* A' with φ (ψ g • a) = g • φ a send cocycles to cocycles by f ↦ φ ∘ f ∘ ψ, preserving cohomology. Taking ψ to be the inclusion of a subgroup gives restriction. Inflation, the other named instance, is in TauCeti/RepresentationTheory/Homological/ContCohomology/Nonabelian/Inflation.lean.

Main definitions

• TauCeti.NonabelianH1.Cocycle G A: the continuous 1-cocycles of G with values in A.
• TauCeti.NonabelianH1.Cocycle.setoid: the cohomology relation on cocycles.
• TauCeti.NonabelianH1.Cocycle.twist: the twist g ↦ a⁻¹ * f g * g • a of a cocycle by a : A; two cocycles are cohomologous exactly when one is a twist of the other (TauCeti.NonabelianH1.Cocycle.equiv_iff_exists_twist_eq).
• TauCeti.NonabelianH1 G A: the pointed set H¹(G, A) of cohomology classes, with TauCeti.NonabelianH1.mk the class of a cocycle.
• TauCeti.NonabelianH1.Cocycle.map and TauCeti.NonabelianH1.map: the maps of cocycles and of classes induced by a compatible pair.
• TauCeti.NonabelianH1.res: restriction to a subgroup.

Main results

• TauCeti.NonabelianH1.mk_eq_mk_iff: two cocycles have the same class exactly when they are cohomologous.
• TauCeti.NonabelianH1.mk_eq_one_iff: the class of a cocycle is the base point exactly when the cocycle is a coboundary g ↦ a⁻¹ * g • a.
• TauCeti.NonabelianH1.map_one, TauCeti.NonabelianH1.map_id and TauCeti.NonabelianH1.map_map: the induced maps are maps of pointed sets, and the construction is functorial.

References

• J.-P. Serre, Galois Cohomology, Springer, 1997, I.5 and III.1.

structure TauCeti.NonabelianH1.Cocycle (G : Type u_1) (A : Type u_2) [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : Type (max u_1 u_2)

A continuous 1-cocycle of G with values in the G-group A: a continuous map f : G → A with f (g * h) = f g * g • f h.

• toFun : G → A

  The underlying function of a cocycle.

• continuous_toFun : Continuous self.toFun

  A cocycle is continuous.

• map_mul' (g h : G) : self.toFun (g * h) = self.toFun g * g • self.toFun h

  The cocycle identity f (g * h) = f g * g • f h.

@[instance_reducible]

instance TauCeti.NonabelianH1.Cocycle.instFunLike {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : FunLike (Cocycle G A) G A

theorem TauCeti.NonabelianH1.Cocycle.ext {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {f f' : Cocycle G A} (h : ∀ (g : G), f g = f' g) : f = f'

theorem TauCeti.NonabelianH1.Cocycle.ext_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {f f' : Cocycle G A} : f = f' ↔ ∀ (g : G), f g = f' g

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.coe_mk {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (f : G → A) (hf : Continuous f) (hmul : ∀ (g h : G), f (g * h) = f g * g • f h) : ⇑{ toFun := f, continuous_toFun := hf, map_mul' := hmul } = f

theorem TauCeti.NonabelianH1.Cocycle.continuous {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (f : Cocycle G A) : Continuous ⇑f

A cocycle is continuous.

theorem TauCeti.NonabelianH1.Cocycle.apply_mul {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (f : Cocycle G A) (g h : G) : f (g * h) = f g * g • f h

The cocycle identity.

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.apply_one {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (f : Cocycle G A) : f 1 = 1

A cocycle takes the value 1 at 1.

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.apply_inv {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (f : Cocycle G A) (g : G) : f g⁻¹ = g⁻¹ • (f g)⁻¹

The value of a cocycle at an inverse.

@[instance_reducible]

instance TauCeti.NonabelianH1.Cocycle.instOne {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : One (Cocycle G A)

The trivial cocycle g ↦ 1.

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.one_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (g : G) : 1 g = 1

@[instance_reducible]

instance TauCeti.NonabelianH1.Cocycle.instInhabited {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : Inhabited (Cocycle G A)

@[instance_reducible]

instance TauCeti.NonabelianH1.Cocycle.setoid {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : Setoid (Cocycle G A)

The cohomology relation on cocycles: f ≈ f' when f' g = a⁻¹ * f g * g • a for one a : A and all g : G.

theorem TauCeti.NonabelianH1.Cocycle.equiv_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {f f' : Cocycle G A} : f ≈ f' ↔ ∃ (a : A), ∀ (g : G), f' g = a⁻¹ * f g * g • a

def TauCeti.NonabelianH1.Cocycle.twist {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] [ContinuousMul A] [ContinuousSMul G A] (f : Cocycle G A) (a : A) : Cocycle G A

The twist g ↦ a⁻¹ * f g * g • a of a cocycle f by a : A, the action of A on cocycles whose orbits are the cohomology classes.

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.twist_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] [ContinuousMul A] [ContinuousSMul G A] (f : Cocycle G A) (a : A) (g : G) : (f.twist a) g = a⁻¹ * f g * g • a

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.twist_one {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] [ContinuousMul A] [ContinuousSMul G A] (f : Cocycle G A) : f.twist 1 = f

theorem TauCeti.NonabelianH1.Cocycle.twist_twist {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] [ContinuousMul A] [ContinuousSMul G A] (f : Cocycle G A) (a b : A) : (f.twist a).twist b = f.twist (a * b)

theorem TauCeti.NonabelianH1.Cocycle.equiv_iff_exists_twist_eq {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] [ContinuousMul A] [ContinuousSMul G A] {f f' : Cocycle G A} : f ≈ f' ↔ ∃ (a : A), f.twist a = f'

Two cocycles are cohomologous exactly when one is a twist of the other.

theorem TauCeti.NonabelianH1.Cocycle.equiv_twist {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] [ContinuousMul A] [ContinuousSMul G A] (f : Cocycle G A) (a : A) : f ≈ f.twist a

def TauCeti.NonabelianH1 (G : Type u_1) (A : Type u_2) [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : Type (max u_1 u_2)

The continuous nonabelian first cohomology H¹(G, A): continuous 1-cocycles of G with values in A, up to the cohomology relation. It is a pointed set, with base point the class of the trivial cocycle.

def TauCeti.NonabelianH1.mk {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (f : Cocycle G A) : NonabelianH1 G A

The cohomology class of a cocycle.

theorem TauCeti.NonabelianH1.mk_surjective {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : Function.Surjective mk

theorem TauCeti.NonabelianH1.induction_on {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {motive : NonabelianH1 G A → Prop} (c : NonabelianH1 G A) (mk : ∀ (f : Cocycle G A), motive (mk f)) : motive c

theorem TauCeti.NonabelianH1.mk_eq_mk_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {f f' : Cocycle G A} : mk f = mk f' ↔ ∃ (a : A), ∀ (g : G), f' g = a⁻¹ * f g * g • a

Two cocycles have the same class exactly when they are cohomologous.

@[instance_reducible]

instance TauCeti.NonabelianH1.instOne {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : One (NonabelianH1 G A)

The base point of H¹(G, A), the class of the trivial cocycle.

@[instance_reducible]

instance TauCeti.NonabelianH1.instInhabited {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : Inhabited (NonabelianH1 G A)

theorem TauCeti.NonabelianH1.one_def {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : 1 = mk 1

@[simp]

theorem TauCeti.NonabelianH1.mk_one {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : mk 1 = 1

theorem TauCeti.NonabelianH1.mk_eq_one_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {f : Cocycle G A} : mk f = 1 ↔ ∃ (a : A), ∀ (g : G), f g = a⁻¹ * g • a

The class of a cocycle is the base point exactly when the cocycle is a coboundary g ↦ a⁻¹ * g • a.

@[simp]

theorem TauCeti.NonabelianH1.mk_twist {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] [ContinuousMul A] [ContinuousSMul G A] (f : Cocycle G A) (a : A) : mk (f.twist a) = mk f

A twisted cocycle has the same class.

def TauCeti.NonabelianH1.Cocycle.map {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {G' : Type u_3} {A' : Type u_4} [Group G'] [TopologicalSpace G'] [Group A'] [TopologicalSpace A'] [MulDistribMulAction G' A'] (ψ : G' →ₜ* G) (φ : A →ₜ* A') (h : ∀ (g : G') (a : A), φ (ψ g • a) = g • φ a) (f : Cocycle G A) : Cocycle G' A'

The cocycle φ ∘ f ∘ ψ induced by a compatible pair (ψ, φ): continuous homomorphisms ψ : G' →ₜ* G and φ : A →ₜ* A' with φ (ψ g • a) = g • φ a.

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.map_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {G' : Type u_3} {A' : Type u_4} [Group G'] [TopologicalSpace G'] [Group A'] [TopologicalSpace A'] [MulDistribMulAction G' A'] (ψ : G' →ₜ* G) (φ : A →ₜ* A') (h : ∀ (g : G') (a : A), φ (ψ g • a) = g • φ a) (f : Cocycle G A) (g : G') : (map ψ φ h f) g = φ (f (ψ g))

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.map_one {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {G' : Type u_3} {A' : Type u_4} [Group G'] [TopologicalSpace G'] [Group A'] [TopologicalSpace A'] [MulDistribMulAction G' A'] (ψ : G' →ₜ* G) (φ : A →ₜ* A') (h : ∀ (g : G') (a : A), φ (ψ g • a) = g • φ a) : map ψ φ h 1 = 1

A compatible pair sends the trivial cocycle to the trivial cocycle.

@[simp]

theorem TauCeti.NonabelianH1.Cocycle.map_id {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (f : Cocycle G A) : map (ContinuousMonoidHom.id G) (ContinuousMonoidHom.id A) ⋯ f = f

The identity pair preserves every cocycle.

theorem TauCeti.NonabelianH1.Cocycle.map_map {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {G' : Type u_3} {A' : Type u_4} [Group G'] [TopologicalSpace G'] [Group A'] [TopologicalSpace A'] [MulDistribMulAction G' A'] {G'' : Type u_5} {A'' : Type u_6} [Group G''] [TopologicalSpace G''] [Group A''] [TopologicalSpace A''] [MulDistribMulAction G'' A''] (f : Cocycle G A) (ψ : G' →ₜ* G) (φ : A →ₜ* A') (h : ∀ (g : G') (a : A), φ (ψ g • a) = g • φ a) (ψ' : G'' →ₜ* G') (φ' : A' →ₜ* A'') (h' : ∀ (g : G'') (a : A'), φ' (ψ' g • a) = g • φ' a) : map ψ' φ' h' (map ψ φ h f) = map (ψ.comp ψ') (φ'.comp φ) ⋯ f

Mapping a cocycle twice agrees with mapping along the composite compatible pair.

def TauCeti.NonabelianH1.map {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {G' : Type u_3} {A' : Type u_4} [Group G'] [TopologicalSpace G'] [Group A'] [TopologicalSpace A'] [MulDistribMulAction G' A'] (ψ : G' →ₜ* G) (φ : A →ₜ* A') (h : ∀ (g : G') (a : A), φ (ψ g • a) = g • φ a) : NonabelianH1 G A → NonabelianH1 G' A'

The map H¹(G, A) → H¹(G', A') induced by a compatible pair (ψ, φ).

@[simp]

theorem TauCeti.NonabelianH1.map_mk {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {G' : Type u_3} {A' : Type u_4} [Group G'] [TopologicalSpace G'] [Group A'] [TopologicalSpace A'] [MulDistribMulAction G' A'] (ψ : G' →ₜ* G) (φ : A →ₜ* A') (h : ∀ (g : G') (a : A), φ (ψ g • a) = g • φ a) (f : Cocycle G A) : map ψ φ h (mk f) = mk (Cocycle.map ψ φ h f)

@[simp]

theorem TauCeti.NonabelianH1.map_one {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {G' : Type u_3} {A' : Type u_4} [Group G'] [TopologicalSpace G'] [Group A'] [TopologicalSpace A'] [MulDistribMulAction G' A'] (ψ : G' →ₜ* G) (φ : A →ₜ* A') (h : ∀ (g : G') (a : A), φ (ψ g • a) = g • φ a) : map ψ φ h 1 = 1

The map induced by a compatible pair preserves the base point.

@[simp]

theorem TauCeti.NonabelianH1.map_id {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] : map (ContinuousMonoidHom.id G) (ContinuousMonoidHom.id A) ⋯ = id

The identity pair induces the identity.

theorem TauCeti.NonabelianH1.map_map {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {G' : Type u_3} {A' : Type u_4} [Group G'] [TopologicalSpace G'] [Group A'] [TopologicalSpace A'] [MulDistribMulAction G' A'] {G'' : Type u_5} {A'' : Type u_6} [Group G''] [TopologicalSpace G''] [Group A''] [TopologicalSpace A''] [MulDistribMulAction G'' A''] (ψ : G' →ₜ* G) (φ : A →ₜ* A') (h : ∀ (g : G') (a : A), φ (ψ g • a) = g • φ a) (ψ' : G'' →ₜ* G') (φ' : A' →ₜ* A'') (h' : ∀ (g : G'') (a : A'), φ' (ψ' g • a) = g • φ' a) (c : NonabelianH1 G A) : map ψ' φ' h' (map ψ φ h c) = map (ψ.comp ψ') (φ'.comp φ) ⋯ c

The maps induced by compatible pairs compose.

def TauCeti.NonabelianH1.res {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (S : Subgroup G) : NonabelianH1 G A → NonabelianH1 (↥S) A

Restriction H¹(G, A) → H¹(S, A) to a subgroup S, carrying the subspace topology: the map induced by the inclusion of S and the identity of A.

theorem TauCeti.NonabelianH1.res_mk {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (S : Subgroup G) (f : Cocycle G A) : res S (mk f) = mk (Cocycle.map (ContinuousMonoidHom.subgroupSubtype S) (ContinuousMonoidHom.id A) ⋯ f)

Restriction restricts a representing cocycle.

@[simp]

theorem TauCeti.NonabelianH1.res_one {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (S : Subgroup G) : res S 1 = 1

Restriction preserves the base point.