theorem monoidalNatTransData_mul_character {G : Type u} [Group G] {A : Type v} [CommGroup A] {μ μ' : Cochain2 G A} {η : Cochain1 G A} (hη : IsMonoidalNatTransData G A μ μ' η) (χ : G →* A) : IsMonoidalNatTransData G A μ μ' fun (g : G) => χ g * η g

Twisting a monoidal natural transformation η by a character χ : G →* A yields another monoidal natural transformation between the same monoidal structures.

theorem monoidalNatTrans_ratio_is_character {G : Type u} [Group G] {A : Type v} [CommGroup A] {μ μ' : Cochain2 G A} {η η' : Cochain1 G A} (hη : IsMonoidalNatTransData G A μ μ' η) (hη' : IsMonoidalNatTransData G A μ μ' η') : ∃ (χ : G →* A), ∀ (g : G), η' g = χ g * η g

The ratio of two monoidal natural transformations between the same monoidal structures is a group character G →* A.

theorem Proposition_1_7_1_i_torsor {G₁ : Type u} [Group G₁] {A : Type v} [CommGroup A] (μ μ' : Cochain2 G₁ A) : ((∃ (η : Cochain1 G₁ A), IsMonoidalNatTransData G₁ A μ μ' η) ↔ Cohomologous2 G₁ A μ μ') ∧ (∀ {η η' : Cochain1 G₁ A}, IsMonoidalNatTransData G₁ A μ μ' η → IsMonoidalNatTransData G₁ A μ μ' η' → ∃ (χ : G₁ →* A), ∀ (g : G₁), η' g = χ g * η g) ∧ ∀ {η : Cochain1 G₁ A}, IsMonoidalNatTransData G₁ A μ μ' η → ∀ (χ : G₁ →* A), IsMonoidalNatTransData G₁ A μ μ' fun (g : G₁) => χ g * η g

EGNO Proposition 1.7.1 (i) (torsor refinement): existence of a monoidal natural transformation between graded vector spaces is equivalent to Cohomologous2, and the set of such transformations forms a torsor under the group of characters G →* A.

theorem Proposition_1_7_1_ii_torsor (G : Type u) [Group G] (A : Type v) [CommGroup A] (μ μ' : Cochain2 G A) : ((∃ (η : Cochain1 G A), IsMonoidalNatIso G A μ μ' η) ↔ Cohomologous2 G A μ μ') ∧ ((∃ (η : Cochain1 G A), ∀ (g h : G), μ' g h = μ g h * d1 G A η g h) ↔ ⟦μ⟧ = ⟦μ'⟧)

EGNO Proposition 1.7.1 (ii) (torsor refinement): existence of monoidal natural isomorphisms is equivalent to Cohomologous2, and equivalence classes of monoidal structures are classified by H²(G, A).

def autPullback3 (G : Type u) [Group G] (A : Type v) (φ : G ≃* G) (ω : Cochain3' G A) : Cochain3' G A

The pullback of a 3-cochain ω along a group automorphism φ.

theorem autPullback3_eq_pullback3 (G : Type u) [Group G] (A : Type v) [CommGroup A] (φ : G ≃* G) (ω : Cochain3' G A) : autPullback3 G A φ ω = pullback3 G G A φ.toMonoidHom ω

The automorphism pullback agrees with the homomorphism pullback applied to the underlying MonoidHom.

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

Two 3-cochains are in the same automorphism orbit if some automorphism of G maps the class of one to the class of the other in H³(G, A).

theorem monoidal_equiv_general_iff_autOrbit (G : Type u) [Group G] (A : Type v) [CommGroup A] (ω₁ ω₂ : Cochain3' G A) : (∃ (φ : G ≃* G) (μ : Cochain2 G A), IsMonoidalFunctorData G G A ω₁ ω₂ φ.toMonoidHom μ) ↔ AutOrbitCohomologous3 G A ω₁ ω₂

A monoidal equivalence between graded categories with arbitrary underlying automorphism exists if and only if the source and target 3-cocycles lie in the same Aut(G)-orbit on H³(G, A).

theorem innerAut_acts_trivially_on_H3 (G : Type u) [Group G] (A : Type v) [CommGroup A] (g : G) (ω : Cochain3' G A) : Cohomologous3 G A ω (autPullback3 G A (MulAut.conj g) ω)

Inner automorphisms of G act trivially on H³(G, A): conjugation by a group element preserves the cohomology class of any 3-cocycle.

theorem Proposition_1_7_1_iii_with_OutG (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 ω₁ ω₂) ∧ ((∃ (φ : G ≃* G) (μ : Cochain2 G A), IsMonoidalFunctorData G G A ω₁ ω₂ φ.toMonoidHom μ) ↔ AutOrbitCohomologous3 G A ω₁ ω₂)

EGNO Proposition 1.7.1 (iii) refined: combining the H³-classification with the Out(G)-action describing the general monoidal-equivalence orbits.

theorem Proposition_1_7_1_combined (G : Type u) [Group G] (A : Type v) [CommGroup A] : (∀ (μ μ' : Cochain2 G A), ((∃ (η : Cochain1 G A), IsMonoidalNatTransData G A μ μ' η) ↔ Cohomologous2 G A μ μ') ∧ (∀ {η η' : Cochain1 G A}, IsMonoidalNatTransData G A μ μ' η → IsMonoidalNatTransData G A μ μ' η' → ∃ (χ : G →* A), ∀ (g : G), η' g = χ g * η g) ∧ ∀ {η : Cochain1 G A}, IsMonoidalNatTransData G A μ μ' η → ∀ (χ : G →* A), IsMonoidalNatTransData G A μ μ' fun (g : G) => χ g * η g) ∧ (∀ (μ μ' : Cochain2 G A), ((∃ (η : Cochain1 G A), IsMonoidalNatIso G A μ μ' η) ↔ Cohomologous2 G A μ μ') ∧ ((∃ (η : Cochain1 G A), ∀ (g h : G), μ' g h = μ g h * d1 G A η g h) ↔ ⟦μ⟧ = ⟦μ'⟧)) ∧ ∀ (ω₁ ω₂ : Cochain3' G A), ((∃ (μ : Cochain2 G A), IsMonoidalFunctorData G G A ω₁ ω₂ (MonoidHom.id G) μ) ↔ Cohomologous3 G A ω₁ ω₂) ∧ ((∃ (φ : G ≃* G) (μ : Cochain2 G A), IsMonoidalFunctorData G G A ω₁ ω₂ φ.toMonoidHom μ) ↔ AutOrbitCohomologous3 G A ω₁ ω₂)

EGNO Proposition 1.7.1 combined statement: assembling parts (i), (ii) (with torsor refinement), and (iii) (with Out(G) action) into a single theorem.