The twisted monoid algebra of a factor set

A factor set on a monoid G with values in the units of a commutative semiring k is a normalized multiplicative 2-cocycle α : G → G → kˣ. The twisted monoid algebra k_α[G] is the k-algebra with a basis e g indexed by G and multiplication e g * e h = α g h • e (g * h); for the trivial factor set it is the ordinary monoid algebra MonoidAlgebra k G. When G is a group it is the twisted group algebra, the module-theoretic home of projective representation theory: a projective representation of G with factor set α is exactly a k_α[G]-module.

This file constructs the algebra as the image of the twisted regular representation. The operator TauCeti.twistedTranslation k α g on G →₀ k sends the basis vector at h to α g h times the basis vector at g * h, and the cocycle identity says exactly that twistedTranslation k α g * twistedTranslation k α h = α g h • twistedTranslation k α (g * h). So the k-span of these operators is a subalgebra of Module.End k (G →₀ k), and that subalgebra is TauCeti.twistedMonoidAlgebra k G α. Associativity and unitality of the twisted product are inherited from composition of linear maps rather than re-proved by hand, and the operators are linearly independent -- each is recovered from its value at the basis vector of 1 -- so they form a basis and the multiplication table above holds on the nose.

Main definitions and results

• TauCeti.IsFactorSet: a normalized factor set, that is, a normalized multiplicative 2-cocycle α : G → G → kˣ, with the pointwise product and inverse of factor sets again factor sets (TauCeti.IsFactorSet.mul, TauCeti.IsFactorSet.inv);
• TauCeti.IsFactorSet.exists_eq_apply_mk: a factor set on a group G that is trivial whenever one of its arguments lies in a normal subgroup N is pulled back from a factor set on G ⧸ N;
• TauCeti.twistedMonoidAlgebra k G α: the twisted monoid algebra k_α[G];
• TauCeti.TwistedMonoidAlgebra.of: its basis elements, with the multiplication table TauCeti.TwistedMonoidAlgebra.of_mul_of, the basis TauCeti.TwistedMonoidAlgebra.basis, and the dimension count TauCeti.TwistedMonoidAlgebra.finrank_eq_natCard;
• TauCeti.TwistedMonoidAlgebra.lift: the universal property. A family u : G → A in a k-algebra A with u 1 = 1 and u g * u h = α g h • u (g * h) -- that is, a projective representation with factor set α -- extends uniquely to an algebra map k_α[G] →ₐ[k] A;
• TauCeti.TwistedMonoidAlgebra.monoidAlgebraEquiv: for the trivial factor set, k_α[G] is the monoid algebra MonoidAlgebra k G;
• TauCeti.TwistedMonoidAlgebra.equivOfCoboundary: two factor sets related by β g h * c (g * h) = α g h * (c g * c h) for some c : G → kˣ have isomorphic twisted monoid algebras. For a group G that relation is exactly the statement that α and β are cohomologous, so there k_α[G] depends up to isomorphism only on the class of α in H²(G, kˣ).

Implementation notes

IsFactorSet is a Prop-valued class on the raw function α, spelled out as the multiplicative 2-cocycle identity α (g * h) j * α g h = α h j * α g (h * j) together with the normalization α 1 g = α g 1 = 1, rather than as groupCohomology.IsMulCocycle₂ for the trivial action of G on kˣ: the twisted algebra wants α curried, and wants the normalization, which the cocycle identity alone gives only up to the constant α 1 1. Carrying the hypotheses in a class keeps the type twistedMonoidAlgebra k G α free of proof arguments.

α g h is the value of the factor set at the ordered pair (g, h). The multiplication e g * e h = (α g h : k) • e (g * h) follows the left-action convention used for projective representations.

Nothing in the construction uses inverses in G, so IsFactorSet, the twisted algebra, its basis, the universal property and the two comparison isomorphisms are all stated for a monoid G. A group is assumed only where an inverse appears, in TauCeti.IsFactorSet.apply_inv_eq_inv_apply and TauCeti.TwistedMonoidAlgebra.isUnit_of.

