structure GroupCocycle3 (G : Type u) [Monoid G] (A : Type v) [CommMonoid A] : Type (max u v)

A 3-cocycle on a monoid G with values in a commutative monoid A: a function ω : G × G × G → A satisfying the cocycle identity used to twist the associator of the pointed monoidal category Vec_G^ω.

• toFun : G → G → G → A
• cocycle_cond (g₁ g₂ g₃ g₄ : G) : self.toFun (g₁ * g₂) g₃ g₄ * self.toFun g₁ g₂ (g₃ * g₄) = self.toFun g₁ g₂ g₃ * self.toFun g₁ (g₂ * g₃) g₄ * self.toFun g₂ g₃ g₄

@[implicit_reducible]

instance instCoeFunGroupCocycle3ForallForallForall {G : Type u} [Monoid G] {A : Type v} [CommMonoid A] : CoeFun (GroupCocycle3 G A) fun (x : GroupCocycle3 G A) => G → G → G → A

Coerce a GroupCocycle3 to its underlying function G → G → G → A.

theorem GroupCocycle3.ext {G : Type u} [Monoid G] {A : Type v} [CommMonoid A] {ω₁ ω₂ : GroupCocycle3 G A} (h : ω₁.toFun = ω₂.toFun) : ω₁ = ω₂

Extensionality for 3-cocycles: equality of toFun implies equality.

theorem GroupCocycle3.ext_iff {G : Type u} [Monoid G] {A : Type v} [CommMonoid A] {ω₁ ω₂ : GroupCocycle3 G A} : ω₁ = ω₂ ↔ ω₁.toFun = ω₂.toFun

structure NormalizedGroupCocycle3 (G : Type u) [Monoid G] (A : Type v) [CommMonoid A] extends GroupCocycle3 G A : Type (max u v)

A normalised 3-cocycle: a GroupCocycle3 satisfying ω(g, 1, h) = 1 for all g, h ∈ G.

• toFun : G → G → G → A
• cocycle_cond (g₁ g₂ g₃ g₄ : G) : self.toFun (g₁ * g₂) g₃ g₄ * self.toFun g₁ g₂ (g₃ * g₄) = self.toFun g₁ g₂ g₃ * self.toFun g₁ (g₂ * g₃) g₄ * self.toFun g₂ g₃ g₄
• normalized (g h : G) : self.toFun g 1 h = 1

def GroupCocycle3.trivial (G : Type u) [Monoid G] (A : Type v) [CommMonoid A] : GroupCocycle3 G A

The trivial 3-cocycle, constantly equal to 1.

def NormalizedGroupCocycle3.trivial (G : Type u) [Monoid G] (A : Type v) [CommMonoid A] : NormalizedGroupCocycle3 G A

The trivial normalised 3-cocycle, constantly equal to 1.

structure CG (G : Type u) (A : Type v) [Monoid G] [CommGroup A] (_ω : NormalizedGroupCocycle3 G A) : Type u

Objects of the twisted pointed monoidal category Vec_G^ω: a single homogeneous component indexed by an element val : G.

• val : G

theorem CG.ext_iff {G : Type u} {A : Type v} {inst✝ : Monoid G} {inst✝¹ : CommGroup A} {_ω : NormalizedGroupCocycle3 G A} {x y : CG G A _ω} : x = y ↔ x.val = y.val

theorem CG.ext {G : Type u} {A : Type v} {inst✝ : Monoid G} {inst✝¹ : CommGroup A} {_ω : NormalizedGroupCocycle3 G A} {x y : CG G A _ω} (val : x.val = y.val) : x = y

structure CG.Hom {G : Type u} {A : Type v} [Monoid G] [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X Y : CG G A ω) : Type v

A morphism X ⟶ Y in Vec_G^ω exists only when X.val = Y.val, and is the data of a single nonzero scalar val : A.

• val : A
• eq : X.val = Y.val

theorem CG.Hom.ext {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} {X Y : CG G A ω} {f f' : X.Hom Y} (hv : f.val = f'.val) : f = f'

Extensionality for CG.Hom: morphisms are determined by their underlying scalar val.

theorem CG.Hom.ext_iff {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} {X Y : CG G A ω} {f f' : X.Hom Y} : f = f' ↔ f.val = f'.val

@[implicit_reducible]

instance CG.instCategory {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} : CategoryTheory.Category.{v, u} (CG G A ω)

Category instance on CG G A ω: composition multiplies the underlying scalars and identity morphisms have scalar 1.

@[simp]

theorem CG.comp_val {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} {X Y Z : CG G A ω} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).val = f.val * g.val

Underlying scalar of the composition of morphisms in CG G A ω.

@[simp]

