Factor sets up to cohomology are the second cohomology group

A factor set α : FactorSet G M is by definition a normalized multiplicative 2-cocycle, so it has a class in H²(G, M) = groupCohomology.H2 (Rep.ofMulDistribMulAction G M). This file builds that class and proves that it is a complete invariant of α modulo coboundaries: the map

FactorSet G M ⧸ (cohomologous) → H²(G, M)

is a bijection (TauCeti.FactorSet.cohomologyClassEquiv). Both halves need an argument. Two factor sets have the same class exactly when their quotient is a coboundary — the interesting direction here is that a coboundary witnessing this is automatically normalized, so no compatibility with the normalization of α and β has to be arranged. And every class is the class of a factor set: an arbitrary 2-cocycle need not be normalized, but dividing it by the coboundary of the constant function f (1, 1) normalizes it without moving its class (TauCeti.FactorSet.ofIsMulCocycle₂).

Read through the group extensions of TauCeti/GroupTheory/GroupExtension/Of/FactorSet.lean and TauCeti/GroupTheory/GroupExtension/FactorSetOfSection.lean, this says several things about extensions of G by an abelian kernel M inducing the given action: the class read off an extension does not depend on the normalized section it is read from (TauCeti.GroupExtension.cohomologyClass_factorSet_eq) and is unchanged by an equivalence of extensions, and two such extensions are equivalent exactly when their classes agree (TauCeti.GroupExtension.nonempty_equiv_iff_cohomologyClass_factorSet_eq), so the class is a complete invariant of the extension. The class vanishes exactly on the split extensions. Specializing the action to the trivial action of G on M = kˣ gives H²(G, kˣ), the group that classifies the factor sets of projective representations of G, equivalently the central extensions of G by kˣ up to equivalence.

Universes

Rep ℤ G puts the group and the module in the universe of ℤ, so the whole file is stated for G M : Type. This is the same restriction Mathlib's own multiplicative interface to groupCohomology.cocycles₂ carries; FactorSet G M itself is universe-polymorphic and stays so.

Main definitions

• TauCeti.FactorSet.toCocycles₂: a factor set read as a 2-cocycle valued in Additive M.
• TauCeti.FactorSet.cohomologyClass: its class in H²(G, M).
• TauCeti.FactorSet.IsCohomologous: two factor sets whose quotient is a multiplicative 2-coboundary, with TauCeti.FactorSet.isCohomologousSetoid the equivalence relation it cuts out, presented as the kernel of the cohomology class.
• TauCeti.FactorSet.ofIsMulCocycle₂: the normalization of an arbitrary multiplicative 2-cocycle.

Main results

• TauCeti.FactorSet.cohomologyClass_eq_iff: two factor sets have the same class exactly when they are cohomologous.
• TauCeti.FactorSet.exists_cohomologyClass_eq: every class in H²(G, M) is the class of a factor set.
• TauCeti.FactorSet.cohomologyClassEquiv: H²(G, M) classifies factor sets up to cohomology.
• TauCeti.FactorSet.cohomologyClass_eq_zero_iff and TauCeti.FactorSet.nonempty_splitting_iff_cohomologyClass_eq_zero: the class vanishes exactly for the coboundaries, equivalently for the factor sets whose extension splits.
• TauCeti.FactorSet.nsmul_cohomologyClass_eq_zero_iff: n kills a factor-set class exactly when the pointwise n-th power of the factor set is a multiplicative coboundary.
• TauCeti.FactorSet.exists_rescale_pow_eq_one: with a surjective n-th power map for nonzero n, a class killed by n admits a normalized rescaling by an action-aware coboundary whose values have n-th power one. For n = 0, no divisibility is needed.
• TauCeti.FactorSet.exists_cohomologyClass_eq_and_pow_eq_one: the rescaling produces a cohomologous factor-set representative with pointwise n-th power one under the same hypotheses, allowing torsion classes to be represented by root-valued factor sets.
• TauCeti.GroupExtension.cohomologyClass_factorSet_eq: the class of the factor set of a normalized section does not depend on the section.
• TauCeti.GroupExtension.nonempty_equiv_iff_cohomologyClass_factorSet_eq: H²(G, M) classifies group extensions of G by M inducing the given action, up to equivalence.

References

This is the second-cohomology target of Layer 7 of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md ("projective representations, factor sets, and the Schur multiplier"), which asks for groupCohomology.H2 of the module of scalars together with a proof that it classifies factor sets up to cohomology. See G. Karpilovsky, Projective Representations of Finite Groups, Marcel Dekker (1985), Ch. 1, and K. S. Brown, Cohomology of Groups, Springer GTM 87 (1982), Ch. IV.3.

The class of a factor set

theorem TauCeti.FactorSet.mem_cocycles₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : (fun (p : G × G) => Additive.ofMul (α p)) ∈ groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction G M)

A factor set is a 2-cocycle for the ℤ-linear representation of G on Additive M induced by the action.

def TauCeti.FactorSet.toCocycles₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : ↥(groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction G M))

A factor set, read as a 2-cocycle valued in Additive M.

Equations

• α.toCocycles₂ = ⟨fun (p : G × G) => Additive.ofMul (α p), ⋯⟩

@[simp]

theorem TauCeti.FactorSet.coe_toCocycles₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : ⇑α.toCocycles₂ = fun (p : G × G) => Additive.ofMul (α p)

noncomputable def TauCeti.FactorSet.cohomologyClass {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction G M))

The cohomology class of a factor set in H²(G, M). Rescaling the factor set by a coboundary does not move it (TauCeti.FactorSet.cohomologyClass_eq_iff), and every class arises this way (TauCeti.FactorSet.exists_cohomologyClass_eq).

Equations

• α.cohomologyClass = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction G M))) α.toCocycles₂

theorem TauCeti.FactorSet.cohomologyClass_def {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.cohomologyClass = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofMulDistribMulAction G M))) α.toCocycles₂

@[simp]

theorem TauCeti.FactorSet.cohomologyClass_trivial {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] : (trivial G M).cohomologyClass = 0

theorem TauCeti.FactorSet.coe_toCocycles₂_sub {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α β : FactorSet G M) : ⇑α.toCocycles₂ - ⇑β.toCocycles₂ = fun (p : G × G) => Additive.ofMul (α p / β p)

The pointwise quotient of two factor sets is the difference of the cocycles they name.

theorem TauCeti.FactorSet.cohomologyClass_eq_iff {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α β : FactorSet G M) : α.cohomologyClass = β.cohomologyClass ↔ groupCohomology.IsMulCoboundary₂ fun (p : G × G) => α p / β p

Two factor sets have the same cohomology class exactly when their quotient is a multiplicative 2-coboundary.

theorem TauCeti.FactorSet.cohomologyClass_eq_zero_iff {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.cohomologyClass = 0 ↔ groupCohomology.IsMulCoboundary₂ ⇑α

The class of a factor set vanishes exactly when it is a multiplicative 2-coboundary.

theorem TauCeti.FactorSet.nsmul_cohomologyClass_eq_zero_iff {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (n : ℕ) : n • α.cohomologyClass = 0 ↔ groupCohomology.IsMulCoboundary₂ fun (p : G × G) => α p ^ n

A natural number kills the class of a factor set exactly when its pointwise power is a multiplicative coboundary.

theorem TauCeti.FactorSet.exists_rescale_pow_eq_one {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) {n : ℕ} (hroot : n ≠ 0 → Function.Surjective fun (z : M) => z ^ n) (hα : n • α.cohomologyClass = 0) : ∃ (d : G → M), d 1 = 1 ∧ ∀ (g h : G), (d g * g • d h * (d (g * h))⁻¹ * α (g, h)) ^ n = 1

If n kills the class of a factor set and the coefficient group is n-divisible, a normalized rescaling by an action-aware coboundary makes every value have n-th power one. When n = 0, no divisibility hypothesis is needed.

theorem TauCeti.FactorSet.exists_cohomologyClass_eq_and_pow_eq_one {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) {n : ℕ} (hroot : n ≠ 0 → Function.Surjective fun (z : M) => z ^ n) (hα : n • α.cohomologyClass = 0) : ∃ (β : FactorSet G M), β.cohomologyClass = α.cohomologyClass ∧ ∀ (p : G × G), β p ^ n = 1

A factor set whose class is killed by n has a cohomologous representative with n-th power one whenever the coefficient power map is surjective for nonzero n. For n = 0, the original factor set is already such a representative.

Normalizing a cocycle

def TauCeti.FactorSet.ofIsMulCocycle₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : groupCohomology.IsMulCocycle₂ f) : FactorSet G M

Every multiplicative 2-cocycle is normalized by a coboundary. Dividing f by the function p ↦ p.1 • f (1, 1) — the coboundary of the function constant at f (1, 1) — leaves a factor set: the cocycle identity survives because the divisor is itself a cocycle, and the value at (1, 1) becomes 1.

Equations

• TauCeti.FactorSet.ofIsMulCocycle₂ hf = { toFun := fun (p : G × G) => f p / p.1 • f (1, 1), isMulCocycle₂' := ⋯, map_one_one' := ⋯ }

@[simp]

theorem TauCeti.FactorSet.coe_ofIsMulCocycle₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : groupCohomology.IsMulCocycle₂ f) : ⇑(ofIsMulCocycle₂ hf) = fun (p : G × G) => f p / p.1 • f (1, 1)

theorem TauCeti.FactorSet.isMulCoboundary₂_div_ofIsMulCocycle₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : groupCohomology.IsMulCocycle₂ f) : groupCohomology.IsMulCoboundary₂ fun (p : G × G) => (ofIsMulCocycle₂ hf) p / f p

The normalization of a cocycle is cohomologous to it, in the pointwise sense that their quotient is a coboundary.

The classification

theorem TauCeti.FactorSet.exists_cohomologyClass_eq {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (x : ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction G M))) : ∃ (α : FactorSet G M), α.cohomologyClass = x

Every class in H²(G, M) is the class of a factor set.

def TauCeti.FactorSet.IsCohomologous {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α β : FactorSet G M) : Prop

Cohomologous factor sets: their pointwise quotient is a multiplicative 2-coboundary, equivalently (TauCeti.FactorSet.cohomologyClass_eq_iff) they have the same class in H²(G, M). This is the relation under which the factor sets of a projective representation, or of a group extension with abelian kernel, are well defined.

Equations

• α.IsCohomologous β = groupCohomology.IsMulCoboundary₂ fun (p : G × G) => α p / β p

@[simp]

theorem TauCeti.FactorSet.isCohomologous_iff_cohomologyClass_eq {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {α β : FactorSet G M} : α.IsCohomologous β ↔ α.cohomologyClass = β.cohomologyClass

noncomputable def TauCeti.FactorSet.isCohomologousSetoid (G M : Type) [Group G] [CommGroup M] [MulDistribMulAction G M] : Setoid (FactorSet G M)

Being cohomologous is an equivalence relation on factor sets: by TauCeti.FactorSet.isCohomologous_iff_cohomologyClass_eq it is the kernel of the cohomology class.

Equations

• TauCeti.FactorSet.isCohomologousSetoid G M = Setoid.ker TauCeti.FactorSet.cohomologyClass

@[simp]

theorem TauCeti.FactorSet.isCohomologousSetoid_apply {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {α β : FactorSet G M} : (isCohomologousSetoid G M) α β ↔ α.IsCohomologous β

The relation of TauCeti.FactorSet.isCohomologousSetoid is being cohomologous, so a coboundary witness gives Quotient.sound.

noncomputable def TauCeti.FactorSet.cohomologyClassEquiv (G M : Type) [Group G] [CommGroup M] [MulDistribMulAction G M] : Quotient (isCohomologousSetoid G M) ≃ ↑(groupCohomology.H2 (Rep.ofMulDistribMulAction G M))

H²(G, M) classifies factor sets up to cohomology. The cohomology class descends to a bijection from the factor sets of G with values in M, taken modulo the cohomologous relation, onto the second cohomology group.

Equations

• TauCeti.FactorSet.cohomologyClassEquiv G M = Setoid.quotientKerEquivOfSurjective TauCeti.FactorSet.cohomologyClass ⋯

@[simp]

theorem TauCeti.FactorSet.cohomologyClassEquiv_apply_mk {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : (cohomologyClassEquiv G M) ⟦α⟧ = α.cohomologyClass

Reading the classification on extensions

theorem TauCeti.FactorSet.nonempty_splitting_iff_cohomologyClass_eq_zero {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} : Nonempty α.groupExtension.Splitting ↔ α.cohomologyClass = 0

The class of a factor set vanishes exactly when its extension splits. A splitting is a section that is a homomorphism, so its M-components form (the inverse of) a function whose coboundary is α; conversely a function with that coboundary is exactly what makes g ↦ ⟨_, g⟩ a homomorphism.

theorem TauCeti.GroupExtension.cohomologyClass_factorSet_eq {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {E : Type u_1} [Group E] {S : GroupExtension M E G} (σ σ' : S.Section) (hσ : σ 1 = 1) (hσ' : σ' 1 = 1) (hact : InducesAction S) : (factorSet σ hσ hact).cohomologyClass = (factorSet σ' hσ' hact).cohomologyClass

The cohomology class of the factor set of an extension does not depend on the section. So the class in H²(G, M) is an invariant of the extension, and by TauCeti.GroupExtension.factorSetToGroupExtensionEquiv the extension is recovered from any one of these factor sets.

theorem TauCeti.GroupExtension.nonempty_equiv_iff_cohomologyClass_factorSet_eq {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {E : Type u_1} {E' : Type u_2} [Group E] [Group E'] {S : GroupExtension M E G} {S' : GroupExtension M E' G} (σ : S.Section) (σ' : S'.Section) (hσ : σ 1 = 1) (hσ' : σ' 1 = 1) (hact : InducesAction S) (hact' : InducesAction S') : Nonempty (S.Equiv S') ↔ (factorSet σ hσ hact).cohomologyClass = (factorSet σ' hσ' hact').cohomologyClass

H²(G, M) classifies group extensions up to equivalence. Two extensions of G by the abelian kernel M, both inducing the ambient action, are equivalent exactly when the factor sets of normalized sections of them have the same class.

The forward direction is the invariance of the class under an equivalence e: the transported section e ∘ σ is a normalized section of S' with literally the same factor set as σ, and by TauCeti.GroupExtension.cohomologyClass_factorSet_eq the class of S' does not see which of its sections it is read from. The backward direction is TauCeti.FactorSet.nonempty_groupExtensionEquiv, carried across the two identifications TauCeti.GroupExtension.factorSetToGroupExtensionEquiv.