Coequalizer does not fulfill the equality specification

[zickgraf]

Using our current notion of equality of FinSets, we have FinSetNC( [ 1, 2 ] ) = FinSetNC( [ 2, 1 ] ) but AsList( FinSetNC( [ 1, 2 ] ) ) <> AsList( FinSetNC( [ 2, 1 ] ) ). In the algorithm for the coequalizer we build lists by iterating over AsList-attributes. Thus, these lists might be different although the FinSets in the input are equal.

For a concrete example, consider the following piece of code:

LoadPackage( "FinSetsForCAP" );

DeactivateCachingOfCategory( FinSets );

M := FinSetNC( [ 1, 2 ] );

phi1 := MapOfFinSets( M, [ [ 1, 1 ], [ 2, 2 ] ], M );
phi2 := MapOfFinSets( M, [ [ 1, 2 ], [ 2, 1 ] ], M );

D1 := [ phi1, phi2 ];

Cq1 := Coequalizer( D1 );

N := FinSetNC( [ 2, 1 ] );

tau1 := MapOfFinSets( N, [ [ 1, 1 ], [ 2, 2 ] ], N );
tau2 := MapOfFinSets( N, [ [ 1, 2 ], [ 2, 1 ] ], N );

D2 := [ tau1, tau2 ];

Cq2 := Coequalizer( D2 );

Display( D1 = D2 );
# true

Display( IsEqualForObjects( Cq1, Cq2 ) );
# false

Display( Cq1 );
# [ [ 1, 2 ] ]

Display( Cq2 );
# [ [ 2, 1 ] ]

I can think of three solutions to the problem:

1. use crisp caching instead of weak caching
2. take the order of elements into account, i.e., FinSetNC( [ 1, 2 ] ) <> FinSetNC( [ 2, 1 ] )
3. adapt the coequalizer: We think of the elements of the coequalizer as equivalence classes, i.e., there is no order defined on the elements. Thus, we should simply realize them as FinSets instead of lists.

My opinion: In my master thesis I have explicitly disabled the caching of FinSets, so 1. is not a solution for me. I think we should definitely do 3., since this is closer to our mathematical intuition than the current implementation. However, currently I have no idea how to check if this issue really only applies to the coequalizer and not to other constructions, too. Thus, we might want to think about 2. since this would solve the problem everywhere. Note that for users of FinSet (and not FinsSetNC) 2. would not change anything and the performance of IsEqualForObjects would be much better. However, we would then model the category of "tuples with pairwise different entries" instead of the category of finite sets.

[sebastianpos]

From a categorical point of view, solution 2 sounds perfect to me. You are actually still modeling the category of finite sets, since you just add more unequal but still isomorphic copies of your objects to the category.

[mohamed-barakat]

I agree with Sebastian, that the resulting category is still equivalent to the category of finite sets and would go for 2. The behaviour FinSetNC( [ 1, 2 ] ) <> FinSetNC( [ 2, 1 ] ) should be added to the documentation of FinSetNC.

[zickgraf]

I have just created pull request #21 which implements solution 2. @mohamed-barakat, please approve and/or merge it if you approve of the changes.