theorem CG.id_val {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : (CategoryTheory.CategoryStruct.id X).val = 1

The underlying scalar of the identity morphism is 1.

@[reducible, inline]

abbrev CG.tensorObj' {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X Y : CG G A ω) : CG G A ω

Tensor product of objects in CG G A ω: degrees multiply.

@[reducible, inline]

abbrev CG.tensorHom' {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} {X₁ X₂ Y₁ Y₂ : CG G A ω} (f : X₁ ⟶ X₂) (f' : Y₁ ⟶ Y₂) : X₁.tensorObj' Y₁ ⟶ X₂.tensorObj' Y₂

Tensor product of morphisms in CG G A ω: scalars multiply.

@[reducible, inline]

abbrev CG.unit' {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} : CG G A ω

The monoidal unit object in CG G A ω lives in degree 1.

def CG.twistedAssociator' {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X Y Z : CG G A ω) : (X.tensorObj' Y).tensorObj' Z ≅ X.tensorObj' (Y.tensorObj' Z)

The associator in the twisted category CG G A ω, with structure constant ω(X.val, Y.val, Z.val) on each component.

@[simp]

theorem CG.twistedAssociator'_hom_val {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X Y Z : CG G A ω) : (X.twistedAssociator' Y Z).hom.val = ω.toFun X.val Y.val Z.val

The forward scalar of the twisted associator is ω(X, Y, Z).

@[simp]

theorem CG.twistedAssociator'_inv_val {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X Y Z : CG G A ω) : (X.twistedAssociator' Y Z).inv.val = (ω.toFun X.val Y.val Z.val)⁻¹

The inverse scalar of the twisted associator is ω(X, Y, Z)⁻¹.

def CG.leftUnitor' {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : unit'.tensorObj' X ≅ X

Left unit isomorphism 1 ⊗ X ≅ X in CG G A ω.

@[simp]

theorem CG.leftUnitor'_hom_val {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : X.leftUnitor'.hom.val = 1

The underlying scalar of the left unitor in CG G A ω is 1.

def CG.rightUnitor' {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : X.tensorObj' unit' ≅ X

Right unit isomorphism X ⊗ 1 ≅ X in CG G A ω.

@[simp]

theorem CG.rightUnitor'_hom_val {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : X.rightUnitor'.hom.val = 1

The underlying scalar of the right unitor in CG G A ω is 1.

@[implicit_reducible]

instance CG.monoidalCategoryStruct {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} : CategoryTheory.MonoidalCategoryStruct (CG G A ω)

Monoidal-category structure data on CG G A ω: tensor product, unit, associator, and unitors as defined above.

@[implicit_reducible]

instance CG.monoidalCategory {G : Type u} [Monoid G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} : CategoryTheory.MonoidalCategory (CG G A ω)

CG G A ω is a monoidal category: the pentagon axiom follows from the cocycle identity of ω and the triangle axiom from normalisation. This is the construction of Vec_G^ω (EGNO §1.7).

def CG.dualObj {G : Type u} [Group G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : CG G A ω

Dual object of X = ⟨g⟩ in CG G A ω, namely ⟨g⁻¹⟩.

theorem NormalizedGroupCocycle3.normalized_right {G : Type u} [Group G] {A : Type v} [CommGroup A] (ω : NormalizedGroupCocycle3 G A) (g h : G) : ω.toFun g h 1 = 1

A normalised 3-cocycle is also normalised in the rightmost slot: ω(g, h, 1) = 1.

theorem NormalizedGroupCocycle3.normalized_left {G : Type u} [Group G] {A : Type v} [CommGroup A] (ω : NormalizedGroupCocycle3 G A) (g h : G) : ω.toFun 1 g h = 1

A normalised 3-cocycle is also normalised in the leftmost slot: ω(1, g, h) = 1.

theorem NormalizedGroupCocycle3.cocycle_inv_cancel {G : Type u} [Group G] {A : Type v} [CommGroup A] (ω : NormalizedGroupCocycle3 G A) (g : G) : ω.toFun g g⁻¹ g * ω.toFun g⁻¹ g g⁻¹ = 1

Specialised cocycle identity used in the rigidity proof: ω(g, g⁻¹, g) · ω(g⁻¹, g, g⁻¹) = 1.

def CG.evalMorphism {G : Type u} [Group G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : X.dualObj.tensorObj' X ⟶ unit'

The evaluation morphism Xᘁ ⊗ X ⟶ 𝟙 in CG G A ω, given by the scalar ω(g, g⁻¹, g)⁻¹ where g = X.val.

def CG.coevMorphism {G : Type u} [Group G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : unit' ⟶ X.tensorObj' X.dualObj

The coevaluation morphism 𝟙 ⟶ X ⊗ Xᘁ in CG G A ω, given by the scalar 1.

@[implicit_reducible]

noncomputable instance CG.exactPairing {G : Type u} [Group G] {A : Type v} [CommGroup A] {ω : NormalizedGroupCocycle3 G A} (X : CG G A ω) : CategoryTheory.ExactPairing X X.dualObj

Each object X of CG G A ω has an exact pairing with its dual Xᘁ = ⟨g⁻¹⟩, exhibiting CG G A ω as a rigid monoidal category.