Central compositors of pseudofunctors and 2-cocycles

Let a monoid G act on a category C by the identity functor at every g : G, and choose the comparison isomorphisms of this action among the central automorphisms of C, that is, among the units of the center CatCenter C = End (𝟭 C). Such a choice is a function c : G × G → (CatCenter C)ˣ, the compositor T_(h * g) ≅ T_g ⋙ T_h being c (h, g). This file shows that the coherence of the compositors has mathematical content: the associativity condition is the multiplicative 2-cocycle identity, and changing the identifications of the transport functors with the identity by central units b : G → (CatCenter C)ˣ multiplies c by the coboundary of b.

Since the center of C is commutative and the action functors are identities, G acts trivially on the coefficients. The cocycle identity is therefore that of groupCohomology.IsMulCocycle₂ for the trivial action, c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j), and the coboundary that of groupCohomology.IsMulCoboundary₂. They are stated explicitly, since Mathlib has no trivial-action instance on an arbitrary commutative group. The same identity, for central units indexed by an additive monoid, is the associativity axiom of Mathlib's CategoryTheory.TwistShiftData, which twists the compositors of a shift by central units.

Main declarations

• TauCeti.centralUnitIso C z: the invertible 2-cell of Cat on the identity functor of C whose components are those of the central unit z.
• TauCeti.centralUnitIso_associativity_iff: the associativity condition of a pseudofunctor out of LocallyDiscrete (SingleObj G) whose 1-cells are identities and whose compositors are centralUnitIso C (c (h, g)) holds at (g, h, j) if and only if c satisfies the 2-cocycle identity there. TauCeti.centralUnitIso_left_unitor_iff and TauCeti.centralUnitIso_right_unitor_iff treat the unit conditions.
• TauCeti.centralCocyclePseudofunctor c hc: the pseudofunctor LocallyDiscrete (SingleObj G) ⥤ᵖ Cat attached to a 2-cocycle c, with identity 1-cells, compositors c and unit comparison (c (1, 1))⁻¹.
• TauCeti.centralUnitIso_naturality_comp_iff: the composition condition of a strong transformation with identity components and naturality 2-cells centralUnitIso C (b g) between two such pseudofunctors holds if and only if the compositors differ by the coboundary of b.
• TauCeti.centralCocycleStrongTrans b hb: the resulting strong transformation centralCocyclePseudofunctor c hc ⟶ centralCocyclePseudofunctor c' hc' when c' (g, h) = b g * b h / b (g * h) * c (g, h).

References

Choices of transport functors whose composition isomorphisms need not be coherent, and the resulting role of coherence for categorical actions, are discussed in

• Edward Frenkel, Langlands Correspondence for Loop Groups, §1.3.

The pseudofunctor and strong-transformation axioms are those of

• Niles Johnson and Donald Yau, 2-Dimensional Categories, arXiv:2002.06055, Chapter 4.

def TauCeti.centralUnitIso (C : Type w) [CategoryTheory.Category.{v, w} C] (z : (CategoryTheory.CatCenter C)ˣ) : CategoryTheory.CategoryStruct.id ↧C ≅ CategoryTheory.CategoryStruct.id ↧C

The invertible 2-cell of Cat on the identity functor of C given by a unit z of the center of C: its components are the automorphisms z.app X of the objects X of C.

@[simp]

theorem TauCeti.centralUnitIso_hom_toNatTrans_app {C : Type w} [CategoryTheory.Category.{v, w} C] (z : (CategoryTheory.CatCenter C)ˣ) (X : C) : (centralUnitIso C z).hom.toNatTrans.app X = (↑z).app X

@[simp]

theorem TauCeti.centralUnitIso_inv_toNatTrans_app {C : Type w} [CategoryTheory.Category.{v, w} C] (z : (CategoryTheory.CatCenter C)ˣ) (X : C) : (centralUnitIso C z).inv.toNatTrans.app X = (↑z⁻¹).app X

theorem TauCeti.centralUnitIso_inv {C : Type w} [CategoryTheory.Category.{v, w} C] (z : (CategoryTheory.CatCenter C)ˣ) : (centralUnitIso C z).inv = (centralUnitIso C z⁻¹).hom

