Projective representations and their factor sets

A projective representation of a monoid G on a k-module V is a normalized lift ρ : G → (V ≃ₗ[k] V) of a homomorphism into the projective linear group: it sends 1 to the identity and is multiplicative up to a scalar,

ρ g₁ (ρ g₂ x) = α g₁ g₂ • ρ (g₁ * g₂) x

for a normalized factor set α : G → G → kˣ, the factor set of ρ. Both the invertibility of each ρ g and the normalization ρ 1 = 1 are load-bearing: the constant zero family satisfies the displayed relation for every α, so without them nothing below is true.

Working with a normalized lift rather than with a homomorphism G → PGL(V) keeps the theory basis-free and puts the factor set in the statement, where the rest of the theory needs it.

That α is a factor set is rarely something to check by hand: as soon as kˣ acts faithfully on V it is determined by ρ, and TauCeti.IsProjectiveRep.of_map_one_mul_apply derives its normalization and its multiplicative 2-cocycle identity from associativity of composition, so there only the two conditions on ρ remain. The main results then identify projective representations with factor set α with modules over the twisted monoid algebra k_α[G] of TauCeti.twistedMonoidAlgebra: a module structure on V is an algebra map k_α[G] →ₐ[k] Module.End k V, and TauCeti.isProjectiveRepEquivAlgHom is the bijection between those and the projective representations with factor set α. Under it the twisted monoid algebra itself becomes the twisted regular representation, which realizes every factor set.

Main definitions

• TauCeti.IsProjectiveRep ρ α: ρ is a projective representation with factor set α.
• TauCeti.IsProjectiveRep.toAlgHom: the algebra map k_α[G] →ₐ[k] Module.End k V a projective representation with factor set α determines, that is, the k_α[G]-module structure on V.
• TauCeti.projectiveRepOfAlgHom: the projective representation attached to an algebra map out of k_α[G], inverse to the previous construction.
• TauCeti.isProjectiveRepEquivAlgHom: the resulting bijection.
• TauCeti.twistedRegularRep: the twisted regular representation of G on G →₀ k.

Main results

• TauCeti.IsProjectiveRep.of_map_one_mul_apply: when kˣ acts faithfully on V the factor-set axioms are automatic, and TauCeti.IsProjectiveRep.factorSet_eq: there the factor set is determined by the lift.
• TauCeti.IsProjectiveRep.rescale: rescaling the lift by c : G → kˣ multiplies the factor set by the coboundary of c. A fixed lift determines its factor set outright; it is the cohomology class that is unchanged by normalized rescaling, hence an invariant of the underlying projective action rather than of the lift.
• TauCeti.IsProjectiveRep.toMonoidHom and TauCeti.IsProjectiveRep.of_monoidHom: the projective representations with trivial factor set are exactly the linear representations.
• TauCeti.IsProjectiveRep.tensorProduct: the tensor product of two projective representations is projective with the product factor set.
• TauCeti.IsProjectiveRep.comp: a projective representation inflates along a homomorphism, with the pulled-back factor set.
• TauCeti.exists_isProjectiveRep: every normalized factor set is the factor set of a projective representation.

Implementation notes

Factor sets use the curried form α : G → G → kˣ: α g h is the scalar attached to the ordered pair (g, h). This is the convention of TauCeti.IsFactorSet and TauCeti.twistedMonoidAlgebra, whose basis elements multiply as e g * e h = (α g h : k) • e (g * h). Thus the twisted algebra and the lift use the same left-action convention.

References

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

structure TauCeti.IsProjectiveRep {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : G → V ≃ₗ[k] V) (α : G → G → kˣ) : Prop

A projective representation of G on V with factor set α: a normalized factor set α, in the sense of TauCeti.IsFactorSet, together with a normalized lift ρ : G → (V ≃ₗ[k] V) that is multiplicative up to the scalars α. Invertibility of the ρ g is carried by the type V ≃ₗ[k] V and normalization by map_one; without them the zero family would satisfy mul_apply for every α, and on the zero module it still does, which is why the factor-set axioms are recorded here rather than left to be derived. When kˣ acts faithfully on V they are derivable, and TauCeti.IsProjectiveRep.of_map_one_mul_apply derives them.

• isFactorSet : IsFactorSet α

  The scalars are a normalized multiplicative 2-cocycle.

• map_one : ρ 1 = 1

  The lift is normalized: the identity of G acts as the identity.

• mul_apply (g₁ g₂ : G) (x : V) : (ρ g₁) ((ρ g₂) x) = ↑(α g₁ g₂) • (ρ (g₁ * g₂)) x

  The lift is multiplicative up to the factor set.

theorem TauCeti.IsProjectiveRep.toLinearMap_mul {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : G → V ≃ₗ[k] V} {α : G → G → kˣ} (h : IsProjectiveRep ρ α) (g₁ g₂ : G) : ↑(ρ g₁) * ↑(ρ g₂) = ↑(α g₁ g₂) • ↑(ρ (g₁ * g₂))

The defining relation, read in the endomorphism algebra: this is the form the universal property of the twisted monoid algebra consumes.

theorem TauCeti.IsProjectiveRep.rescale {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : G → V ≃ₗ[k] V} {α : G → G → kˣ} (h : IsProjectiveRep ρ α) (c : G → kˣ) (hc : c 1 = 1) : IsProjectiveRep (fun (g : G) => ρ g ≪≫ₗ LinearEquiv.smulOfUnit (c g)) fun (g₁ g₂ : G) => c g₁ * c g₂ * (c (g₁ * g₂))⁻¹ * α g₁ g₂

Rescaling a projective representation. Multiplying the lift by units c : G → kˣ, again normalized, is again a projective representation, and multiplies the factor set by the coboundary of c. So only the class of the factor set modulo coboundaries is an invariant of the underlying homomorphism to the projective linear group.

