Rigidity of the matrix envelope

When C is a right rigid monoidal preadditive category, the matrix envelope Mat_ C is right rigid: the dual of an object M = (ι, X) is (ι, fun i => (X i)ᘁ), with coevaluation and evaluation built diagonally from the componentwise cups and caps. The snake identities reduce to collapsing off-diagonal sums (all zero by MonoidalPreadditive) and applying the base snake identity at each index.

When C is moreover braided, Mat_ C is rigid.

Componentwise access lemmas

The private access lemmas in MatBraided.lean are not visible here, so we restate the ones we need. Each is proved by rfl.

The dual object

@[reducible]

noncomputable def RS.matRightDualObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (M : CategoryTheory.Mat_ C) : CategoryTheory.Mat_ C

The right dual of M in Mat_ C: same index set, componentwise dual.

Equations

• RS.matRightDualObj M = { ι := M.ι, fintype := M.fintype, X := fun (i : M.ι) => (M.X i)ᘁ }

Coevaluation and evaluation

noncomputable def RS.matCoev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (M : CategoryTheory.Mat_ C) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mat_ C) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M (matRightDualObj M)

Componentwise coevaluation: diagonal matrix of cups.

Equations

• RS.matCoev M x✝ p = if h : p.1 = p.2 then CategoryTheory.CategoryStruct.comp (η_ (M.X p.1) (M.X p.1)ᘁ) (CategoryTheory.eqToHom ⋯) else 0

noncomputable def RS.matEv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (M : CategoryTheory.Mat_ C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (matRightDualObj M) M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Mat_ C)

Componentwise evaluation: diagonal matrix of caps.

Equations

• RS.matEv M p x✝ = if h : p.1 = p.2 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (ε_ (M.X p.2) (M.X p.2)ᘁ) else 0

Entry lemmas for coev/ev

The snake identities

The exact pairing and rigidity instances

@[instance_reducible]

noncomputable def RS.matExactPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RightRigidCategory C] (M : CategoryTheory.Mat_ C) : CategoryTheory.ExactPairing M (matRightDualObj M)

The exact pairing between M and its componentwise right dual.

Equations

• RS.matExactPairing M = { coevaluation' := RS.matCoev M, evaluation' := RS.matEv M, coevaluation_evaluation' := ⋯, evaluation_coevaluation' := ⋯ }

@[instance_reducible]

noncomputable instance RS.matHasRightDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RightRigidCategory C] (M : CategoryTheory.Mat_ C) : CategoryTheory.HasRightDual M

Every object in Mat_ C has a right dual.

Equations

• RS.matHasRightDual M = { rightDual := RS.matRightDualObj M, exact := RS.matExactPairing M }

@[instance_reducible]

noncomputable instance RS.matRightRigid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RightRigidCategory C] : CategoryTheory.RightRigidCategory (CategoryTheory.Mat_ C)

Mat_ C is right rigid when C is right rigid.

Equations

• RS.matRightRigid = { rightDual := fun (X : CategoryTheory.Mat_ C) => RS.matHasRightDual X }

@[instance_reducible]

noncomputable instance RS.matRigid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.RigidCategory (CategoryTheory.Mat_ C)

Mat_ C is rigid when C is right rigid and braided.

Equations

• RS.matRigid = CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory