The factor set of a group extension with abelian kernel

TauCeti.FactorSet.groupExtension builds a group extension 1 → M → E_α → G → 1 out of a factor set α. This file runs the construction backwards: an extension S : GroupExtension M E G with abelian kernel, together with a set-theoretic section σ of its projection normalized by σ 1 = 1, determines a factor set, and S is equivalent to the extension that factor set builds. So every extension with abelian kernel is one of the twisted products, and — with TauCeti.FactorSet.nonempty_groupExtensionEquiv for the converse direction — the classification of such extensions is the classification of factor sets modulo coboundaries.

Two ingredients make the correspondence precise.

The action of G on M must be the one the extension itself provides. Conjugation in E moves the copy of M, and because M is abelian this conjugation is trivial on the copy of M (TauCeti.GroupExtension.conjAct_inl), hence depends only on the image in G (TauCeti.GroupExtension.conjAct_eq_of_rightHom_eq); packaged as a homomorphism it is TauCeti.GroupExtension.conjActOfSection, independent of the section used to write it down. TauCeti.GroupExtension.InducesAction S says that this conjugation is the ambient MulDistribMulAction of G on M, equivalently that conjActOfSection is that action (TauCeti.GroupExtension.inducesAction_iff_conjActOfSection_eq). For a central extension the conjugation is trivial (TauCeti.GroupExtension.conjAct_eq_one_of_le_center), so there InducesAction holds exactly for the trivial action (TauCeti.GroupExtension.inducesAction_iff_smul_eq_self), the case in which a projective representation of G becomes a linear representation of E.

The factor set itself measures the failure of the section to be a homomorphism: σ g * σ h * (σ (g * h))⁻¹ lies in the copy of M, and TauCeti.GroupExtension.factorSetFun is its preimage. Changing the section changes the factor set by a coboundary (TauCeti.GroupExtension.isMulCoboundary₂_div), so the class in H²(G, M) is an invariant of the extension.

Only the descent of the conjugation action and the factor set itself need M abelian; the section bookkeeping (TauCeti.GroupExtension.factorSetFun, TauCeti.GroupExtension.normalizeSection, TauCeti.GroupExtension.sectionDiff) is stated for an arbitrary kernel.

Main definitions

• TauCeti.GroupExtension.conjActOfSection: the action of G on an abelian kernel by conjugation.
• TauCeti.GroupExtension.InducesAction: the extension conjugates the kernel by the given action.
• TauCeti.GroupExtension.factorSet: the factor set of a normalized section.
• TauCeti.GroupExtension.normalizeSection: any section, corrected to send 1 to 1.

Main results

• TauCeti.GroupExtension.inducesAction_iff_conjActOfSection_eq and TauCeti.GroupExtension.inducesAction_iff_smul_eq_self: InducesAction holds exactly when the descended conjugation action is the ambient one, and, for a central extension, exactly when the ambient action is trivial.
• TauCeti.GroupExtension.factorSet_monoidHomComp: the factor set of a section transported along a homomorphism of extensions over G restricting to f on the kernels is the pushforward along f of the factor set of the section.
• TauCeti.GroupExtension.section_mul: σ g * σ h = inl (α (g, h)) * σ (g * h), the defining property of the factor set.
• TauCeti.GroupExtension.factorSetToGroupExtensionEquiv: the extension is equivalent to the twisted product built from its factor set, and TauCeti.GroupExtension.exists_factorSet is the resulting existence statement for an arbitrary extension with abelian kernel.
• TauCeti.GroupExtension.factorSet_canonicalSection: reading the factor set off the twisted product built from α, using its canonical section, returns α.
• TauCeti.GroupExtension.isMulCoboundary₂_div: two normalized sections give factor sets that differ by a multiplicative 2-coboundary.

References

This continues the central-extension target of Layer 7 of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md ("projective representations, factor sets, and the Schur multiplier"), which asks that H²(G, k^×) classify central extensions up to equivalence. See G. Karpilovsky, Projective Representations of Finite Groups, Marcel Dekker (1985), Ch. 1, and I. M. Isaacs, Character Theory of Finite Groups, AMS Chelsea (1976), Ch. 11.

