def Cochain1 (G : Type u) (A : Type v) : Type (max u v)

A 1-cochain on the group G with values in the commutative group A: a function G → A.

def Cochain2 (G : Type u) (A : Type v) : Type (max u v)

A 2-cochain on the group G with values in the commutative group A: a function G × G → A.

def Cochain3' (G : Type u) (A : Type v) : Type (max u v)

A 3-cochain on the group G with values in the commutative group A: a function G × G × G → A.

def Cochain4 (G : Type u) (A : Type v) : Type (max u v)

A 4-cochain on the group G with values in the commutative group A: a function G⁴ → A.

def d1 (G : Type u) [Group G] (A : Type v) [CommGroup A] (η : Cochain1 G A) : Cochain2 G A

The group coboundary d¹η(g, h) = η(g) η(h) η(gh)⁻¹ sending a 1-cochain to a 2-cochain.

def d2 (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ : Cochain2 G A) : Cochain3' G A

The group coboundary d²μ(g, h, l) = μ(h,l) μ(g, hl) μ(gh, l)⁻¹ μ(g, h)⁻¹ sending a 2-cochain to a 3-cochain.

def d3 (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω : Cochain3' G A) : Cochain4 G A

The group coboundary d³ω sending a 3-cochain to a 4-cochain.

theorem prod5_eq_one_iff {A : Type u_1} [CommGroup A] {a b c d e : A} : a * b * c * d⁻¹ * e⁻¹ = 1 ↔ e * d = a * b * c

Rearrangement lemma: a * b * c * d⁻¹ * e⁻¹ = 1 is equivalent to e * d = a * b * c in a commutative group.

theorem prod4_eq_one_iff {A : Type u_1} [CommGroup A] {a b c d : A} : a * b * c⁻¹ * d⁻¹ = 1 ↔ d * c = a * b

Rearrangement lemma: a * b * c⁻¹ * d⁻¹ = 1 is equivalent to d * c = a * b in a commutative group.

theorem comm_group_rearrange {A : Type u_1} [CommGroup A] {x a b c d : A} : x * (a * b * c⁻¹ * d⁻¹) * d * c = x * a * b

Rearrangement lemma in a commutative group: x * (a * b * c⁻¹ * d⁻¹) * d * c = x * a * b.

theorem d2_comp_d1 (G : Type u) [Group G] (A : Type v) [CommGroup A] (η : Cochain1 G A) (g h l : G) : d2 G A (d1 G A η) g h l = 1

The cochain identity d² ∘ d¹ = 0: applying d² to a coboundary d¹η yields the trivial 3-cochain.

theorem d1_inv (G : Type u) [Group G] (A : Type v) [CommGroup A] (η : Cochain1 G A) (g h : G) : d1 G A (fun (x : G) => (η x)⁻¹) g h = (d1 G A η g h)⁻¹

d¹ of the pointwise inverse of a 1-cochain is the pointwise inverse of d¹.

theorem d2_inv (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ : Cochain2 G A) (g h l : G) : d2 G A (fun (x y : G) => (μ x y)⁻¹) g h l = (d2 G A μ g h l)⁻¹

d² of the pointwise inverse of a 2-cochain is the pointwise inverse of d².

def IsCocycle2 (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ : Cochain2 G A) : Prop

A 2-cochain is a 2-cocycle if its coboundary d²μ vanishes identically.

def IsCoboundary2 (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ : Cochain2 G A) : Prop

A 2-cochain is a 2-coboundary if it equals d¹η for some 1-cochain η.

def IsCocycle3 (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω : Cochain3' G A) : Prop

A 3-cochain is a 3-cocycle if its coboundary d³ω vanishes identically.

def IsCoboundary3 (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω : Cochain3' G A) : Prop

A 3-cochain is a 3-coboundary if it equals d²μ for some 2-cochain μ.

theorem isCocycle3_iff_cocycleCond (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω : Cochain3' G A) : IsCocycle3 G A ω ↔ ∀ (g₁ g₂ g₃ g₄ : G), ω (g₁ * g₂) g₃ g₄ * ω g₁ g₂ (g₃ * g₄) = ω g₁ g₂ g₃ * ω g₁ (g₂ * g₃) g₄ * ω g₂ g₃ g₄

Reformulation of the 3-cocycle condition in the form used to define monoidal associativity: ω(g₁g₂, g₃, g₄) ω(g₁, g₂, g₃g₄) = ω(g₁, g₂, g₃) ω(g₁, g₂g₃, g₄) ω(g₂, g₃, g₄).

theorem isCocycle2_iff_assoc (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ : Cochain2 G A) : IsCocycle2 G A μ ↔ ∀ (g h l : G), μ g h * μ (g * h) l = μ h l * μ g (h * l)

Reformulation of the 2-cocycle condition: μ(g, h) μ(gh, l) = μ(h, l) μ(g, hl).

def Cohomologous2 (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ₁ μ₂ : Cochain2 G A) : Prop

Two 2-cochains are cohomologous if they differ by a coboundary d¹η.

def Cohomologous3 (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω₁ ω₂ : Cochain3' G A) : Prop

Two 3-cochains are cohomologous if they differ by a coboundary d²μ.

def cohomologous2Setoid (G : Type u) [Group G] (A : Type v) [CommGroup A] : Setoid (Cochain2 G A)

The equivalence relation on 2-cochains given by being cohomologous, packaged as a Setoid.

def cohomologous3Setoid (G : Type u) [Group G] (A : Type v) [CommGroup A] : Setoid (Cochain3' G A)

The equivalence relation on 3-cochains given by being cohomologous, packaged as a Setoid.

def H2 (G : Type u) [Group G] (A : Type v) [CommGroup A] : Type (max u v)

The second group cohomology H²(G, A) realised as the quotient of 2-cochains by the cohomologous relation.

def H3 (G : Type u) [Group G] (A : Type v) [CommGroup A] : Type (max u v)

The third group cohomology H³(G, A) realised as the quotient of 3-cochains by the cohomologous relation.

def pullback3 (G₁ : Type u) [Group G₁] (G₂ : Type u) [Group G₂] (A : Type v) (f : G₁ →* G₂) (ω : Cochain3' G₂ A) : Cochain3' G₁ A

The pullback of a 3-cochain on G₂ along a group homomorphism f : G₁ →* G₂.

def IsMonoidalFunctorData (G₁ : Type u) [Group G₁] (G₂ : Type u) [Group G₂] (A : Type v) [CommGroup A] (ω₁ : Cochain3' G₁ A) (ω₂ : Cochain3' G₂ A) (f : G₁ →* G₂) (μ : Cochain2 G₁ A) : Prop

The compatibility condition relating the 2-cochain data μ of a monoidal functor to the source and target 3-cocycles, expressing the hexagon-type axiom of EGNO §1.7.

theorem isMonoidalFunctorData_iff_pullback (G₁ : Type u) [Group G₁] (G₂ : Type u) [Group G₂] (A : Type v) [CommGroup A] (ω₁ : Cochain3' G₁ A) (ω₂ : Cochain3' G₂ A) (f : G₁ →* G₂) (μ : Cochain2 G₁ A) : IsMonoidalFunctorData G₁ G₂ A ω₁ ω₂ f μ ↔ ∀ (g h l : G₁), pullback3 G₁ G₂ A f ω₂ g h l = ω₁ g h l * d2 G₁ A μ g h l

Equivalent reformulation: μ witnesses that the pullback of ω₂ along f and the 3-cocycle ω₁ are cohomologous via d²μ.

theorem monoidalFunctor_exists_iff_cohomologous (G₁ : Type u) [Group G₁] (G₂ : Type u) [Group G₂] (A : Type v) [CommGroup A] (ω₁ : Cochain3' G₁ A) (ω₂ : Cochain3' G₂ A) (f : G₁ →* G₂) : (∃ (μ : Cochain2 G₁ A), IsMonoidalFunctorData G₁ G₂ A ω₁ ω₂ f μ) ↔ Cohomologous3 G₁ A ω₁ (pullback3 G₁ G₂ A f ω₂)

A monoidal functor (G₁, ω₁) → (G₂, ω₂) with underlying group homomorphism f exists if and only if ω₁ and the pullback of ω₂ are cohomologous.

def IsMonoidalNatTransData (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) (η : Cochain1 G A) : Prop

The compatibility condition η(g) η(h) μ(g,h) = μ'(g,h) η(gh) on a 1-cochain η relating two 2-cochains μ and μ'; this is the condition that η is a monoidal natural transformation between the corresponding monoidal structures.

theorem isMonoidalNatTransData_iff_coboundary (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) (η : Cochain1 G A) : IsMonoidalNatTransData G A μ μ' η ↔ ∀ (g h : G), μ' g h = μ g h * d1 G A η g h

The compatibility condition for η is equivalent to μ' being μ shifted by d¹η.

theorem monoidalNatTrans_iff_cohomologous2 (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) : (∃ (η : Cochain1 G A), IsMonoidalNatTransData G A μ μ' η) ↔ Cohomologous2 G A μ μ'

A monoidal natural transformation between the monoidal structures on Vec_G defined by μ and μ' exists if and only if μ and μ' are cohomologous as 2-cochains.

def IsMonoidalNatIso (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) (η : Cochain1 G A) : Prop

A monoidal natural isomorphism is monoidal natural transformation data η together with a pointwise inverse 1-cochain η_inv.

theorem isMonoidalNatIso_of_isMonoidalNatTransData (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) (η : Cochain1 G A) (h : IsMonoidalNatTransData G A μ μ' η) : IsMonoidalNatIso G A μ μ' η

Any monoidal natural transformation data η is automatically a monoidal natural isomorphism, since values in a commutative group are always invertible.

theorem monoidal_iso_iff_cohomologous2 (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) : (∃ (η : Cochain1 G A), IsMonoidalNatIso G A μ μ' η) ↔ Cohomologous2 G A μ μ'

A monoidal natural isomorphism between the monoidal structures defined by μ and μ' exists if and only if μ and μ' are cohomologous.

theorem monoidal_autoequiv_classes_H2 (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ₁ μ₂ : Cochain2 G A) : (∃ (η : Cochain1 G A), ∀ (g h : G), μ₂ g h = μ₁ g h * d1 G A η g h) ↔ ⟦μ₁⟧ = ⟦μ₂⟧

The classes of monoidal auto-equivalences with the same underlying monoidal structure are classified by H²(G, A).

theorem pullback3_id (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω : Cochain3' G A) : pullback3 G G A (MonoidHom.id G) ω = ω

Pullback along the identity homomorphism leaves a 3-cochain unchanged.

theorem monoidal_equiv_iff_cohomologous3 (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω₁ ω₂ : Cochain3' G A) : (∃ (μ : Cochain2 G A), IsMonoidalFunctorData G G A ω₁ ω₂ (MonoidHom.id G) μ) ↔ Cohomologous3 G A ω₁ ω₂

A monoidal equivalence (over the identity homomorphism) between (G, ω₁) and (G, ω₂) exists if and only if ω₁ and ω₂ are cohomologous as 3-cochains.

theorem monoidal_structure_parametrized_by_H3 (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω₁ ω₂ : Cochain3' G A) : (∃ (μ : Cochain2 G A), IsMonoidalFunctorData G G A ω₁ ω₂ (MonoidHom.id G) μ) ↔ ⟦ω₁⟧ = ⟦ω₂⟧

Monoidal structures on the category of G-graded vector spaces with values in A are parametrized by H³(G, A).

def groupCocycle3_of_isCocycle3 {G : Type u} [Group G] {A : Type v} [CommGroup A] (ω : Cochain3' G A) (h : IsCocycle3 G A ω) : GroupCocycle3 G A

Repackage a 3-cocycle as a GroupCocycle3, the structure consumed by the GradedVec machinery to produce a monoidal structure on graded vector spaces.

theorem isMonoidalFunctorData_id (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω : Cochain3' G A) : IsMonoidalFunctorData G G A ω ω (MonoidHom.id G) fun (x x_1 : G) => 1

The identity homomorphism together with the trivial 2-cochain provides identity monoidal functor data on (G, ω).

def compCochain2 {G₁ G₂ : Type u} [Group G₁] [Group G₂] {A : Type v} [CommGroup A] (f₁ : G₁ →* G₂) (μ₁ : Cochain2 G₁ A) (μ₂ : Cochain2 G₂ A) : Cochain2 G₁ A

Composition of 2-cochains along a group homomorphism f₁ : G₁ →* G₂: the 2-cochain μ₂(f₁ g, f₁ h) * μ₁(g, h) on G₁.

theorem isMonoidalFunctorData_comp {G₁ G₂ G₃ : Type u} [Group G₁] [Group G₂] [Group G₃] {A : Type v} [CommGroup A] {ω₁ : Cochain3' G₁ A} {ω₂ : Cochain3' G₂ A} {ω₃ : Cochain3' G₃ A} {f₁ : G₁ →* G₂} {f₂ : G₂ →* G₃} {μ₁ : Cochain2 G₁ A} {μ₂ : Cochain2 G₂ A} (h₁ : IsMonoidalFunctorData G₁ G₂ A ω₁ ω₂ f₁ μ₁) (h₂ : IsMonoidalFunctorData G₂ G₃ A ω₂ ω₃ f₂ μ₂) : IsMonoidalFunctorData G₁ G₃ A ω₁ ω₃ (f₂.comp f₁) (compCochain2 f₁ μ₁ μ₂)

Composition of monoidal functor data: composing the underlying group homomorphisms together with compCochain2 yields monoidal functor data for the composite.

structure MonoidalFunctorCocycleData (G₁ G₂ : Type u) [Group G₁] [Group G₂] (A : Type v) [CommGroup A] (ω₁ : Cochain3' G₁ A) (ω₂ : Cochain3' G₂ A) : Type (max u v)

Bundled data of a monoidal functor from (G₁, ω₁) to (G₂, ω₂): a group homomorphism f, a 2-cochain μ, and the monoidal compatibility condition.

• f : G₁ →* G₂
• μ : Cochain2 G₁ A
• isMonoidal : IsMonoidalFunctorData G₁ G₂ A ω₁ ω₂ self.f self.μ

def MonoidalFunctorCocycleData.id (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω : Cochain3' G A) : MonoidalFunctorCocycleData G G A ω ω

The identity monoidal functor on (G, ω).

def MonoidalFunctorCocycleData.comp {G₁ G₂ G₃ : Type u} [Group G₁] [Group G₂] [Group G₃] {A : Type v} [CommGroup A] {ω₁ : Cochain3' G₁ A} {ω₂ : Cochain3' G₂ A} {ω₃ : Cochain3' G₃ A} (D₁ : MonoidalFunctorCocycleData G₁ G₂ A ω₁ ω₂) (D₂ : MonoidalFunctorCocycleData G₂ G₃ A ω₂ ω₃) : MonoidalFunctorCocycleData G₁ G₃ A ω₁ ω₃

Composition of monoidal functor cocycle data.

theorem Proposition_1_7_1_i (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) : (∃ (η : Cochain1 G A), IsMonoidalNatTransData G A μ μ' η) ↔ Cohomologous2 G A μ μ'

EGNO Proposition 1.7.1 (i): monoidal natural transformations between the monoidal structures defined by μ and μ' exist iff μ and μ' are cohomologous as 2-cochains.

theorem Proposition_1_7_1_ii (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) : (∃ (η : Cochain1 G A), IsMonoidalNatIso G A μ μ' η) ↔ Cohomologous2 G A μ μ'

EGNO Proposition 1.7.1 (ii): monoidal natural isomorphisms exist iff μ and μ' are cohomologous as 2-cochains.

theorem Proposition_1_7_1_iii (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω₁ ω₂ : Cochain3' G A) : (∃ (μ : Cochain2 G A), IsMonoidalFunctorData G G A ω₁ ω₂ (MonoidHom.id G) μ) ↔ ⟦ω₁⟧ = ⟦ω₂⟧

EGNO Proposition 1.7.1 (iii): equivalence classes of monoidal structures on Vec_G^A under monoidal equivalence are in bijection with H³(G, A).