A projective representation is a linear representation of the central extension of its factor set

A projective representation ρ : G → (V ≃ₗ[k] V) with factor set α is multiplicative only up to the scalars α, so it is not a homomorphism. Enlarging G by those scalars repairs this: the central extension 1 → kˣ → E_α → G → 1 built from α in TauCeti/GroupTheory/GroupExtension/Of/FactorSet.lean carries a genuine homomorphism

E_α → (V ≃ₗ[k] V), ⟨a, g⟩ ↦ a • ρ g,

the linearization of ρ. This file builds it, and shows that nothing is lost: the projective representation is recovered by restricting the linearization along the canonical section g ↦ ⟨1, g⟩, and the two constructions are mutually inverse. The linear representations of E_α that arise this way are exactly those under which the central copy of kˣ acts by its own scalars, so TauCeti.isProjectiveRepEquivExtensionHom is a bijection between the projective representations of G with factor set α and the linear representations of E_α with that property.

The curried/uncurried bookkeeping bridges come first, because the two halves of the theory spell a factor set differently. TauCeti.FactorSet is the uncurried, bundled G × G → M of a general G-module M, which is what the group extension is built from, while TauCeti.IsFactorSet is a curried Prop-valued class on G → G → kˣ, which is what a projective representation carries. The two agree when G acts trivially on kˣ, the case in which the extension is central (TauCeti.FactorSet.inl_range_le_center), and TauCeti.FactorSet.isFactorSet_curry and TauCeti.IsFactorSet.toFactorSet translate in the two directions. Triviality of the action is carried as an explicit hypothesis ∀ (g : G) (a : kˣ), g • a = a rather than as a chosen instance, matching TauCeti.FactorSet.inl_range_le_center: the type TauCeti.FactorSet G kˣ already depends on an ambient MulDistribMulAction G kˣ, so leaving that action free lets a factor set for any action be fed to the statements, and only the results that genuinely need centrality pay for it. A projective representation itself carries no action, so the closing existence statement supplies the trivial one, TauCeti.trivialMulDistribMulAction, and asks for nothing of its caller.

For a factor set whose values have exponent dividing n, TauCeti.IsFactorSet.toRootsOfUnityFactorSet also restricts the values to rootsOfUnity n k. This lets finite lifting extensions use roots of unity as their kernel coefficients.

Main definitions

• TauCeti.IsFactorSet.toFactorSet: a normalized curried factor set, bundled as a TauCeti.FactorSet for a trivial action, so that its central extension is available.
• TauCeti.IsFactorSet.toRootsOfUnityFactorSet: a factor set with values of exponent dividing n, bundled with coefficients in the n-th roots of unity for finite lifting extensions.
• TauCeti.IsProjectiveRep.linearization: the homomorphism E_α → (V ≃ₗ[k] V) attached to a projective representation with factor set α, with TauCeti.IsProjectiveRep.linearizationRepresentation its packaging as a Representation k E_α V.
• TauCeti.FactorSet.restrictCanonicalSection: the restriction of a Representation k E_α V along the canonical section, as linear automorphisms of V, the form in which it is a projective representation.
• TauCeti.isProjectiveRepEquivExtensionHom: the resulting bijection.

Main results

• TauCeti.FactorSet.isFactorSet_curry: for a trivial action a TauCeti.FactorSet valued in kˣ is a normalized factor set in the curried sense of TauCeti.IsFactorSet.
• TauCeti.IsProjectiveRep.linearization_mk_one: restricting the linearization along the canonical section returns the projective representation, and TauCeti.IsProjectiveRep.linearization_inl: the central kˣ acts by its own scalars.
• TauCeti.isProjectiveRep_comp_canonicalSection: conversely, restricting along the canonical section any linear representation of E_α under which kˣ acts by scalars gives a projective representation with factor set α, and TauCeti.isProjectiveRep_of_representation_canonicalSection: the same for a linear representation presented as an ordinary Representation k E_α V, whose scalar condition is read off the linearization by TauCeti.IsProjectiveRep.linearizationRepresentation_inl, with TauCeti.isProjectiveRep_restrictCanonicalSection its instance at the canonical restriction.
• TauCeti.IsProjectiveRep.forall_linearization_mem_iff: the linearization and the projective representation have the same invariant submodules, which is why irreducibility transfers between them.
• TauCeti.IsProjectiveRep.exists_factorSet_linearization: every projective representation of G is a linear representation of a central extension of G by kˣ, for the extension built from the factor set the projective representation carries.