@[simp]

theorem TauCeti.centralUnitIso_one {C : Type w} [CategoryTheory.Category.{v, w} C] : centralUnitIso C 1 = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id ↧C)

@[simp]

theorem TauCeti.centralUnitIso_hom_comp_hom {C : Type w} [CategoryTheory.Category.{v, w} C] (z z' : (CategoryTheory.CatCenter C)ˣ) : CategoryTheory.CategoryStruct.comp (centralUnitIso C z).hom (centralUnitIso C z').hom = (centralUnitIso C (z * z')).hom

@[simp]

theorem TauCeti.centralUnitIso_hom_comp_hom_assoc {C : Type w} [CategoryTheory.Category.{v, w} C] (z z' : (CategoryTheory.CatCenter C)ˣ) {Z : ↧C ⟶ ↧C} (h : CategoryTheory.CategoryStruct.id ↧C ⟶ Z) : CategoryTheory.CategoryStruct.comp (centralUnitIso C z).hom (CategoryTheory.CategoryStruct.comp (centralUnitIso C z').hom h) = CategoryTheory.CategoryStruct.comp (centralUnitIso C (z * z')).hom h

@[simp]

theorem TauCeti.centralUnitIso_hom_inj {C : Type w} [CategoryTheory.Category.{v, w} C] {z z' : (CategoryTheory.CatCenter C)ˣ} : (centralUnitIso C z).hom = (centralUnitIso C z').hom ↔ z = z'

@[simp]

theorem TauCeti.centralUnitIso_hom_eq_id_iff {C : Type w} [CategoryTheory.Category.{v, w} C] {z : (CategoryTheory.CatCenter C)ˣ} : (centralUnitIso C z).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id ↧C) ↔ z = 1

theorem TauCeti.centralUnitIso_associativity_iff {G : Type u} [Monoid G] (C : Type w) [CategoryTheory.Category.{v, w} C] (c : G × G → (CategoryTheory.CatCenter C)ˣ) (g h j : G) : CategoryTheory.CategoryStruct.comp (centralUnitIso C (c (j, h * g))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (centralUnitIso C (c (h, g))).hom (CategoryTheory.CategoryStruct.id ↧C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id ↧C) (centralUnitIso C (c (j, h))).inv) (centralUnitIso C (c (j * h, g))).inv))) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id ↧C) ↔ c (j * h, g) * c (j, h) = c (h, g) * c (j, h * g)

The associativity condition of a pseudofunctor out of LocallyDiscrete (SingleObj G) with identity 1-cells and central compositors centralUnitIso C (c (h, g)) at g ≫ h = h * g, evaluated at (g, h, j), is the 2-cocycle identity c (j * h, g) * c (j, h) = c (h, g) * c (j, h * g) of c at (j, h, g).

theorem TauCeti.centralUnitIso_left_unitor_iff {G : Type u} [Monoid G] (C : Type w) [CategoryTheory.Category.{v, w} C] (c : G × G → (CategoryTheory.CatCenter C)ˣ) (u : (CategoryTheory.CatCenter C)ˣ) (g : G) : CategoryTheory.CategoryStruct.comp (centralUnitIso C (c (g, 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (centralUnitIso C u).hom (CategoryTheory.CategoryStruct.id ↧C)) (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id ↧C)).hom) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id ↧C) ↔ c (g, 1) * u = 1

The left unit condition of a pseudofunctor out of LocallyDiscrete (SingleObj G) with identity 1-cells, central compositors centralUnitIso C (c (h, g)) at g ≫ h = h * g and unit comparison centralUnitIso C u, evaluated at g, is c (g, 1) * u = 1.

theorem TauCeti.centralUnitIso_right_unitor_iff {G : Type u} [Monoid G] (C : Type w) [CategoryTheory.Category.{v, w} C] (c : G × G → (CategoryTheory.CatCenter C)ˣ) (u : (CategoryTheory.CatCenter C)ˣ) (g : G) : CategoryTheory.CategoryStruct.comp (centralUnitIso C (c (1, g))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id ↧C) (centralUnitIso C u).hom) (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id ↧C)).hom) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id ↧C) ↔ c (1, g) * u = 1

