Closed zickgraf closed 2 years ago
Nice catch! This is something I was always a bit afraid of to happen, since some morphisms are specializations of others and consistency can be hard to check.
I am mostly worried about the derivations in SymmetricClosedMonoidalCategories*
which make use of dual objects and are also used for the rigid closed case. I think there can be a clash with closed
monoidal categories and rigid closed
ones:
Now, I glanced over the derivations in SymmetricClosedMonoidalCategories*
which make use of dual objects and as far as I can tell, they don't specifically rely on any of the two cases above and should work with either definition.
So, I changed the last two final derivations to $\underline{Hom}(a,1) \coloneqq a^\vee \otimes 1$, squashed the final derivations as you suggested, ran the compiler (only LinearAlgebraForCAP
had slight obvious changes) and ran the tests of several packages, which worked fine. So this does the trick and for now it doesn't seem to break anything.
But for the future, it has to be remembered, that depending on whether one is working with closed
or rigid closed
, the representative of $\underline{Hom}(a,1)$ is different (albeit being isomorphic). And I think, this needs to be documented.
Is my reasoning fine?
I will do a PR tomorrow (also for the coclosed case, which has the same problem).
Nice catch! This is something I was always a bit afraid of to happen, since some morphisms are specializations of others and consistency can be hard to check.
I am mostly worried about the derivations in
SymmetricClosedMonoidalCategories*
which make use of dual objects and are also used for the rigid closed case. I think there can be a clash withclosed
monoidal categories andrigid closed
ones:
For closed we surely want Hom―(a,1)=a∨ (thinking of Toposes and FinSets)
For rigid closed we want Hom―(a,1)=a∨⊗1 for consistency
Now, I glanced over the derivations in
SymmetricClosedMonoidalCategories*
which make use of dual objects and as far as I can tell, they don't specifically rely on any of the two cases above and should work with either definition.So, I changed the last two final derivations to Hom―(a,1):=a∨⊗1, squashed the final derivations as you suggested, ran the compiler (only
LinearAlgebraForCAP
had slight obvious changes) and ran the tests of several packages, which worked fine. So this does the trick and for now it doesn't seem to break anything.Is my reasoning fine?
Yes, very nice, thanks a lot for this in-depth analysis and testing!
But for the future, it has to be remembered, that depending on whether one is working with
closed
orrigid closed
, the representative of Hom―(a,1) is different (albeit being isomorphic). And I think, this needs to be documented.
I don't think this needs explicit documentation (although of course it can't hurt^^). One simply must not rely on a certain representation. In both cases, someone could implement InternalHom...
and Dual...
primitively in such a way that neither $\underline{Hom}(a,1) = a^v$ nor $\underline{Hom}(a,1) = a^v \otimes 1$. We have similar situations all over the place. For example, we can derive
KernelObject( alpha ) := Equalizer( alpha, 0 )
or we can deriveEqualizer( alpha, beta ) := KernelObject( alpha - beta )
.In the second case, in particular we get Equalizer( alpha, 0 ) = KernelObject( alpha - 0 )
which is not equal to KernelObject( alpha )
in general.
I will do a PR tomorrow (also for the coclosed case, which has the same problem).
Perfect, thanks!
The following final derivations are inconsistent: https://github.com/homalg-project/CAP_project/blob/8c610224cd4a24adb2e9f69b6bcd25e0eb00d5e5/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi#L429-L538
The first two derivations set $\underline{Hom}( a, b ) = a^v \otimes b$ and thus in particular $\underline{Hom}( a, 1 ) = a^v \otimes 1$, while the last two derivations set $\underline{Hom}( a, 1 ) = a^v$. That is, the two interpretations differ by the right unitor. This gives the expected error in the following example:
gives
In addition to the missing right unitor, it would also be a good idea to use a single final derivation to install all four operations at once as in e.g. https://github.com/homalg-project/CAP_project/blob/master/MonoidalCategories/gap/HomomorphismStructureDerivedMethods.gi.
@TKuh Is this something you could have a look at?