twistedMonoidAlgebra k G α is a Subalgebra k (Module.End k (G →₀ k)) rather than a fresh type carrying a hand-built ring structure on G →₀ k. The two are the same algebra: TauCeti.TwistedMonoidAlgebra.basis exhibits G as a basis and TauCeti.TwistedMonoidAlgebra.of_mul_of is the intended multiplication table, while TauCeti.TwistedMonoidAlgebra.lift and TauCeti.TwistedMonoidAlgebra.algHom_ext say it has the expected universal property.

References

• G. Karpilovsky, Projective Representations of Finite Groups, Marcel Dekker (1985), Ch. 3.

class TauCeti.IsFactorSet {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) : Prop

A normalized factor set on a monoid G with values in the units of a commutative semiring k: a function α : G → G → kˣ satisfying the multiplicative 2-cocycle identity and normalized at 1. For a group G these are exactly the factor sets arising from projective representations of G over k.

• cocycle (g h j : G) : α (g * h) j * α g h = α h j * α g (h * j)

  The multiplicative 2-cocycle identity, the associativity constraint of the twisted product.

• one_left (g : G) : α 1 g = 1

  Normalization on the left, half of the unitality of the twisted product.

• one_right (g : G) : α g 1 = 1

  Normalization on the right, half of the unitality of the twisted product.

instance TauCeti.IsFactorSet.instOfNatForallForallUnits {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] : IsFactorSet 1

The trivial factor set, whose twisted monoid algebra is the ordinary monoid algebra.

instance TauCeti.IsFactorSet.mul {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α β : G → G → kˣ) [IsFactorSet α] [IsFactorSet β] : IsFactorSet (α * β)

The pointwise product of two factor sets is a factor set. It is the factor set of a tensor product of projective representations (TauCeti.IsProjectiveRep.tensorProduct).

instance TauCeti.IsFactorSet.inv {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] : IsFactorSet α⁻¹

The pointwise inverse of a factor set is a factor set.

theorem TauCeti.IsFactorSet.apply_inv_eq_inv_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (α : G → G → kˣ) [IsFactorSet α] (g : G) : α g g⁻¹ = α g⁻¹ g

A factor set is symmetric on an inverse pair: it takes the same value at (g, g⁻¹) as at (g⁻¹, g). This is the cocycle identity at (g, g⁻¹, g), and it is the coherence making the twisted basis elements two-sided units.

theorem TauCeti.IsFactorSet.comp {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommSemiring k] [Monoid G] [Monoid H] (f : G →* H) (β : H → H → kˣ) [IsFactorSet β] : IsFactorSet fun (g₁ g₂ : G) => β (f g₁) (f g₂)

The pullback of a normalized factor set along a homomorphism f : G →* H is a normalized factor set.

theorem TauCeti.IsFactorSet.of_comp {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommSemiring k] [Monoid G] [Monoid H] {β : H → H → kˣ} (f : G →* H) (hf : Function.Surjective ⇑f) (h : IsFactorSet fun (g₁ g₂ : G) => β (f g₁) (f g₂)) : IsFactorSet β

A function on H whose pullback along a surjective homomorphism f : G →* H is a normalized factor set is itself a normalized factor set.

Descent to a quotient group

A factor set that is trivial whenever one of its arguments lies in a normal subgroup N is constant on the cosets of N in each argument, so it is pulled back from a factor set on G ⧸ N.

theorem TauCeti.IsFactorSet.apply_mul_right_of_mem {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {α : G → G → kˣ} [IsFactorSet α] {N : Subgroup G} (hr : ∀ (g n : G), n ∈ N → α g n = 1) (g h : G) {n : G} (hn : n ∈ N) : α g (h * n) = α g h

A factor set that is trivial whenever its second argument lies in N does not change when its second argument is multiplied on the right by an element of N.

theorem TauCeti.IsFactorSet.apply_mul_left_of_mem {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {α : G → G → kˣ} [IsFactorSet α] {N : Subgroup G} [N.Normal] (hr : ∀ (g n : G), n ∈ N → α g n = 1) (hl : ∀ (g n : G), n ∈ N → α n g = 1) (g h : G) {n : G} (hn : n ∈ N) : α (g * n) h = α g h

A factor set that is trivial whenever one of its arguments lies in the normal subgroup N does not change when its first argument is multiplied on the right by an element of N.

theorem TauCeti.IsFactorSet.exists_eq_apply_mk {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {α : G → G → kˣ} [IsFactorSet α] {N : Subgroup G} [N.Normal] (hr : ∀ (g n : G), n ∈ N → α g n = 1) (hl : ∀ (g n : G), n ∈ N → α n g = 1) : ∃ (β : G ⧸ N → G ⧸ N → kˣ), IsFactorSet β ∧ ∀ (g h : G), α g h = β ↑g ↑h

A factor set that is trivial whenever one of its arguments lies in the normal subgroup N is inflated from G ⧸ N: it is the pullback of a normalized factor set on the quotient.

noncomputable def TauCeti.twistedTranslation (k : Type u_1) {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) (g : G) : (G →₀ k) →ₗ[k] G →₀ k

The α-twisted translation by g on G →₀ k: it sends the basis vector at h to α g h times the basis vector at g * h. For the trivial factor set this is the regular representation of G on its monoid algebra.

Equations

• TauCeti.twistedTranslation k α g = (Finsupp.lsum k) fun (h : G) => ↑(α g h) • Finsupp.lsingle (g * h)

@[simp]

theorem TauCeti.twistedTranslation_single (k : Type u_1) {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) (g h : G) (b : k) : (twistedTranslation k α g) (Finsupp.single h b) = Finsupp.single (g * h) (↑(α g h) * b)

@[simp]

theorem TauCeti.twistedTranslation_one (k : Type u_1) {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] : twistedTranslation k α 1 = 1

theorem TauCeti.twistedTranslation_mul (k : Type u_1) {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] (g h : G) : twistedTranslation k α g * twistedTranslation k α h = ↑(α g h) • twistedTranslation k α (g * h)

The twisted composition law. The composite of two twisted translations is the twisted translation of the product, scaled by the factor set; this is the cocycle identity, restated.

theorem TauCeti.linearIndependent_twistedTranslation (k : Type u_1) {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] : LinearIndependent k (twistedTranslation k α)

The twisted translations are linearly independent: the translation by g is recovered from its value at the basis vector of 1, which is the basis vector of g.

noncomputable def TauCeti.twistedMonoidAlgebra (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] : Subalgebra k (Module.End k (G →₀ k))

The twisted monoid algebra k_α[G] of a factor set α, realized as the k-span of the twisted translations inside Module.End k (G →₀ k). It is a subalgebra because the cocycle identity makes the span closed under composition (TauCeti.twistedTranslation_mul) and the normalization puts the identity operator into it (TauCeti.twistedTranslation_one).

Equations

• TauCeti.twistedMonoidAlgebra k G α = (Submodule.span k (Set.range (TauCeti.twistedTranslation k α))).toSubalgebra ⋯ ⋯

@[simp]

theorem TauCeti.toSubmodule_twistedMonoidAlgebra (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] : Subalgebra.toSubmodule (twistedMonoidAlgebra k G α) = Submodule.span k (Set.range (twistedTranslation k α))

theorem TauCeti.twistedTranslation_mem_twistedMonoidAlgebra (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] (g : G) : twistedTranslation k α g ∈ twistedMonoidAlgebra k G α

The twisted translations lie in the twisted monoid algebra: they are its basis elements.

noncomputable def TauCeti.TwistedMonoidAlgebra.of {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] (g : G) : ↥(twistedMonoidAlgebra k G α)

The basis element of k_α[G] at g : G, namely the α-twisted translation by g.

Equations

• TauCeti.TwistedMonoidAlgebra.of g = ⟨TauCeti.twistedTranslation k α g, ⋯⟩

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.coe_of {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] (g : G) : ↑(of g) = twistedTranslation k α g

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.of_one {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] : of 1 = 1

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.of_mul_of {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] (g h : G) : of g * of h = ↑(α g h) • of (g * h)

The multiplication table of the twisted monoid algebra: e g * e h = α g h • e (g * h).

theorem TauCeti.TwistedMonoidAlgebra.isUnit_of {k : Type u_3} {G : Type u_4} [CommSemiring k] [Group G] {α : G → G → kˣ} [IsFactorSet α] (g : G) : IsUnit (of g)

The basis elements are units, with (α g g⁻¹)⁻¹ • e g⁻¹ as a two-sided inverse.

noncomputable def TauCeti.TwistedMonoidAlgebra.basis (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] : Module.Basis G k ↥(twistedMonoidAlgebra k G α)

The twisted translations form a basis of k_α[G] indexed by G: the twisted monoid algebra is free with basis the elements TauCeti.TwistedMonoidAlgebra.of.

Equations

• TauCeti.TwistedMonoidAlgebra.basis k G α = Module.Basis.span ⋯

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.basis_apply (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] (g : G) : (basis k G α) g = of g

instance TauCeti.TwistedMonoidAlgebra.instFreeSubtypeEndFinsuppMemSubalgebraTwistedMonoidAlgebra (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] : Module.Free k ↥(twistedMonoidAlgebra k G α)

theorem TauCeti.TwistedMonoidAlgebra.finrank_eq_natCard (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] [StrongRankCondition k] : Module.finrank k ↥(twistedMonoidAlgebra k G α) = Nat.card G

The twisted monoid algebra has dimension #G, as the ordinary monoid algebra does. For an infinite G both sides are 0.

theorem TauCeti.TwistedMonoidAlgebra.algHom_ext {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] {A : Type u_3} [Semiring A] [Algebra k A] {f g : ↥(twistedMonoidAlgebra k G α) →ₐ[k] A} (h : ∀ (x : G), f (of x) = g (of x)) : f = g

An algebra map out of k_α[G] is determined by its values on the basis elements.

theorem TauCeti.TwistedMonoidAlgebra.algHom_ext_iff {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] {A : Type u_3} [Semiring A] [Algebra k A] {f g : ↥(twistedMonoidAlgebra k G α) →ₐ[k] A} : f = g ↔ ∀ (x : G), f (of x) = g (of x)

theorem TauCeti.TwistedMonoidAlgebra.constr_of {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] {A : Type u_3} [AddCommMonoid A] [Module k A] (u : G → A) (g : G) : (((basis k G α).constr k) u) (of g) = u g

The linear extension of a family u : G → A along the basis takes the value u g at the basis element TauCeti.TwistedMonoidAlgebra.of g.

noncomputable def TauCeti.TwistedMonoidAlgebra.lift {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] {A : Type u_3} [Semiring A] [Algebra k A] (u : G → A) (hu₁ : u 1 = 1) (hu : ∀ (g h : G), u g * u h = ↑(α g h) • u (g * h)) : ↥(twistedMonoidAlgebra k G α) →ₐ[k] A

The universal property of the twisted monoid algebra. A projective representation of G with factor set α in a k-algebra A -- a family u : G → A with u 1 = 1 and u g * u h = α g h • u (g * h) -- extends to an algebra map k_α[G] →ₐ[k] A. Uniqueness is TauCeti.TwistedMonoidAlgebra.algHom_ext.

Equations

• TauCeti.TwistedMonoidAlgebra.lift u hu₁ hu = AlgHom.ofLinearMap (((TauCeti.TwistedMonoidAlgebra.basis k G α).constr k) u) ⋯ ⋯

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.lift_of {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : G → G → kˣ} [IsFactorSet α] {A : Type u_3} [Semiring A] [Algebra k A] (u : G → A) (hu₁ : u 1 = 1) (hu : ∀ (g h : G), u g * u h = ↑(α g h) • u (g * h)) (g : G) : (lift u hu₁ hu) (of g) = u g

noncomputable def TauCeti.TwistedMonoidAlgebra.toMonoidAlgebra (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] : ↥(twistedMonoidAlgebra k G 1) →ₐ[k] MonoidAlgebra k G

For the trivial factor set the basis elements multiply exactly as the group elements do, so they assemble into an algebra map to the monoid algebra.

Equations

• TauCeti.TwistedMonoidAlgebra.toMonoidAlgebra k G = TauCeti.TwistedMonoidAlgebra.lift (fun (g : G) => MonoidAlgebra.single g 1) ⋯ ⋯

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.toMonoidAlgebra_of (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (g : G) : (toMonoidAlgebra k G) (of g) = MonoidAlgebra.single g 1

noncomputable def TauCeti.TwistedMonoidAlgebra.fromMonoidAlgebra (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] : MonoidAlgebra k G →ₐ[k] ↥(twistedMonoidAlgebra k G 1)

For the trivial factor set the basis elements form a copy of G inside k_1[G], giving an algebra map from the monoid algebra by its universal property.

Equations

• TauCeti.TwistedMonoidAlgebra.fromMonoidAlgebra k G = (MonoidAlgebra.lift k (↥(TauCeti.twistedMonoidAlgebra k G 1)) G) { toFun := TauCeti.TwistedMonoidAlgebra.of, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.fromMonoidAlgebra_single (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (g : G) : (fromMonoidAlgebra k G) (MonoidAlgebra.single g 1) = of g

noncomputable def TauCeti.TwistedMonoidAlgebra.monoidAlgebraEquiv (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] : ↥(twistedMonoidAlgebra k G 1) ≃ₐ[k] MonoidAlgebra k G

The twisted monoid algebra of the trivial factor set is the monoid algebra.

Equations

• TauCeti.TwistedMonoidAlgebra.monoidAlgebraEquiv k G = AlgEquiv.ofAlgHom (TauCeti.TwistedMonoidAlgebra.toMonoidAlgebra k G) (TauCeti.TwistedMonoidAlgebra.fromMonoidAlgebra k G) ⋯ ⋯

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.monoidAlgebraEquiv_of (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (g : G) : (monoidAlgebraEquiv k G) (of g) = MonoidAlgebra.single g 1

theorem TauCeti.TwistedMonoidAlgebra.eq_one_of_coboundary {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] (β : G → G → kˣ) [IsFactorSet β] (c : G → kˣ) (hc : ∀ (g h : G), β g h * c (g * h) = α g h * (c g * c h)) : c 1 = 1

A function exhibiting two factor sets as differing by a coboundary is automatically normalized at 1.

noncomputable def TauCeti.TwistedMonoidAlgebra.homOfCoboundary {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] (β : G → G → kˣ) [IsFactorSet β] (c : G → kˣ) (hc : ∀ (g h : G), β g h * c (g * h) = α g h * (c g * c h)) : ↥(twistedMonoidAlgebra k G β) →ₐ[k] ↥(twistedMonoidAlgebra k G α)

Rescaling the basis elements by c carries the multiplication table of β to that of α, giving an algebra map k_β[G] →ₐ[k] k_α[G].

Equations

• TauCeti.TwistedMonoidAlgebra.homOfCoboundary α β c hc = TauCeti.TwistedMonoidAlgebra.lift (fun (g : G) => ↑(c g) • TauCeti.TwistedMonoidAlgebra.of g) ⋯ ⋯

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.homOfCoboundary_of {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] (β : G → G → kˣ) [IsFactorSet β] (c : G → kˣ) (hc : ∀ (g h : G), β g h * c (g * h) = α g h * (c g * c h)) (g : G) : (homOfCoboundary α β c hc) (of g) = ↑(c g) • of g

theorem TauCeti.TwistedMonoidAlgebra.coboundary_inv {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α β : G → G → kˣ) (c : G → kˣ) (hc : ∀ (g h : G), β g h * c (g * h) = α g h * (c g * c h)) (g h : G) : α g h * (c (g * h))⁻¹ = β g h * ((c g)⁻¹ * (c h)⁻¹)

The inverse rescaling witnesses the same coboundary relation with the two factor sets exchanged; this is what makes TauCeti.TwistedMonoidAlgebra.homOfCoboundary invertible.

noncomputable def TauCeti.TwistedMonoidAlgebra.equivOfCoboundary {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] (β : G → G → kˣ) [IsFactorSet β] (c : G → kˣ) (hc : ∀ (g h : G), β g h * c (g * h) = α g h * (c g * c h)) : ↥(twistedMonoidAlgebra k G β) ≃ₐ[k] ↥(twistedMonoidAlgebra k G α)

Factor sets differing by a coboundary have isomorphic twisted monoid algebras. The isomorphism rescales the basis element at g by c g. When G is a group, the hypothesis says exactly that α and β are cohomologous, so there k_α[G] depends up to isomorphism only on the class of α in H²(G, kˣ).

Equations

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

@[simp]

theorem TauCeti.TwistedMonoidAlgebra.equivOfCoboundary_of {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (α : G → G → kˣ) [IsFactorSet α] (β : G → G → kˣ) [IsFactorSet β] (c : G → kˣ) (hc : ∀ (g h : G), β g h * c (g * h) = α g h * (c g * c h)) (g : G) : (equivOfCoboundary α β c hc) (of g) = ↑(c g) • of g