Scalars in a monoidal category

A scalar in a monoidal category C is an endomorphism a : 𝟙_ C ⟶ 𝟙_ C of the unit. Whiskering an object by a scalar is compatible with every morphism to or from the unit: a scalar acting on the unit factor of Y ⊗ 𝟙_ C can be moved past any morphism Y ⊗ 𝟙_ C ⟶ 𝟙_ C (TauCeti.whiskerLeft_scalar_comp), and dually a scalar acting on the unit factor of 𝟙_ C ⊗ Y can be moved past any morphism 𝟙_ C ⟶ 𝟙_ C ⊗ Y (TauCeti.comp_scalar_whiskerRight). In particular scalars commute with each other (TauCeti.scalar_comm).

A scalar a acts on every object Y in two ways, from the left as (λ_ Y).inv ≫ a ▷ Y ≫ (λ_ Y).hom and from the right as (ρ_ Y).inv ≫ Y ◁ a ≫ (ρ_ Y).hom. The two actions need not agree in a general monoidal category, but they do in a braided one (TauCeti.leftUnitor_inv_scalar_whiskerRight_leftUnitor_hom). They also agree in a linear one over an algebraically closed field whose unit is simple with finite-dimensional endomorphisms, where every scalar is a multiple of the identity (TauCeti.leftUnitor_inv_scalar_whiskerRight_leftUnitor_hom_of_simple).

TauCeti.CirclesCommuteAt d X records agreement of the two actions of a particular scalar d on a particular object X. These objects form a replete monoidal full subcategory: agreement holds at the unit, is preserved by isomorphisms, and is closed under tensor products. Thus a circle value central on a generating object is central on every interpreted tensor word in that object, without requiring it to be central on every object of the ambient category. Agreement is also closed under composition of scalars, so any finite number of such circles can be moved between the two sides.

References

• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §2.2.

theorem TauCeti.whiskerLeft_scalar_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (e : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y a) e = CategoryTheory.CategoryStruct.comp e a

A scalar acting on the unit factor of Y ⊗ 𝟙_ C can be moved past any morphism to the unit: Y ◁ a ≫ e = e ≫ a.

theorem TauCeti.whiskerLeft_scalar_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (e : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y a) (CategoryTheory.CategoryStruct.comp e h) = CategoryTheory.CategoryStruct.comp e (CategoryTheory.CategoryStruct.comp a h)

A scalar acting on the unit factor of Y ⊗ 𝟙_ C can be moved past any morphism to the unit: Y ◁ a ≫ e = e ≫ a.

theorem TauCeti.comp_scalar_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y) : CategoryTheory.CategoryStruct.comp e (CategoryTheory.MonoidalCategoryStruct.whiskerRight a Y) = CategoryTheory.CategoryStruct.comp a e

A scalar acting on the unit factor of 𝟙_ C ⊗ Y can be moved past any morphism from the unit: e ≫ a ▷ Y = a ≫ e.

theorem TauCeti.comp_scalar_whiskerRight_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y ⟶ Z) : CategoryTheory.CategoryStruct.comp e (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight a Y) h) = CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp e h)

A scalar acting on the unit factor of 𝟙_ C ⊗ Y can be moved past any morphism from the unit: e ≫ a ▷ Y = a ≫ e.

theorem TauCeti.scalar_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (a b : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp a b = CategoryTheory.CategoryStruct.comp b a

Scalars commute: the endomorphisms of the unit form a commutative monoid.

theorem TauCeti.leftUnitor_inv_scalar_whiskerRight_leftUnitor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight a Y) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y a) (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom)

In a braided monoidal category, a scalar acts on every object in the same way from the left and from the right.

theorem TauCeti.leftUnitor_inv_scalar_whiskerRight_leftUnitor_hom_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (k : Type w) [Field k] [IsAlgClosed k] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] [FiniteDimensional k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight a Y) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y a) (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom)

If the tensor unit is simple with finite-dimensional endomorphisms over an algebraically closed field, a scalar acts on every object in the same way from the left and from the right.

Centrality at an object

def TauCeti.CirclesCommuteAt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (d : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (X : C) : Prop

A scalar d acts in the same way on the right and on the left of X. For the value of a closed circle, this is the condition allowing that circle to be moved past X. It is a condition at X alone, not at all objects of the category.

theorem TauCeti.circlesCommuteAt_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (d : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (X : C) : CirclesCommuteAt d X ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X d) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight d X) (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)

The two scalar actions whose agreement defines CirclesCommuteAt.

instance TauCeti.circlesCommuteAt_isMonoidal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (d : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.ObjectProperty.IsMonoidal (CirclesCommuteAt d)

The objects at which a fixed scalar is central form a monoidal full subcategory. In particular, centrality holds at the unit and propagates from generators to their tensor words by CategoryTheory.ObjectProperty.prop_projectObj.

instance TauCeti.circlesCommuteAt_isClosedUnderIsomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (d : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms (CirclesCommuteAt d)

Centrality of a scalar at an object is invariant under isomorphism. The full monoidal subcategory of central objects is therefore replete.

@[simp]

theorem TauCeti.circlesCommuteAt_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : CirclesCommuteAt (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) X

The identity scalar is central at every object.

theorem TauCeti.CirclesCommuteAt.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {d e : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C} {X : C} (hd : CirclesCommuteAt d X) (he : CirclesCommuteAt e X) : CirclesCommuteAt (CategoryTheory.CategoryStruct.comp d e) X

Two scalars central at X have composite central at X. This allows repeated circles to be moved past the same object.

@[simp]

theorem TauCeti.circlesCommuteAt_smul_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {R : Type u_1} [Semiring R] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (r : R) (X : C) : CirclesCommuteAt (r • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) X

A scalar multiple of the identity of the unit is central at every object of a monoidal linear category. Thus prescribing a loop value δ • 𝟙 needs no separate centrality assumption.