The right unit condition of a pseudofunctor out of LocallyDiscrete (SingleObj G) with identity 1-cells, central compositors centralUnitIso C (c (h, g)) at g ≫ h = h * g and unit comparison centralUnitIso C u, evaluated at g, is c (1, g) * u = 1.

def TauCeti.centralCocyclePseudofunctor {G : Type u} [Monoid G] (C : Type w) [CategoryTheory.Category.{v, w} C] (c : G × G → (CategoryTheory.CatCenter C)ˣ) (hc : ∀ (g h j : G), c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j)) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.SingleObj G)) CategoryTheory.Cat

The pseudofunctor LocallyDiscrete (SingleObj G) ⥤ᵖ Cat attached to a 2-cocycle c of G with coefficients in the central units of C, for the trivial action. It sends the unique object to C and every g to the identity functor; its composition comparison at g ≫ h = h * g is centralUnitIso C (c (h, g)), and its unit comparison is centralUnitIso C (c (1, 1))⁻¹.

@[simp]

theorem TauCeti.centralCocyclePseudofunctor_obj {G : Type u} [Monoid G] {C : Type w} [CategoryTheory.Category.{v, w} C] {c : G × G → (CategoryTheory.CatCenter C)ˣ} {hc : ∀ (g h j : G), c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j)} (a : CategoryTheory.LocallyDiscrete (CategoryTheory.SingleObj G)) : (centralCocyclePseudofunctor C c hc).obj a = ↧C

@[simp]

theorem TauCeti.centralCocyclePseudofunctor_map {G : Type u} [Monoid G] {C : Type w} [CategoryTheory.Category.{v, w} C] {c : G × G → (CategoryTheory.CatCenter C)ˣ} {hc : ∀ (g h j : G), c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j)} {a b : CategoryTheory.LocallyDiscrete (CategoryTheory.SingleObj G)} (g : a ⟶ b) : (centralCocyclePseudofunctor C c hc).map g = CategoryTheory.CategoryStruct.id ↧C

@[simp]

theorem TauCeti.centralCocyclePseudofunctor_mapId {G : Type u} [Monoid G] {C : Type w} [CategoryTheory.Category.{v, w} C] {c : G × G → (CategoryTheory.CatCenter C)ˣ} {hc : ∀ (g h j : G), c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j)} (a : CategoryTheory.LocallyDiscrete (CategoryTheory.SingleObj G)) : (centralCocyclePseudofunctor C c hc).mapId a = centralUnitIso C (c (1, 1))⁻¹

@[simp]

theorem TauCeti.centralCocyclePseudofunctor_mapComp {G : Type u} [Monoid G] {C : Type w} [CategoryTheory.Category.{v, w} C] {c : G × G → (CategoryTheory.CatCenter C)ˣ} {hc : ∀ (g h j : G), c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j)} {a b d : CategoryTheory.LocallyDiscrete (CategoryTheory.SingleObj G)} (g : a ⟶ b) (h : b ⟶ d) : (centralCocyclePseudofunctor C c hc).mapComp g h = centralUnitIso C (c (h.as, g.as))

theorem TauCeti.centralUnitIso_naturality_id_iff {G : Type u} [Monoid G] (C : Type w) [CategoryTheory.Category.{v, w} C] (b : G → (CategoryTheory.CatCenter C)ˣ) (u u' : (CategoryTheory.CatCenter C)ˣ) : CategoryTheory.CategoryStruct.comp (centralUnitIso C (b 1)).hom (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id ↧C) (centralUnitIso C u').hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (centralUnitIso C u).hom (CategoryTheory.CategoryStruct.id ↧C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id ↧C)).hom (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id ↧C)).inv) ↔ b 1 * u' = u

The unit condition of a strong transformation with identity components and naturality 2-cells centralUnitIso C (b g), between pseudofunctors with identity 1-cells and unit comparisons centralUnitIso C u and centralUnitIso C u', is b 1 * u' = u.

