Duals in a monoidal preadditive category

In a monoidal preadditive category the right adjoint mate f ↦ fᘁ is additive, because it is built from whiskering and composition, and the coevaluation of an exact pairing out of a nonzero object is nonzero, by the zigzag identity.

In a monoidal k-linear category the Frobenius reciprocity bijections tensorLeftHomEquiv and tensorRightHomEquiv are k-linear, so they compare dimensions of morphism spaces, for instance of the multiplicity spaces of a fusion category. Specializing to tensorPow V 2 identifies 𝟙_ C ⟶ tensorPow V 2 k-linearly with Vᘁ ⟶ V (TauCeti.homTensorPowTwoLinearEquiv).

Main declarations

• TauCeti.rightAdjointMate_zero and TauCeti.rightAdjointMate_add: the right adjoint mate is additive;
• TauCeti.coevaluation_ne_zero: the coevaluation η_ X Y is nonzero when X is;
• TauCeti.tensorLeftHomLinearEquiv and TauCeti.tensorRightHomLinearEquiv: Frobenius reciprocity as k-linear equivalences, and TauCeti.homTensorPowTwoLinearEquiv (with TauCeti.homTensorPowTwoLinearEquiv_apply and TauCeti.homTensorPowTwoLinearEquiv_symm_apply): its specialization (𝟙_ C ⟶ tensorPow V 2) ≃ₗ[k] (Vᘁ ⟶ V).

@[simp]

theorem TauCeti.rightAdjointMate_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X Y : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] : 0ᘁ = 0

The right adjoint mate of the zero morphism is zero.

@[simp]

theorem TauCeti.rightAdjointMate_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X Y : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] (f g : X ⟶ Y) : (f + g)ᘁ = fᘁ + gᘁ

The right adjoint mate is additive.

theorem TauCeti.coevaluation_ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X Y : C} [CategoryTheory.ExactPairing X Y] (hX : ¬CategoryTheory.Limits.IsZero X) : η_ X Y ≠ 0

The coevaluation of an exact pairing of X with Y is nonzero when X is nonzero: otherwise the zigzag identity would make the identity of X zero.

noncomputable def TauCeti.tensorLeftHomLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y Y' Z : C) [CategoryTheory.ExactPairing Y Y'] : (CategoryTheory.MonoidalCategoryStruct.tensorObj Y' X ⟶ Z) ≃ₗ[k] X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z

Frobenius reciprocity (Y' ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z) for an exact pairing of Y and Y' (CategoryTheory.tensorLeftHomEquiv) is k-linear.

@[simp]

theorem TauCeti.tensorLeftHomLinearEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y Y' Z : C) [CategoryTheory.ExactPairing Y Y'] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj Y' X ⟶ Z) : (tensorLeftHomLinearEquiv k X Y Y' Z) f = (CategoryTheory.tensorLeftHomEquiv X Y Y' Z) f

TauCeti.tensorLeftHomLinearEquiv acts as CategoryTheory.tensorLeftHomEquiv.

@[simp]

theorem TauCeti.tensorLeftHomLinearEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y Y' Z : C) [CategoryTheory.ExactPairing Y Y'] (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) : (tensorLeftHomLinearEquiv k X Y Y' Z).symm f = (CategoryTheory.tensorLeftHomEquiv X Y Y' Z).symm f

The inverse of TauCeti.tensorLeftHomLinearEquiv acts as that of CategoryTheory.tensorLeftHomEquiv.

noncomputable def TauCeti.tensorRightHomLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y Y' Z : C) [CategoryTheory.ExactPairing Y Y'] : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) ≃ₗ[k] X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y'

Frobenius reciprocity (X ⊗ Y ⟶ Z) ≃ (X ⟶ Z ⊗ Y') for an exact pairing of Y and Y' (CategoryTheory.tensorRightHomEquiv) is k-linear.

@[simp]

theorem TauCeti.tensorRightHomLinearEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y Y' Z : C) [CategoryTheory.ExactPairing Y Y'] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : (tensorRightHomLinearEquiv k X Y Y' Z) f = (CategoryTheory.tensorRightHomEquiv X Y Y' Z) f

TauCeti.tensorRightHomLinearEquiv acts as CategoryTheory.tensorRightHomEquiv.

@[simp]

theorem TauCeti.tensorRightHomLinearEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y Y' Z : C) [CategoryTheory.ExactPairing Y Y'] (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y') : (tensorRightHomLinearEquiv k X Y Y' Z).symm f = (CategoryTheory.tensorRightHomEquiv X Y Y' Z).symm f

The inverse of TauCeti.tensorRightHomLinearEquiv acts as that of CategoryTheory.tensorRightHomEquiv.

noncomputable def TauCeti.homTensorPowTwoLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (V : C) [CategoryTheory.HasRightDual V] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ tensorPow V 2) ≃ₗ[k] Vᘁ ⟶ V

Frobenius reciprocity identifies 𝟙_ C ⟶ tensorPow V 2 k-linearly with Vᘁ ⟶ V.

theorem TauCeti.homTensorPowTwoLinearEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (V : C) [CategoryTheory.HasRightDual V] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ tensorPow V 2) : (homTensorPowTwoLinearEquiv k V) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Vᘁ).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Vᘁ (CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Vᘁ V V).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ V Vᘁ) V) (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom)))

Evaluating homTensorPowTwoLinearEquiv closes up the first factor of tensorPow V 2 against Vᘁ with ε_ V Vᘁ.

theorem TauCeti.homTensorPowTwoLinearEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (k : Type w) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (V : C) [CategoryTheory.HasRightDual V] (g : Vᘁ ⟶ V) : (homTensorPowTwoLinearEquiv k V).symm g = CategoryTheory.CategoryStruct.comp (η_ V Vᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv))

The inverse of homTensorPowTwoLinearEquiv sends g : Vᘁ ⟶ V to η_ V Vᘁ composed with g on the second factor, up to the right unitor of V.