support the adjunction (a ⊗ -) ⊢ hom(a,-)

[mohamed-barakat]

Currently, we are supporting the adjunction

(- ⊗ b) ⊢ hom(b,-).

When specialized to ⊗ = × in the context of SkeletalFinSets it yields, as expected, an isomorphism

Hom(a × b, c) → Hom(a,hom(b,c)),

which in this case is not the identity. However, the adjunction

(a ⊗ -) ⊢ hom(a,-)

specialized to ⊗ = × in the context of SkeletalFinSets yields the identity:

Hom(a × b, c) → Hom(b, hom(a,c)).

I assume the same will be true in MatrixCategory/CategoryOfRows/CategoryOfColums. This is very useful for other computations so I would like to support this adjunction.

Suggestion:

1. I will rename all occurrences of CAP operations involving the supported adjunction by adding the prefix Second (and deprecating the old name)
2. I will add new CAP operations with the prefix First to support the adjunction (a ⊗ -) ⊢ hom(a,-).

[mohamed-barakat]

This is a nice example for proving using the compiler as a proof-assistant that Hom(a ⊗ b, c) → Hom(b, hom(a,c)) in the above-mentioned skeletal categories is the identity morphism.

[zickgraf]

Is this related to #1501?

This is a nice example for proving using the compiler as a proof-assistant that Hom(a ⊗ b, c) → Hom(b, hom(a,c)) in the above-mentioned skeletal categories is the identity morphism.

Have you tried doing so? Until now, all proofs in monoidal categories I tried to do turned out to be difficult because we have not formalized the coherence theorems for monoidal categories.

[TKuh]

However, the adjunction

(a ⊗ -) ⊢ hom(a,-)

specialized to ⊗ = × in the context of SkeletalFinSets yields the identity:

Hom(a × b, c) → Hom(b, hom(a,c)).

I assume the same will be true in MatrixCategory/CategoryOfRows/CategoryOfColums. This is very useful for other computations so I would like to support this adjunction.

Nice! :)

Suggestion:

1. I will rename all occurrences of CAP operations involving the supported adjunction by adding the prefix `Second` (and deprecating the old name)

2. I will add new CAP operations with the prefix `First` to support the adjunction (a ⊗ -) ⊢ hom(a,-).

How about the names I used in my thesis, see Section 1.1 and Remark 1.1.7 and the tables after it? At least nLab also (partly) uses this naming convention.

Is this related to #1501?

Kind of, I think.

The adjunction $(- \otimes b) \dashv \underline{\mathrm{Hom}}(b,-)$ together with correct notion of dual object leads to deriving $\underline{\mathrm{Hom}}(b,c) \coloneqq c \otimes b^*$ in the rigid setting.

So I suspect, that again with the correct notion of dual, the new adjunction $(b \otimes -) \dashv \underline{\mathrm{Hom}}(b,-)$ from this issue leads to deriving $\underline{\mathrm{Hom}}(b,c) \coloneqq b^* \otimes c$ in a rigid setting. And this is the current derivation of the internal hom.

Also, the two tensor functors $(- \otimes b)$ and $(b \otimes -)$ only differ by a braiding in the rigid setting, so I guess when writing their adjoints again as tensor products, these adjoints should also be related by a braiding.

[mohamed-barakat]

This was completed with 1cb9bb7.