structure TensorCategories.Definition_1_1_2_MonoidalSubcategory (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Type (max (max (max u₁ (u₂ + 1)) v₁) (v₂ + 1))

Definition 1.1.2: a monoidal subcategory of a monoidal category C is a monoidal category D together with a faithful monoidal functor ι : D ⥤ C.

• D : Type u₂
• instCat : CategoryTheory.Category.{v₂, u₂} self.D
• instMonoidal : CategoryTheory.MonoidalCategory self.D
• ι : CategoryTheory.Functor self.D C
• instFaithful : self.ι.Faithful
• instMonoidalFunctor : self.ι.Monoidal

def TensorCategories.Definition_1_1_2_MonoidalSubcategory.ofFullSubcategory (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] : Definition_1_1_2_MonoidalSubcategory C

A full subcategory cut out by a monoidal object-property of C gives a monoidal subcategory in the sense of Definition_1_1_2_MonoidalSubcategory.

@[reducible, inline]

abbrev TensorCategories.Definition_1_1_2 (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Type (max (max (max u₁ (u_1 + 1)) v₁) (u_2 + 1))

Definition 1.1.2 (alias): the type of monoidal subcategories of C.

@[reducible, inline]

abbrev TensorCategories.def_1_1_2 (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Type (max (max (max u₁ (u_1 + 1)) v₁) (u_2 + 1))

Lower-case alias for Definition_1_1_2, used by other files.

@[reducible]

def TensorCategories.def_1_1_3_monoidalOpposite (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory Cᴹᵒᵖ

Definition 1.1.3 (helper): the monoidal-category instance on the monoidal opposite of C, where tensor product is reversed.

@[reducible, inline]

abbrev TensorCategories.Definition_1_1_3 (C : Type u₁) : Type u₁

Definition 1.1.3: the monoidal opposite category C^{op,⊗} of a monoidal category.

theorem TensorCategories.prop_1_2_2_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom Y

Proposition 1.2.2 (left triangle): the pentagon-axiom consequence α(1,X,Y) ≫ λ_{X⊗Y} = λ_X ▷ Y.

structure TensorCategories.IsUnitObject {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (U : C) : Type (max u₁ v₁)

The property of an object U : C being a (two-sided) unit object: tensoring with U on either side is naturally isomorphic to the identity.

• leftEquiv (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj U X ≅ X
• rightEquiv (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ X

def TensorCategories.isUnitObject_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : IsUnitObject (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The monoidal unit object 𝟙_ C is a unit object, with the natural left and right unitor isomorphisms.

theorem TensorCategories.unitors_inv_equal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv

The inverses of the left and right unitor at the unit object coincide: λ_{𝟙}⁻¹ = ρ_{𝟙}⁻¹.

theorem TensorCategories.rightUnitor_conjugate_whiskerRight_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.MonoidalCategoryStruct.whiskerRight h (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom (CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)

Right-whiskering by 𝟙_ C of an endomorphism of the unit equals conjugation by the right unitor: h ▷ 𝟙 = ρ_{𝟙} ≫ h ≫ ρ_{𝟙}⁻¹.

theorem TensorCategories.rightUnitor_conjugate_whiskerLeft_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom (CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)

Left-whiskering by 𝟙_ C of an endomorphism of the unit equals the same conjugation by the right unitor as in rightUnitor_conjugate_whiskerRight_unit.

theorem TensorCategories.prop_1_2_7 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (f g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp g f

Proposition 1.2.7 (Eckmann–Hilton): the endomorphism monoid of the unit object in a monoidal category is commutative.

theorem TensorCategories.Proposition_1_2_7 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (f g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp g f

Proposition 1.2.7 (textbook-named alias of prop_1_2_7): endomorphisms of the unit object commute.

@[reducible, inline]

abbrev TensorCategories.Definition_1_2_6 (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Type (max u₁ v₁)

Definition 1.2.6: a monoidal category is the data of a category together with a monoidal structure (tensor product, unit, associator, unitors satisfying pentagon and triangle).

def TensorCategories.IsMonoidalEquivalence_def_1_1_3 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Monoidal] : Prop

A monoidal functor F : C ⥤ D is a monoidal equivalence if its underlying functor is an equivalence of categories.

structure TensorCategories.def_1_4_5_MonoidalNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F₁ F₂ : CategoryTheory.Functor C D) [F₁.LaxMonoidal] [F₂.LaxMonoidal] : Type (max u₁ v₂)

Definition 1.4.5: a monoidal natural isomorphism between two lax-monoidal functors is a natural isomorphism whose forward component is a monoidal natural transformation.

• toNatIso : F₁ ≅ F₂
• isMonoidal : CategoryTheory.NatTrans.IsMonoidal self.toNatIso.hom

instance TensorCategories.def_1_4_5_MonoidalNatIso.inv_isMonoidal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F₁ F₂ : CategoryTheory.Functor C D} [F₁.LaxMonoidal] [F₂.LaxMonoidal] (η : def_1_4_5_MonoidalNatIso F₁ F₂) : CategoryTheory.NatTrans.IsMonoidal η.toNatIso.inv

The inverse component of a monoidal natural isomorphism is again a monoidal natural transformation.

instance TensorCategories.rightExactEndofunctor_isMonoidal (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : (CategoryTheory.rightExactFunctor C C).IsMonoidal

The category of right-exact endofunctors of an additive category inherits a monoidal structure from composition: the unit (the identity functor) is right-exact and composition of right-exact functors is right-exact.

@[reducible, inline]

abbrev TensorCategories.EnvelopingAlgebra (k : Type u_1) [CommRing k] (A : Type u_2) [Ring A] [Algebra k A] : Type u_2

The enveloping algebra A^e := A ⊗_k A^{op} of a k-algebra A.

noncomputable def TensorCategories.eilenbergWattsEquiv (k : Type u_1) [Field k] (A : Type u_2) [Ring A] [Algebra k A] [Module.Finite k A] : ModuleCat (EnvelopingAlgebra k A) ≌ ModuleCat A ⥤ᵣ ModuleCat A

Eilenberg–Watts equivalence: for a finite-dimensional k-algebra A, the category of A^e-modules is equivalent to the category of right-exact endofunctors of Mod A.

noncomputable def TensorCategories.prop_1_6_4_bimod_endFunctor_equiv (k : Type u_1) [Field k] (A : Type u_2) [Ring A] [Algebra k A] [Module.Finite k A] : ModuleCat (EnvelopingAlgebra k A) ≌ ModuleCat A ⥤ᵣ ModuleCat A

Proposition 1.6.4: bimodules over a finite-dimensional algebra A are equivalent to right-exact endofunctors of Mod A, via the Eilenberg–Watts equivalence.

@[reducible, inline]

abbrev TensorCategories.Definition_1_4_5_MonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [hF : F.Monoidal] : F.Monoidal

Definition 1.4.5 (alias): packages a Functor.Monoidal instance for a functor between monoidal categories.

def TensorCategories.IsMonoidalFunctorDatum {G₁ : Type u_1} {G₂ : Type u_2} [Group G₁] [Group G₂] {A : Type u_3} [CommGroup A] (ω₁ : G₁ → G₁ → G₁ → A) (ω₂ : G₂ → G₂ → G₂ → A) (f : G₁ →* G₂) (μ : G₁ → G₁ → A) : Prop

The cocycle condition describing the data of a monoidal functor between two 3-cocycle-twisted vector-space categories Vec_{G₁}^{ω₁} → Vec_{G₂}^{ω₂} associated to a group homomorphism f and a 2-cochain μ.

def TensorCategories.IsMonoidalTransformationDatum {G₁ : Type u_1} [Group G₁] {A : Type u_3} [CommGroup A] (μ μ' : G₁ → G₁ → A) (η : G₁ → A) : Prop

The cohomological condition characterising when a 1-cochain η : G₁ → A provides a monoidal natural transformation between two monoidal functors with cochain data μ and μ'.

class TensorCategories.IsStrictMonoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Prop

A monoidal category is strict if the associator and unitors are identities on the nose: (X ⊗ Y) ⊗ Z = X ⊗ (Y ⊗ Z), 𝟙_ C ⊗ X = X, and X ⊗ 𝟙_ C = X.

• assoc_strict (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z = CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
• left_unit_strict (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X = X
• right_unit_strict (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = X

@[reducible]

def TensorCategories.ex_1_8_2_endofunctor_monoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.MonoidalCategory (CategoryTheory.Functor C C)

Example 1.8.2: the category of endofunctors C ⥤ C of any category is monoidal under composition, and that monoidal structure is strict.

def TensorCategories.thm_1_9_normalization (C : Type u_1) : CategoryTheory.Functor.id (CategoryTheory.FreeMonoidalCategory C) ≅ (CategoryTheory.FreeMonoidalCategory.fullNormalize C).comp CategoryTheory.FreeMonoidalCategory.inclusion

Theorem 1.9 (Mac Lane normalization): the identity on the free monoidal category on C is naturally isomorphic to the composition fullNormalize ⋙ inclusion.

@[reducible, inline]

abbrev def_1_1_2 (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Type (max (max (max u_1 (u_3 + 1)) u_2) (u_4 + 1))

Top-level alias for Definition_1_1_2_MonoidalSubcategory, namespaced for external use.

@[reducible, inline]

abbrev def_1_1_3 (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory Cᴹᵒᵖ

Top-level alias for def_1_1_3_monoidalOpposite, namespaced for external use.