Rigidity of the Karoubi envelope

For a right rigid monoidal category C, the Karoubi envelope is right rigid: the dual of an idempotent (X, p) is (Xᘁ, pᘁ), the adjoint mate of p being idempotent by contravariant functoriality of the mate. The coevaluation and evaluation are the idempotent-corrected cup and cap; the snake identities reduce to the base category's by sliding the idempotents around the cup and cap — the first collapses onto the defining formula of the adjoint mate, the second onto the base snake identity.

When C is moreover braided, Karoubi C is rigid.

Componentwise access to the Karoubi monoidal data

The dual idempotent

theorem RS.mate_idem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (P.pᘁ) (P.pᘁ) = P.pᘁ

The adjoint mate of an idempotent is idempotent.

noncomputable def RS.karoubiRightDualObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.Idempotents.Karoubi C

The right dual object in the Karoubi envelope.

Equations

• RS.karoubiRightDualObj P = { X := P.Xᘁ, p := P.pᘁ, idem := ⋯ }

Cup and cap absorption

theorem RS.coev_corr_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (η_ P.X P.Xᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ)) = CategoryTheory.CategoryStruct.comp (η_ P.X P.Xᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (P.pᘁ))

The corrected coevaluation absorbs into a single whisker on the dual leg.

theorem RS.coev_corr_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (η_ P.X P.Xᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ)) = CategoryTheory.CategoryStruct.comp (η_ P.X P.Xᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.p P.Xᘁ)

The corrected coevaluation absorbs into a single whisker on the primal leg.

theorem RS.ev_corr_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) P.p) (ε_ P.X P.Xᘁ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.Xᘁ P.p) (ε_ P.X P.Xᘁ)

The corrected evaluation absorbs into a single whisker on the primal leg.

theorem RS.ev_corr_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) P.p) (ε_ P.X P.Xᘁ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (P.pᘁ) P.X) (ε_ P.X P.Xᘁ)

The corrected evaluation absorbs into a single whisker on the dual leg.

theorem RS.coev_corr_idem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (η_ P.X P.Xᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ))) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ)) = CategoryTheory.CategoryStruct.comp (η_ P.X P.Xᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ))

The corrected coevaluation is stable under the correction.

theorem RS.ev_corr_idem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) P.p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) P.p) (ε_ P.X P.Xᘁ)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) P.p) (ε_ P.X P.Xᘁ)

The corrected evaluation is stable under the correction.

The snake identities, componentwise

theorem RS.karoubi_snake_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) (CategoryTheory.CategoryStruct.comp (η_ P.X P.Xᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ))) (CategoryTheory.MonoidalCategoryStruct.associator P.Xᘁ P.X P.Xᘁ).inv) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) P.p) (ε_ P.X P.Xᘁ)) (P.pᘁ))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) (CategoryTheory.MonoidalCategoryStruct.rightUnitor P.Xᘁ).hom) (CategoryTheory.CategoryStruct.comp (P.pᘁ) (CategoryTheory.MonoidalCategoryStruct.leftUnitor P.Xᘁ).inv)

The first snake in the base category, with corrections: collapses onto the defining formula of the adjoint mate.

theorem RS.karoubi_snake_two {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (η_ P.X P.Xᘁ) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ))) P.p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (P.pᘁ)) P.p) (CategoryTheory.MonoidalCategoryStruct.associator P.X P.Xᘁ P.X).hom) (CategoryTheory.MonoidalCategoryStruct.tensorHom P.p (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (P.pᘁ) P.p) (ε_ P.X P.Xᘁ)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) P.p) (CategoryTheory.MonoidalCategoryStruct.leftUnitor P.X).hom) (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.MonoidalCategoryStruct.rightUnitor P.X).inv)

The second snake in the base category, with corrections: collapses onto the base snake identity.

The exact pairing and rigidity

@[instance_reducible]

noncomputable def RS.karoubiExactPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.ExactPairing P (karoubiRightDualObj P)

The exact pairing between an idempotent and its mate dual.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.karoubiHasRightDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (P : CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.HasRightDual P

Every Karoubi object has a right dual: the ambient dual, cut by the dual idempotent.

Equations

• RS.karoubiHasRightDual P = { rightDual := RS.karoubiRightDualObj P, exact := RS.karoubiExactPairing P }

@[instance_reducible]

noncomputable instance RS.karoubiRightRigid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] : CategoryTheory.RightRigidCategory (CategoryTheory.Idempotents.Karoubi C)

The Karoubi envelope of a right rigid category is right rigid.

Equations

• RS.karoubiRightRigid = { rightDual := fun (X : CategoryTheory.Idempotents.Karoubi C) => RS.karoubiHasRightDual X }

@[instance_reducible]

noncomputable instance RS.karoubiRigid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.RigidCategory (CategoryTheory.Idempotents.Karoubi C)

The Karoubi envelope of a braided right rigid category is rigid.

Equations

• RS.karoubiRigid = CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory