structure IsStrictMonoidal (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Prop

A monoidal category C is strict (Definition 1.8.1) if the tensor product is strictly associative and strictly unital, i.e., (X ⊗ Y) ⊗ Z = X ⊗ (Y ⊗ Z), 𝟙_ C ⊗ X = X and X ⊗ 𝟙_ C = X hold on the nose.

• tensorObj_assoc (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z = CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
• tensorUnit_left (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X = X
• tensorUnit_right (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = X

theorem isStrictMonoidal_of_skeletal {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (hC : CategoryTheory.Skeletal C) : IsStrictMonoidal C

A skeletal monoidal category is automatically strict, since the associator and unit isomorphisms become identities.

theorem Theorem_1_15_1_endUnit_semisimple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [inst_ab : CategoryTheory.Abelian C] [TensorCategories.MonoidalBiexact C] [IsArtinianRing (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] : IsSemisimpleRing (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

Theorem 1.15.1: In any multiring category (here a monoidally biexact abelian category with Artinian endomorphism ring of the unit), the algebra End(𝟙) is semisimple.

structure QuantumSl2Witness (k : Type u) [Field k] (q : k) : Type (u + 1)

Definition 1.25.1 / Theorem 1.25.2: A witness for the Hopf algebra U_q(sl_2). It packages the carrier algebra H with generators K, K⁻¹, E, F satisfying the defining commutation relations and the prescribed comultiplication.

• carrier : Type u
• instRing : Ring self.carrier
• instHopf : HopfAlgebra k self.carrier
• K : self.carrier
• Kinv : self.carrier
• E : self.carrier
• F : self.carrier
• K_mul_Kinv : self.K * self.Kinv = 1
• Kinv_mul_K : self.Kinv * self.K = 1
• K_E_Kinv : self.K * self.E * self.Kinv = q ^ 2 • self.E
• K_F_Kinv : self.K * self.F * self.Kinv = (q ^ 2)⁻¹ • self.F
• EF_comm : self.E * self.F - self.F * self.E = (q - q⁻¹)⁻¹ • (self.K - self.Kinv)
• comul_K : CoalgebraStruct.comul self.K = self.K ⊗ₜ[k] self.K
• comul_E : CoalgebraStruct.comul self.E = self.E ⊗ₜ[k] self.K + 1 ⊗ₜ[k] self.E
• comul_F : CoalgebraStruct.comul self.F = self.F ⊗ₜ[k] 1 + self.Kinv ⊗ₜ[k] self.F

theorem Thm_1_35_6_quasi_hopf_reconstruction (k : Type u) [Field k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.RightRigidCategory C] (F : CategoryTheory.Functor C (ModuleCat k)) [F.Faithful] [F.Additive] : ∃ (H : Type (max u v w)) (x : Ring H) (x_1 : Algebra k H), Nonempty (C ≌ ModuleCat H)

Theorem 1.35.6 (reconstruction): A finite tensor category C equipped with a faithful additive functor F : C ⥤ ModuleCat k can be realized as the representation category of some k-algebra H.

noncomputable def EGNO.leftQuantumTrace {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] {V : C} (a : V ⟶ Vᘁᘁ) : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The left quantum trace Tr^L_V(a) of a morphism a : V ⟶ V** in a rigid monoidal category, defined via coevaluation, the morphism a whiskered on the right by V*, and evaluation.

noncomputable def EGNO.rightQuantumTrace {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] {V : C} (a : V ⟶ ᘁᘁV) : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The right quantum trace Tr^R_V(a) of a morphism a : V ⟶ **V in a rigid monoidal category, defined via coevaluation, the morphism a whiskered on the left by *V, and evaluation.

noncomputable def Prop_1_41_1_leftDual_iso_rightDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.IsMultifusionCategory C] (V : C) : ᘁV ≅ Vᘁ

Proposition 1.41.1 (part 1): In a semisimple multifusion category, the left dual *V is canonically isomorphic to the right dual V*.

noncomputable def Prop_1_41_1_doubleDual_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.IsMultifusionCategory C] (V : C) : V ≅ Vᘁᘁ

Proposition 1.41.1 (part 2): In a semisimple multifusion category, every object V is canonically isomorphic to its double dual V**.