theorem TauCeti.GroupExtension.conjAct_eq_one_of_le_center {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (h : S.inl.range ≤ Subgroup.center E) (e : E) : S.conjAct e = 1

A central extension acts trivially on its kernel.

def TauCeti.GroupExtension.InducesAction {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] (S : GroupExtension M E G) [MulDistribMulAction G M] : Prop

The extension S conjugates its kernel by the ambient action of G on M. This is the compatibility that makes TauCeti.GroupExtension.factorSet a TauCeti.FactorSet for that action; for a central extension it says the ambient action is trivial.

Equations

• TauCeti.GroupExtension.InducesAction S = ∀ (e : E) (m : M), (S.conjAct e) m = S.rightHom e • m

theorem TauCeti.GroupExtension.inducesAction_iff_smul_eq_self {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} [MulDistribMulAction G M] (h : S.inl.range ≤ Subgroup.center E) : InducesAction S ↔ ∀ (g : G) (m : M), g • m = m

A central extension induces exactly the trivial action. This is the constructor for TauCeti.GroupExtension.InducesAction in the central case: the hypothesis holds if and only if the ambient action of G on M is trivial.

theorem TauCeti.GroupExtension.inl_smul {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hact : InducesAction S) (g : G) (m : M) : S.inl (g • m) = σ g * S.inl m * (σ g)⁻¹

The image of the kernel is conjugated by a section according to the ambient action.

theorem TauCeti.GroupExtension.conjAct_inl {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} (m : M) : S.conjAct (S.inl m) = 1

Conjugating an abelian kernel by an element of the kernel does nothing.

theorem TauCeti.GroupExtension.conjAct_eq_of_rightHom_eq {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} {e e' : E} (h : S.rightHom e = S.rightHom e') : S.conjAct e = S.conjAct e'

Conjugation of an abelian kernel depends only on the image of the conjugating element in the quotient.

noncomputable def TauCeti.GroupExtension.conjActOfSection {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} (σ : S.Section) : G →* MulAut M

The action of G on an abelian kernel. Conjugation in E descends along the projection to G because it is trivial on the kernel, so any section presents it as a homomorphism G →* MulAut M; TauCeti.GroupExtension.conjActOfSection_eq says the presentation does not depend on the section. Mathlib's GroupExtension.Splitting.conjAct is the special case of a section that is a homomorphism, which exists only for a split extension.

Equations

• TauCeti.GroupExtension.conjActOfSection σ = { toFun := fun (g : G) => S.conjAct (σ g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GroupExtension.conjActOfSection_apply {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} (σ : S.Section) (g : G) : (conjActOfSection σ) g = S.conjAct (σ g)

theorem TauCeti.GroupExtension.conjActOfSection_eq {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} (σ σ' : S.Section) : conjActOfSection σ = conjActOfSection σ'

theorem TauCeti.GroupExtension.InducesAction.conjActOfSection_eq_toMulAut {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (hact : InducesAction S) (σ : S.Section) : conjActOfSection σ = MulDistribMulAction.toMulAut G M

theorem TauCeti.GroupExtension.inducesAction_iff_conjActOfSection_eq {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) : InducesAction S ↔ conjActOfSection σ = MulDistribMulAction.toMulAut G M

InducesAction says exactly that the descended conjugation action is the ambient one. The reverse implication is the constructor: it suffices to check the two actions agree after presenting conjugation through a single section.

noncomputable def TauCeti.GroupExtension.factorSetFun {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ : S.Section) (p : G × G) : M

The factor set of a section, as a bare function: σ g * σ h * (σ (g * h))⁻¹ lies in the kernel, and this is its preimage there. It is a genuine factor set once the kernel is abelian, the section is normalized and the ambient action is the conjugation action; see TauCeti.GroupExtension.factorSet.

Equations

• TauCeti.GroupExtension.factorSetFun σ p = TauCeti.GroupExtension.inlInv✝ S (σ p.1 * σ p.2 * (σ (p.1 * p.2))⁻¹)

@[simp]

theorem TauCeti.GroupExtension.inl_factorSetFun {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ : S.Section) (g h : G) : S.inl (factorSetFun σ (g, h)) = σ g * σ h * (σ (g * h))⁻¹

theorem TauCeti.GroupExtension.section_mul {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ : S.Section) (g h : G) : σ g * σ h = S.inl (factorSetFun σ (g, h)) * σ (g * h)

The factor set measures the failure of a section to be a homomorphism. This matches the convention of TauCeti.FactorSet.canonicalSection_mul.

theorem TauCeti.GroupExtension.factorSetFun_one_one {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ : S.Section) (hσ : σ 1 = 1) : factorSetFun σ (1, 1) = 1

theorem TauCeti.GroupExtension.isMulCocycle₂_factorSetFun {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hact : InducesAction S) : groupCohomology.IsMulCocycle₂ (factorSetFun σ)

noncomputable def TauCeti.GroupExtension.factorSet {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hσ : σ 1 = 1) (hact : InducesAction S) : FactorSet G M

The factor set of a normalized section of an extension whose conjugation action on its abelian kernel is the ambient one.

Equations

• TauCeti.GroupExtension.factorSet σ hσ hact = { toFun := TauCeti.GroupExtension.factorSetFun σ, isMulCocycle₂' := ⋯, map_one_one' := ⋯ }

@[simp]

theorem TauCeti.GroupExtension.coe_factorSet {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hσ : σ 1 = 1) (hact : InducesAction S) : ⇑(factorSet σ hσ hact) = factorSetFun σ

theorem TauCeti.GroupExtension.inl_factorSet {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hσ : σ 1 = 1) (hact : InducesAction S) (g h : G) : S.inl ((factorSet σ hσ hact) (g, h)) = σ g * σ h * (σ (g * h))⁻¹

theorem TauCeti.GroupExtension.factorSet_monoidHomComp {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] {N : Type u_1} [CommGroup N] [MulDistribMulAction G N] {E' : Type u_2} [Group E'] {S' : GroupExtension N E' G} (σ : S.Section) (hσ : σ 1 = 1) (hact : InducesAction S) (hact' : InducesAction S') (f : M →*[G] N) (φ : E →* E') (hinl : φ.comp S.inl = S'.inl.comp f.toMonoidHom) (hright : S'.rightHom.comp φ = S.rightHom) : factorSet (σ.monoidHomComp φ hright) ⋯ hact' = (factorSet σ hσ hact).map f

The factor set of a section transported along a homomorphism of extensions φ over the identity of G that restricts to the equivariant f on the kernels is the pushforward along f of the factor set of the section.

noncomputable def TauCeti.GroupExtension.ofFactorSetHom {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hσ : σ 1 = 1) (hact : InducesAction S) : (factorSet σ hσ hact).Extension →* E

The comparison homomorphism ⟨a, g⟩ ↦ inl a * σ g from the twisted product built from the factor set of σ back to the extension. It is an isomorphism; see TauCeti.GroupExtension.factorSetToGroupExtensionEquiv.

Equations

• TauCeti.GroupExtension.ofFactorSetHom σ hσ hact = { toFun := fun (x : (TauCeti.GroupExtension.factorSet σ hσ hact).Extension) => S.inl x.left * σ x.right, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GroupExtension.ofFactorSetHom_apply {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hσ : σ 1 = 1) (hact : InducesAction S) (x : (factorSet σ hσ hact).Extension) : (ofFactorSetHom σ hσ hact) x = S.inl x.left * σ x.right

noncomputable def TauCeti.GroupExtension.factorSetToGroupExtensionEquiv {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hσ : σ 1 = 1) (hact : InducesAction S) : (factorSet σ hσ hact).groupExtension.Equiv S

An extension with abelian kernel is the twisted product built from its factor set.

Equations

• TauCeti.GroupExtension.factorSetToGroupExtensionEquiv σ hσ hact = GroupExtension.Equiv.ofMonoidHom (TauCeti.GroupExtension.ofFactorSetHom σ hσ hact) ⋯ ⋯

@[simp]

theorem TauCeti.GroupExtension.factorSetToGroupExtensionEquiv_apply {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (σ : S.Section) (hσ : σ 1 = 1) (hact : InducesAction S) (x : (factorSet σ hσ hact).Extension) : (factorSetToGroupExtensionEquiv σ hσ hact) x = S.inl x.left * σ x.right

noncomputable def TauCeti.GroupExtension.normalizeSection {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ : S.Section) : S.Section

Any section can be corrected at the identity to a normalized one; see TauCeti.GroupExtension.normalizeSection_one and TauCeti.GroupExtension.normalizeSection_apply.

Equations

• TauCeti.GroupExtension.normalizeSection σ = { toFun := fun (g : G) => if g = 1 then 1 else σ g, rightInverse_rightHom := ⋯ }

@[simp]

theorem TauCeti.GroupExtension.normalizeSection_one {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ : S.Section) : (normalizeSection σ) 1 = 1

@[simp]

theorem TauCeti.GroupExtension.normalizeSection_apply {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ : S.Section) (g : G) [Decidable (g = 1)] : (normalizeSection σ) g = if g = 1 then 1 else σ g

@[simp]

theorem TauCeti.GroupExtension.normalizeSection_apply_of_ne {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ : S.Section) {g : G} (hg : g ≠ 1) : (normalizeSection σ) g = σ g

theorem TauCeti.GroupExtension.exists_factorSet {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} [MulDistribMulAction G M] (hact : InducesAction S) : ∃ (α : FactorSet G M), Nonempty (α.groupExtension.Equiv S)

Every group extension with abelian kernel arises from a factor set, provided the ambient action of G on the kernel is the one the extension conjugates by.

theorem TauCeti.GroupExtension.inducesAction_groupExtension {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : InducesAction α.groupExtension

The twisted product built from a factor set conjugates its kernel by the given action of G.

theorem TauCeti.GroupExtension.factorSet_canonicalSection {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : factorSet α.canonicalSection ⋯ ⋯ = α

Reading the factor set back off the extension it builds returns it unchanged, when the factor set is read off the canonical section.

noncomputable def TauCeti.GroupExtension.sectionDiff {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ σ' : S.Section) (g : G) : M

The difference of two sections, as a function G → M: σ g * (σ' g)⁻¹ lies in the kernel, and this is its preimage there. It is the rescaling relating the two factor sets; see TauCeti.GroupExtension.isMulCoboundary₂_div.

Equations

• TauCeti.GroupExtension.sectionDiff σ σ' g = TauCeti.GroupExtension.inlInv✝ S (σ g * (σ' g)⁻¹)

@[simp]

theorem TauCeti.GroupExtension.inl_sectionDiff {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [Group M] {S : GroupExtension M E G} (σ σ' : S.Section) (g : G) : S.inl (sectionDiff σ σ' g) = σ g * (σ' g)⁻¹

theorem TauCeti.GroupExtension.factorSet_div_factorSet {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} (σ σ' : S.Section) [MulDistribMulAction G M] (hσ : σ 1 = 1) (hσ' : σ' 1 = 1) (hact : InducesAction S) (g h : G) : (factorSet σ hσ hact) (g, h) / (factorSet σ' hσ' hact) (g, h) = g • sectionDiff σ σ' h / sectionDiff σ σ' (g * h) * sectionDiff σ σ' g

The factor sets of two normalized sections differ by the coboundary of their difference, with the coboundary spelled as in groupCohomology.IsMulCoboundary₂. This is the identity behind TauCeti.GroupExtension.isMulCoboundary₂_div, stated with its witness visible so that properties of the witness, such as its continuity, can be tracked.

theorem TauCeti.GroupExtension.isMulCoboundary₂_div {G : Type u} {M : Type v} {E : Type w} [Group G] [Group E] [CommGroup M] {S : GroupExtension M E G} (σ σ' : S.Section) [MulDistribMulAction G M] (hσ : σ 1 = 1) (hσ' : σ' 1 = 1) (hact : InducesAction S) : groupCohomology.IsMulCoboundary₂ fun (p : G × G) => (factorSet σ hσ hact) p / (factorSet σ' hσ' hact) p

Two normalized sections give cohomologous factor sets. Combined with TauCeti.FactorSet.nonempty_groupExtensionEquiv, which turns a coboundary back into an equivalence of extensions, this says the class of the factor set in H²(G, M) is an invariant of the extension.