References

This is the linearization step of Layer 7 of the induction and restriction roadmap, "projective representations, factor sets, and the Schur multiplier": it is the mechanism behind the representation group, through which every projective representation of G lifts to an ordinary linear representation of a central extension.

• G. Karpilovsky, Projective Representations of Finite Groups, Marcel Dekker (1985), Ch. 3.
• I. M. Isaacs, Character Theory of Finite Groups, AMS Chelsea (1976), Ch. 11.

Factor sets, curried and uncurried

The extension is built from a bundled, uncurried factor set while a projective representation carries a curried one; for the trivial action TauCeti.trivialMulDistribMulAction, the two notions agree.

def TauCeti.IsFactorSet.toRootsOfUnityFactorSet {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {α : G → G → kˣ} (hα : IsFactorSet α) {n : ℕ} (hpow : ∀ (g h : G), α g h ^ n = 1) : FactorSet G ↥(rootsOfUnity n k)

A factor set whose values have exponent dividing n, valued in the n-th roots of unity.

Equations

• hα.toRootsOfUnityFactorSet hpow = { toFun := fun (p : G × G) => ⟨α p.1 p.2, ⋯⟩, isMulCocycle₂' := ⋯, map_one_one' := ⋯ }

@[simp]

theorem TauCeti.IsFactorSet.coe_toRootsOfUnityFactorSet_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {α : G → G → kˣ} (hα : IsFactorSet α) {n : ℕ} (hpow : ∀ (g h : G), α g h ^ n = 1) (p : G × G) : ↑((hα.toRootsOfUnityFactorSet hpow) p) = α p.1 p.2

theorem TauCeti.FactorSet.isFactorSet_curry {k : Type u} {G : Type v} [CommSemiring k] [Group G] [MulDistribMulAction G kˣ] (α : FactorSet G kˣ) (htriv : ∀ (g : G) (a : kˣ), g • a = a) : IsFactorSet (Function.curry ⇑α)

A factor set valued in kˣ for the trivial action is a normalized factor set in the curried sense of TauCeti.IsFactorSet. The cocycle identity of TauCeti.FactorSet carries an action on one of its four terms, which the hypothesis removes; the two normalizations agree.

def TauCeti.IsFactorSet.toFactorSet {k : Type u} {G : Type v} [CommSemiring k] [Group G] [MulDistribMulAction G kˣ] (α : G → G → kˣ) [IsFactorSet α] (htriv : ∀ (g : G) (a : kˣ), g • a = a) : FactorSet G kˣ

A normalized factor set in the curried sense of TauCeti.IsFactorSet, bundled as a TauCeti.FactorSet for a trivial action of G on kˣ. This is what makes the central extension TauCeti.FactorSet.Extension of the factor set of a projective representation available.

Equations

• TauCeti.IsFactorSet.toFactorSet α htriv = { toFun := fun (p : G × G) => α p.1 p.2, isMulCocycle₂' := ⋯, map_one_one' := ⋯ }

@[simp]

theorem TauCeti.IsFactorSet.toFactorSet_apply {k : Type u} {G : Type v} [CommSemiring k] [Group G] [MulDistribMulAction G kˣ] (α : G → G → kˣ) [IsFactorSet α] (htriv : ∀ (g : G) (a : kˣ), g • a = a) (p : G × G) : (toFactorSet α htriv) p = α p.1 p.2

The bundled factor set of a curried one takes the same values.

@[simp]

theorem TauCeti.IsFactorSet.curry_coe_toFactorSet {k : Type u} {G : Type v} [CommSemiring k] [Group G] [MulDistribMulAction G kˣ] (α : G → G → kˣ) [IsFactorSet α] (htriv : ∀ (g : G) (a : kˣ), g • a = a) : Function.curry ⇑(toFactorSet α htriv) = α

Bundling a curried factor set and currying it back returns it unchanged, so a projective representation with factor set α is one with the factor set of TauCeti.IsFactorSet.toFactorSet.

The linearization of a projective representation

Multiplying by the scalar recorded in the kˣ-component of the extension repairs the failure of ρ to be multiplicative, because that failure is exactly the factor set the extension is twisted by.

def TauCeti.IsProjectiveRep.linearization {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (hρ : IsProjectiveRep ρ (Function.curry ⇑α)) (htriv : ∀ (g : G) (a : kˣ), g • a = a) : α.Extension →* V ≃ₗ[k] V

The linearization of a projective representation with factor set α: the homomorphism from the central extension E_α of G by kˣ to the linear automorphisms of V, sending ⟨a, g⟩ to a • ρ g. It is multiplicative precisely because the extension is twisted by the same factor set that measures the failure of ρ to be multiplicative.

Equations

• hρ.linearization htriv = { toFun := fun (x : α.Extension) => LinearEquiv.smulOfUnit x.left * ρ x.right, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.IsProjectiveRep.linearization_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (hρ : IsProjectiveRep ρ (Function.curry ⇑α)) (htriv : ∀ (g : G) (a : kˣ), g • a = a) (x : α.Extension) (v : V) : ((hρ.linearization htriv) x) v = ↑x.left • (ρ x.right) v

The linearization acts by the scalar recorded in the kˣ-component of the extension, followed by the projective representation at its G-component.

@[simp]

theorem TauCeti.IsProjectiveRep.linearization_inl {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (hρ : IsProjectiveRep ρ (Function.curry ⇑α)) (htriv : ∀ (g : G) (a : kˣ), g • a = a) (a : kˣ) : (hρ.linearization htriv) (α.inl a) = LinearEquiv.smulOfUnit a

The central copy of kˣ acts through the linearization by its own scalars. This is the condition that singles out the linearizations among all linear representations of E_α; see TauCeti.isProjectiveRepEquivExtensionHom.

@[simp]

theorem TauCeti.IsProjectiveRep.linearization_mk_one {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (hρ : IsProjectiveRep ρ (Function.curry ⇑α)) (htriv : ∀ (g : G) (a : kˣ), g • a = a) (g : G) : (hρ.linearization htriv) { left := 1, right := g } = ρ g

The projective representation is recovered from its linearization, stated at the element ⟨1, g⟩ that TauCeti.FactorSet.canonicalSection_apply rewrites the canonical section to, so that simp also restricts the linearization along the canonical section. Unlike TauCeti.IsProjectiveRep.linearization_apply it applies to the linearization itself rather than to its value at a vector.

theorem TauCeti.IsProjectiveRep.forall_linearization_mem_iff {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (hρ : IsProjectiveRep ρ (Function.curry ⇑α)) (htriv : ∀ (g : G) (a : kˣ), g • a = a) {W : Submodule k V} : (∀ (x : α.Extension), ∀ w ∈ W, ((hρ.linearization htriv) x) w ∈ W) ↔ ∀ (g : G), ∀ w ∈ W, (ρ g) w ∈ W

The linearization has the same invariant submodules as the projective representation. The kˣ-component of the extension acts by a scalar, which no submodule can escape, so invariance under E_α is invariance under the automorphisms ρ g alone. This is what makes irreducibility of a projective representation and of its linearization the same condition.

def TauCeti.IsProjectiveRep.linearizationRepresentation {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (hρ : IsProjectiveRep ρ (Function.curry ⇑α)) (htriv : ∀ (g : G) (a : kˣ), g • a = a) : Representation k α.Extension V

The linearization, packaged as a Representation of the central extension E_α on V, so that the machinery written against Representation applies to it.

Equations

• hρ.linearizationRepresentation htriv = LinearEquiv.automorphismGroup.toLinearMapMonoidHom.comp (hρ.linearization htriv)

@[simp]

theorem TauCeti.IsProjectiveRep.linearizationRepresentation_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (hρ : IsProjectiveRep ρ (Function.curry ⇑α)) (htriv : ∀ (g : G) (a : kˣ), g • a = a) (x : α.Extension) (v : V) : ((hρ.linearizationRepresentation htriv) x) v = ↑x.left • (ρ x.right) v

The packaged representation acts by the same formula as the linearization it is built from.

@[simp]

theorem TauCeti.IsProjectiveRep.linearizationRepresentation_inl {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (hρ : IsProjectiveRep ρ (Function.curry ⇑α)) (htriv : ∀ (g : G) (a : kˣ), g • a = a) (a : kˣ) : (hρ.linearizationRepresentation htriv) (α.inl a) = ↑a • LinearMap.id

The central copy of kˣ acts through the packaged representation by its own scalars, the condition of TauCeti.isProjectiveRep_of_representation_canonicalSection read on TauCeti.IsProjectiveRep.linearizationRepresentation.

theorem TauCeti.isProjectiveRep_comp_canonicalSection {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} (htriv : ∀ (g : G) (a : kˣ), g • a = a) (π : α.Extension →* V ≃ₗ[k] V) (hπ : ∀ (a : kˣ), π (α.inl a) = LinearEquiv.smulOfUnit a) : IsProjectiveRep (fun (g : G) => π (α.canonicalSection g)) (Function.curry ⇑α)

Restricting a linear representation of E_α along the canonical section gives a projective representation with factor set α, as soon as the central copy of kˣ acts by its own scalars. The canonical section fails to be a homomorphism by exactly α, and that failure becomes the factor set.

theorem TauCeti.isProjectiveRep_of_representation_canonicalSection {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} {ρ : G → V ≃ₗ[k] V} (htriv : ∀ (g : G) (a : kˣ), g • a = a) (π : Representation k α.Extension V) (hπ : ∀ (a : kˣ), π (α.inl a) = ↑a • LinearMap.id) (hρ : ∀ (g : G), ↑(ρ g) = π (α.canonicalSection g)) : IsProjectiveRep ρ (Function.curry ⇑α)

The same converse for an ordinary Representation k E_α V, the form in which the machinery written against Representation supplies a linear representation of the extension: if the central copy of kˣ acts by its own scalars, then a family ρ of linear automorphisms restricting π along the canonical section is a projective representation with factor set α. The automorphisms are taken as data because a Representation records only linear maps; TauCeti.IsProjectiveRep.linearizationRepresentation together with TauCeti.IsProjectiveRep.linearizationRepresentation_inl is the case that recovers ρ itself, and TauCeti.isProjectiveRep_restrictCanonicalSection is the case of the canonical restriction TauCeti.FactorSet.restrictCanonicalSection, which needs no automorphisms supplied.

def TauCeti.FactorSet.restrictCanonicalSection {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] (α : FactorSet G kˣ) (π : Representation k α.Extension V) (g : G) : V ≃ₗ[k] V

A linear representation of the extension E_α, restricted along the canonical section, as the family of linear automorphisms of V that a projective representation asks for: a Representation records only linear maps, and Representation.asGroupHom together with LinearMap.GeneralLinearGroup.generalLinearEquiv promotes its values back to automorphisms. When the central copy of kˣ acts by its own scalars this family is a projective representation with factor set α, by TauCeti.isProjectiveRep_restrictCanonicalSection.

Equations

• α.restrictCanonicalSection π g = (LinearMap.GeneralLinearGroup.generalLinearEquiv k V) (π.asGroupHom (α.canonicalSection g))

@[simp]

theorem TauCeti.FactorSet.restrictCanonicalSection_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] (α : FactorSet G kˣ) (π : Representation k α.Extension V) (g : G) (v : V) : (α.restrictCanonicalSection π g) v = (π (α.canonicalSection g)) v

The restriction along the canonical section acts as the representation does at ⟨1, g⟩.

theorem TauCeti.isProjectiveRep_restrictCanonicalSection {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] {α : FactorSet G kˣ} (htriv : ∀ (g : G) (a : kˣ), g • a = a) (π : Representation k α.Extension V) (hπ : ∀ (a : kˣ), π (α.inl a) = ↑a • LinearMap.id) : IsProjectiveRep (α.restrictCanonicalSection π) (Function.curry ⇑α)

Restricting an ordinary Representation k E_α V along the canonical section gives a projective representation with factor set α, as soon as the central copy of kˣ acts by its own scalars. This is TauCeti.isProjectiveRep_of_representation_canonicalSection for the canonical choice of automorphisms, so that no conversion has to be supplied by the caller.

def TauCeti.isProjectiveRepEquivExtensionHom (k : Type u) {G : Type v} (V : Type w) [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] (α : FactorSet G kˣ) (htriv : ∀ (g : G) (a : kˣ), g • a = a) : { ρ : G → V ≃ₗ[k] V // IsProjectiveRep ρ (Function.curry ⇑α) } ≃ { π : α.Extension →* V ≃ₗ[k] V // ∀ (a : kˣ), π (α.inl a) = LinearEquiv.smulOfUnit a }

Projective representations of G with factor set α are exactly the linear representations of the central extension E_α under which the central copy of kˣ acts by its own scalars. The bijection sends a projective representation to its linearization, and a linear representation to its restriction along the canonical section.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.isProjectiveRepEquivExtensionHom_apply (k : Type u) {G : Type v} (V : Type w) [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] (α : FactorSet G kˣ) (htriv : ∀ (g : G) (a : kˣ), g • a = a) (ρ : { ρ : G → V ≃ₗ[k] V // IsProjectiveRep ρ (Function.curry ⇑α) }) : ↑((isProjectiveRepEquivExtensionHom k V α htriv) ρ) = ⋯.linearization htriv

The bijection sends a projective representation to its linearization.

@[simp]

theorem TauCeti.isProjectiveRepEquivExtensionHom_symm_apply (k : Type u) {G : Type v} (V : Type w) [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [MulDistribMulAction G kˣ] (α : FactorSet G kˣ) (htriv : ∀ (g : G) (a : kˣ), g • a = a) (π : { π : α.Extension →* V ≃ₗ[k] V // ∀ (a : kˣ), π (α.inl a) = LinearEquiv.smulOfUnit a }) : ↑((isProjectiveRepEquivExtensionHom k V α htriv).symm π) = fun (g : G) => ↑π (α.canonicalSection g)

The inverse bijection restricts a linear representation along the canonical section.

Every projective representation linearizes

A projective representation carries no action of G on kˣ, so the statement below supplies the trivial one, the action for which the extension of its factor set is central.

theorem TauCeti.IsProjectiveRep.exists_factorSet_linearization {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {ρ : G → V ≃ₗ[k] V} {α : G → G → kˣ} (hρ : IsProjectiveRep ρ α) : ∃ (β : FactorSet G kˣ) (π : β.Extension →* V ≃ₗ[k] V), β.inl.range ≤ Subgroup.center β.Extension ∧ (∀ (a : kˣ), π (β.inl a) = LinearEquiv.smulOfUnit a) ∧ ∀ (g : G), π (β.canonicalSection g) = ρ g

Every projective representation of G linearizes over a central extension of G by kˣ. The extension is the one built from the factor set the projective representation carries, over the trivial action TauCeti.trivialMulDistribMulAction of G on kˣ: its copy of kˣ is central, it acts by its own scalars, and restricting along the canonical section returns the projective representation.