theorem TauCeti.IsProjectiveRep.of_monoidHom {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (π : G →* V ≃ₗ[k] V) : IsProjectiveRep (⇑π) 1

A linear representation, presented as a homomorphism into the group of linear automorphisms, is a projective representation with trivial factor set.

def TauCeti.IsProjectiveRep.toMonoidHom {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : G → V ≃ₗ[k] V} (h : IsProjectiveRep ρ 1) : G →* V ≃ₗ[k] V

A projective representation with trivial factor set is a linear representation: the lift is itself a homomorphism into the group of linear automorphisms.

Equations

• h.toMonoidHom = { toFun := ρ, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.IsProjectiveRep.coe_toMonoidHom {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : G → V ≃ₗ[k] V} (h : IsProjectiveRep ρ 1) : ⇑h.toMonoidHom = ρ

The homomorphism attached to a projective representation with trivial factor set is the lift itself.

theorem TauCeti.IsProjectiveRep.tensorProduct {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : G → V ≃ₗ[k] V} {α : G → G → kˣ} {V' : Type u_1} [AddCommMonoid V'] [Module k V'] {ρ' : G → V' ≃ₗ[k] V'} {α' : G → G → kˣ} (h : IsProjectiveRep ρ α) (h' : IsProjectiveRep ρ' α') : IsProjectiveRep (fun (g : G) => TensorProduct.congr (ρ g) (ρ' g)) (α * α')

The tensor product of two projective representations is a projective representation whose factor set is the product of the two factor sets. In particular a projective representation tensored with one carrying the inverse factor set is a linear representation.

theorem TauCeti.IsProjectiveRep.comp {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : G → V ≃ₗ[k] V} {α : G → G → kˣ} {H : Type u_1} [Monoid H] (h : IsProjectiveRep ρ α) (f : H →* G) : IsProjectiveRep (fun (g : H) => ρ (f g)) fun (g₁ g₂ : H) => α (f g₁) (f g₂)

Inflation of a projective representation. Pulling a projective representation of G back along a homomorphism f : H →* G gives a projective representation of H whose factor set is the pullback of the factor set.

For a faithful action of the units the factor-set axioms are automatic

When kˣ acts faithfully on V the scalars in the defining relation are determined by the lift, and associativity of composition forces the cocycle identity on them. So there a normalized lift that is multiplicative up to α is already a projective representation, and its factor set is unique. Faithfulness is exactly what lets a scalar be read off from its action, and only the scalars in kˣ are ever compared, so [FaithfulSMul kˣ V] is what is asked for; k acting faithfully — as it does on a nonzero torsion-free module, a nonzero vector space in particular — supplies it.

theorem TauCeti.IsProjectiveRep.of_map_one_mul_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [FaithfulSMul kˣ V] {ρ : G → V ≃ₗ[k] V} {α : G → G → kˣ} (h₁ : ρ 1 = 1) (h₂ : ∀ (g₁ g₂ : G) (x : V), (ρ g₁) ((ρ g₂) x) = ↑(α g₁ g₂) • (ρ (g₁ * g₂)) x) : IsProjectiveRep ρ α

For a faithful scalar action the factor-set axioms come for free. A normalized lift that is multiplicative up to α is a projective representation: the normalization of α follows from that of the lift, and its multiplicative 2-cocycle identity from associativity of composition. So on a nonzero vector space, say, the cocycle identity never has to be checked.

theorem TauCeti.IsProjectiveRep.factorSet_eq {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [FaithfulSMul kˣ V] {ρ : G → V ≃ₗ[k] V} {α β : G → G → kˣ} (h : IsProjectiveRep ρ α) (h' : IsProjectiveRep ρ β) : α = β

The factor set is determined by the lift: for a faithful action of the units a projective representation has at most one factor set, so α is not extra data but an invariant of ρ.

Projective representations are twisted-group-algebra modules

noncomputable def TauCeti.IsProjectiveRep.toAlgHom {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid V] [Module k V] [Monoid G] {ρ : G → V ≃ₗ[k] V} {α : G → G → kˣ} (h : IsProjectiveRep ρ α) : ↥(twistedMonoidAlgebra k G α) →ₐ[k] Module.End k V

A projective representation with factor set α is a k_α[G]-module. The algebra map is the one the universal property of TauCeti.twistedMonoidAlgebra produces from the lift; a module structure on V over an algebra is exactly such an algebra map to Module.End k V.

Writing the domain down needs the factor-set axioms, since TauCeti.twistedMonoidAlgebra takes them as an instance argument; they are supplied by h itself, so no separate IsFactorSet α instance need be in scope.

Equations

• h.toAlgHom = TauCeti.TwistedMonoidAlgebra.lift (fun (g : G) => ↑(ρ g)) ⋯ ⋯

@[simp]

theorem TauCeti.IsProjectiveRep.toAlgHom_of {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid V] [Module k V] [Monoid G] {ρ : G → V ≃ₗ[k] V} {α : G → G → kˣ} (h : IsProjectiveRep ρ α) (g : G) : h.toAlgHom (TwistedMonoidAlgebra.of g) = ↑(ρ g)

The k_α[G]-module structure attached to a projective representation acts on the basis element at g by the lift at g.

noncomputable def TauCeti.projectiveRepOfAlgHom {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid V] [Module k V] [Group G] {α : G → G → kˣ} [IsFactorSet α] (φ : ↥(twistedMonoidAlgebra k G α) →ₐ[k] Module.End k V) (g : G) : V ≃ₗ[k] V

A k_α[G]-module is a projective representation with factor set α. The basis element at g is a unit of k_α[G], so it acts on V as a linear automorphism.

Equations

• TauCeti.projectiveRepOfAlgHom φ g = LinearEquiv.ofBijective (φ (TauCeti.TwistedMonoidAlgebra.of g)) ⋯

@[simp]

theorem TauCeti.projectiveRepOfAlgHom_apply {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid V] [Module k V] [Group G] {α : G → G → kˣ} [IsFactorSet α] (φ : ↥(twistedMonoidAlgebra k G α) →ₐ[k] Module.End k V) (g : G) (x : V) : (projectiveRepOfAlgHom φ g) x = (φ (TwistedMonoidAlgebra.of g)) x

The projective representation attached to a k_α[G]-module acts at g by the basis element at g.

theorem TauCeti.isProjectiveRep_projectiveRepOfAlgHom {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid V] [Module k V] [Group G] {α : G → G → kˣ} [IsFactorSet α] (φ : ↥(twistedMonoidAlgebra k G α) →ₐ[k] Module.End k V) : IsProjectiveRep (projectiveRepOfAlgHom φ) α

The action of the basis elements of k_α[G] on a module is a projective representation with factor set α.

@[simp]

theorem TauCeti.toAlgHom_projectiveRepOfAlgHom {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid V] [Module k V] [Group G] {α : G → G → kˣ} [IsFactorSet α] {φ : ↥(twistedMonoidAlgebra k G α) →ₐ[k] Module.End k V} : ⋯.toAlgHom = φ

Reading a k_α[G]-module as a projective representation and back returns the module.

@[simp]

theorem TauCeti.projectiveRepOfAlgHom_toAlgHom {k : Type u} {G : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid V] [Module k V] [Group G] {α : G → G → kˣ} {ρ : G → V ≃ₗ[k] V} (h : IsProjectiveRep ρ α) : projectiveRepOfAlgHom h.toAlgHom = ρ

Reading a projective representation as a k_α[G]-module and back returns the lift.

noncomputable def TauCeti.isProjectiveRepEquivAlgHom (k : Type u) {G : Type v} (V : Type w) [CommSemiring k] [AddCommMonoid V] [Module k V] [Group G] (α : G → G → kˣ) [IsFactorSet α] : { ρ : G → V ≃ₗ[k] V // IsProjectiveRep ρ α } ≃ (↥(twistedMonoidAlgebra k G α) →ₐ[k] Module.End k V)

Projective representations with factor set α are exactly the k_α[G]-modules.

Equations

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

@[simp]

theorem TauCeti.isProjectiveRepEquivAlgHom_apply (k : Type u) {G : Type v} (V : Type w) [CommSemiring k] [AddCommMonoid V] [Module k V] [Group G] (α : G → G → kˣ) [IsFactorSet α] (ρ : { ρ : G → V ≃ₗ[k] V // IsProjectiveRep ρ α }) : (isProjectiveRepEquivAlgHom k V α) ρ = ⋯.toAlgHom

The bijection sends a projective representation to the k_α[G]-module structure it determines.

@[simp]

theorem TauCeti.isProjectiveRepEquivAlgHom_symm_apply (k : Type u) {G : Type v} (V : Type w) [CommSemiring k] [AddCommMonoid V] [Module k V] [Group G] (α : G → G → kˣ) [IsFactorSet α] (ψ : ↥(twistedMonoidAlgebra k G α) →ₐ[k] Module.End k V) : ↑((isProjectiveRepEquivAlgHom k V α).symm ψ) = projectiveRepOfAlgHom ψ

The inverse bijection sends a k_α[G]-module structure to the action of the basis elements.

The twisted regular representation

noncomputable def TauCeti.twistedRegularRep (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] (α : G → G → kˣ) [IsFactorSet α] (g : G) : (G →₀ k) ≃ₗ[k] G →₀ k

The twisted regular representation of G on G →₀ k: the twisted monoid algebra k_α[G] acting on itself, read through its realization as operators on G →₀ k. Its factor set is α, so every normalized factor set is realized by a projective representation.

Equations

• TauCeti.twistedRegularRep k G α g = TauCeti.projectiveRepOfAlgHom (TauCeti.twistedMonoidAlgebra k G α).val g

@[simp]

theorem TauCeti.twistedRegularRep_apply (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] (α : G → G → kˣ) [IsFactorSet α] (g : G) (x : G →₀ k) : (twistedRegularRep k G α g) x = (twistedTranslation k α g) x

The twisted regular representation acts by the twisted translations.

theorem TauCeti.isProjectiveRep_twistedRegularRep (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] (α : G → G → kˣ) [IsFactorSet α] : IsProjectiveRep (twistedRegularRep k G α) α

The twisted regular representation has factor set α.

theorem TauCeti.exists_isProjectiveRep (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] (α : G → G → kˣ) [IsFactorSet α] : ∃ (ρ : G → (G →₀ k) ≃ₗ[k] G →₀ k), IsProjectiveRep ρ α

Every normalized factor set arises from a projective representation. Together with TauCeti.IsProjectiveRep.isFactorSet this characterizes the factor sets of projective representations of a group: they are exactly the normalized multiplicative 2-cocycles.