theorem TauCeti.centralUnitIso_naturality_comp_iff {G : Type u} [Monoid G] (C : Type w) [CategoryTheory.Category.{v, w} C] (b : G → (CategoryTheory.CatCenter C)ˣ) (c c' : G × G → (CategoryTheory.CatCenter C)ˣ) (g h : G) : CategoryTheory.CategoryStruct.comp (centralUnitIso C (b (h * g))).hom (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id ↧C) (centralUnitIso C (c' (h, g))).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (centralUnitIso C (c (h, g))).hom (CategoryTheory.CategoryStruct.id ↧C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id ↧C) (centralUnitIso C (b h)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (centralUnitIso C (b g)).hom (CategoryTheory.CategoryStruct.id ↧C)) (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C)).hom)))) ↔ c' (h, g) = b h * b g / b (h * g) * c (h, g)

The composition condition of a strong transformation with identity components and naturality 2-cells centralUnitIso C (b g), between pseudofunctors with identity 1-cells and central compositors centralUnitIso C (c (h, g)) and centralUnitIso C (c' (h, g)) at g ≫ h = h * g, evaluated at (g, h), states that c' is c multiplied by the coboundary of b at (h, g).

def TauCeti.centralCocycleStrongTrans {G : Type u} [Monoid G] {C : Type w} [CategoryTheory.Category.{v, w} C] {c c' : G × G → (CategoryTheory.CatCenter C)ˣ} {hc : ∀ (g h j : G), c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j)} {hc' : ∀ (g h j : G), c' (g * h, j) * c' (g, h) = c' (h, j) * c' (g, h * j)} (b : G → (CategoryTheory.CatCenter C)ˣ) (hb : ∀ (g h : G), c' (g, h) = b g * b h / b (g * h) * c (g, h)) : (centralCocyclePseudofunctor C c hc).StrongTrans (centralCocyclePseudofunctor C c' hc')

The strong transformation centralCocyclePseudofunctor C c hc ⟶ centralCocyclePseudofunctor C c' hc' with identity components whose naturality 2-cell at g is centralUnitIso C (b g), when c' is c multiplied by the coboundary of b : G → (CatCenter C)ˣ. By centralUnitIso_naturality_comp_iff, this coboundary relation is also necessary for the identity components and the 2-cells centralUnitIso C (b g) to form a strong transformation.

@[simp]

theorem TauCeti.centralCocycleStrongTrans_app {G : Type u} [Monoid G] {C : Type w} [CategoryTheory.Category.{v, w} C] {c c' : G × G → (CategoryTheory.CatCenter C)ˣ} {hc : ∀ (g h j : G), c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j)} {hc' : ∀ (g h j : G), c' (g * h, j) * c' (g, h) = c' (h, j) * c' (g, h * j)} (b : G → (CategoryTheory.CatCenter C)ˣ) (hb : ∀ (g h : G), c' (g, h) = b g * b h / b (g * h) * c (g, h)) (a : CategoryTheory.LocallyDiscrete (CategoryTheory.SingleObj G)) : (centralCocycleStrongTrans b hb).app a = CategoryTheory.CategoryStruct.id ↧C

@[simp]

theorem TauCeti.centralCocycleStrongTrans_naturality {G : Type u} [Monoid G] {C : Type w} [CategoryTheory.Category.{v, w} C] {c c' : G × G → (CategoryTheory.CatCenter C)ˣ} {hc : ∀ (g h j : G), c (g * h, j) * c (g, h) = c (h, j) * c (g, h * j)} {hc' : ∀ (g h j : G), c' (g * h, j) * c' (g, h) = c' (h, j) * c' (g, h * j)} (b : G → (CategoryTheory.CatCenter C)ˣ) (hb : ∀ (g h : G), c' (g, h) = b g * b h / b (g * h) * c (g, h)) {a a' : CategoryTheory.LocallyDiscrete (CategoryTheory.SingleObj G)} (g : a ⟶ a') : (centralCocycleStrongTrans b hb).naturality g = centralUnitIso C (b g.as)