Skip to content

Commit

Permalink
Added monoidal structure to AdditiveClosure
Browse files Browse the repository at this point in the history
  • Loading branch information
@damian-delafuente
damian-delafuente committed Sep 30, 2024
1 parent 6bbb7db commit 0ef4253
Show file tree
Hide file tree
Showing 2 changed files with 337 additions and 0 deletions.
75 changes: 75 additions & 0 deletions FreydCategoriesForCAP/examples/AdditiveClosureMonoidal.g
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
#! @Chapter Examples and Tests

#! @Section Monoidal structure of AdditiveClosure

#! @Example
LoadPackage( "FreydCategoriesForCAP", false );
#! true
T := TerminalCategoryWithMultipleObjects( );
#! TerminalCategoryWithMultipleObjects( )
A := "A" / T;
#! <A zero object in TerminalCategoryWithMultipleObjects( )>
B := "B" / T;
#! <A zero object in TerminalCategoryWithMultipleObjects( )>
AT := AdditiveClosure( T );
#! AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
ABAA := [ A, B, A, A ] / AT;
#! <An object in AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
#! defined by 4 underlying objects>
IsWellDefined( ABAA );
#! true
BAB := [ B, A, B ] / AT;
#! <An object in AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
#! defined by 3 underlying objects>
IsWellDefined( BAB );
#! true
mor_AB := MorphismConstructor( A, "A -> B", B );
#! <A zero, isomorphism in TerminalCategoryWithMultipleObjects( )>
mor_BA := MorphismConstructor( B, "B -> A", A );
#! <A zero, isomorphism in TerminalCategoryWithMultipleObjects( )>
id_A := IdentityMorphism( A );
#! <A zero, identity morphism in TerminalCategoryWithMultipleObjects( )>
id_B := IdentityMorphism( B );
#! <A zero, identity morphism in TerminalCategoryWithMultipleObjects( )>
alpha := MorphismConstructor( ABAA,
[ [ mor_AB, id_A, mor_AB ],
[ id_B, mor_BA, id_B ],
[ mor_AB, id_A, mor_AB ],
[ mor_AB, id_A, mor_AB ] ],
BAB );
#! <A morphism in AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
#! defined by a 4 x 3 matrix of underlying morphisms>
IsWellDefined( alpha );
#! true
alpha2 := TensorProduct( alpha, alpha );
#! <A morphism in AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
#! defined by a 16 x 9 matrix of underlying morphisms>
IsWellDefined( alpha2 );
#! true
IsIsomorphism( alpha2 );
#! true
left := LeftUnitor( ABAA );
#! <A morphism in AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
#! defined by a 4 x 4 matrix of underlying morphisms>
IsWellDefined( left );
#! true
left_inv := LeftUnitorInverse( ABAA );
#! <A morphism in AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
#! defined by a 4 x 4 matrix of underlying morphisms>
IsOne( PreCompose( left, left_inv ) );
#! true
IsOne( PreCompose( left_inv, left ) );
#! true
right := RightUnitor( BAB );
#! <A morphism in AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
#! defined by a 3 x 3 matrix of underlying morphisms>
IsWellDefined( right );
#! true
right_inv := RightUnitorInverse( BAB );
#! <A morphism in AdditiveClosure( TerminalCategoryWithMultipleObjects( ) )
#! defined by a 3 x 3 matrix of underlying morphisms>
IsOne( PreCompose( right, right_inv ) );
#! true
IsOne( PreCompose( right_inv, right ) );
#! true
#! @EndExample
262 changes: 262 additions & 0 deletions FreydCategoriesForCAP/gap/AdditiveClosure.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,12 @@ InstallMethod( ADDITIVE_CLOSURE,
fi;

fi;

if HasIsStrictMonoidalCategory( underlying_category ) and IsStrictMonoidalCategory( underlying_category ) then
SetIsStrictMonoidalCategory( category, true );
elif HasIsMonoidalCategory( underlying_category ) and IsMonoidalCategory( underlying_category ) then
SetIsMonoidalCategory( category, true );
fi;

INSTALL_FUNCTIONS_FOR_ADDITIVE_CLOSURE( category );

Expand Down Expand Up @@ -1356,6 +1362,262 @@ InstallGlobalFunction( INSTALL_FUNCTIONS_FOR_ADDITIVE_CLOSURE,

fi;

if HasIsMonoidalCategory( underlying_category ) and IsMonoidalCategory( underlying_category ) then

AddTensorUnit( category,
function( cat )
local underlying_category;

underlying_category := UnderlyingCategory( cat );

return ObjectConstructor( cat, [ TensorUnit ( underlying_category ) ] );

end );

AddTensorProductOnObjects( category,
function( cat, obj_1, obj_2 )
local underlying_category, objdat_1, objdat_2, len_1, len_2;

underlying_category := UnderlyingCategory( cat );
objdat_1 := ObjectDatum( cat, obj_1 );
objdat_2 := ObjectDatum( cat, obj_2 );
len_1 := Length( objdat_1 );
len_2 := Length( objdat_2 );

return ObjectConstructor( cat,
List( [ 0 .. len_1 * len_2 - 1 ], i ->
TensorProductOnObjects( underlying_category,
objdat_1[ QuoInt( i, len_2 ) + 1 ],
objdat_2[ RemInt( i, len_2 ) + 1 ] ) ) );

end );

AddTensorProductOnMorphismsWithGivenTensorProducts( category,
function( cat, source, morph_1, morph_2, target )
local underlying_category, source_list, target_list, source_1, source_2, target_1, target_2,
len_s1, len_s2, len_t1, len_t2, mat_1, mat_2, EntriesOfTensorProductMatrix;

underlying_category := UnderlyingCategory( cat );
source_list := ObjectDatum( cat, source );
target_list := ObjectDatum( cat, target );
source_1 := Source( morph_1 );
source_2 := Source( morph_2 );
target_1 := Target( morph_1 );
target_2 := Target( morph_2 );
len_s1 := Length( ObjectDatum( cat, source_1 ) );
len_s2 := Length( ObjectDatum( cat, source_2 ) );
len_t1 := Length( ObjectDatum( cat, target_1 ) );
len_t2 := Length( ObjectDatum( cat, target_2 ) );
mat_1 := MorphismDatum( cat, morph_1 );
mat_2 := MorphismDatum( cat, morph_2 );
EntriesOfTensorProductMatrix := function( i, j )
local underlyingmorph_1, underlyingmorph_2;

underlyingmorph_1 := mat_1[ QuoInt( i, len_s2 ) + 1 ][ QuoInt( j, len_t2 ) + 1 ];
underlyingmorph_2 := mat_2[ RemInt( i, len_s2 ) + 1 ][ RemInt( j, len_t2 ) + 1 ];

return TensorProductOnMorphismsWithGivenTensorProducts( underlying_category,
source_list[1 + len_s2 * QuoInt( i, len_s2 ) + RemInt( i, len_s2 )],
underlyingmorph_1,
underlyingmorph_2,
target_list[1 + len_t2 * QuoInt( j, len_t2 ) + RemInt( j, len_t2 )] );
end;

return MorphismConstructor( cat,
source,
List( [ 0 .. len_s1 * len_s2 - 1 ], i ->
List( [ 0 .. len_t1 * len_t2 - 1 ], j ->
EntriesOfTensorProductMatrix( i, j ) ) ),
target );
end );

if not ( HasIsStrictMonoidalCategory( underlying_category ) and IsStrictMonoidalCategory( underlying_category ) ) then


AddLeftUnitorWithGivenTensorProduct( category,
function( cat, obj, unit_tensor_obj )
local underlying_category, unit_tensor_obj_list, obj_list, rank, source_diagram, target_diagram;

underlying_category := UnderlyingCategory( cat );
unit_tensor_obj_list := ObjectDatum( cat, unit_tensor_obj );
obj_list := ObjectDatum( cat, obj );
rank := Length( obj_list );
source_diagram := List( [ 1 .. rank ], o -> ObjectConstructor( cat, [ unit_tensor_obj_list[ o ] ] ) );
target_diagram := List( [ 1 .. rank ], o -> ObjectConstructor( cat, [ obj_list[ o ] ] ) );

return DirectSumFunctorialWithGivenDirectSums( cat,
unit_tensor_obj,
source_diagram,
List( [ 1 .. rank ], o ->
MorphismConstructor( cat,
source_diagram[ o ],
[ [ LeftUnitorWithGivenTensorProduct( underlying_category,
obj_list[ o ],
unit_tensor_obj_list[ o ] ) ] ],
target_diagram[ o ] ) ),
target_diagram,
obj );

end );

AddLeftUnitorInverseWithGivenTensorProduct( category,
function( cat, obj, unit_tensor_obj )
local underlying_category, unit_tensor_obj_list, obj_list, rank, source_diagram, target_diagram;

underlying_category := UnderlyingCategory( cat );
unit_tensor_obj_list := ObjectDatum( cat, unit_tensor_obj );
obj_list := ObjectDatum( cat, obj );
rank := Length( obj_list );
source_diagram := List( [ 1 .. rank ], o -> ObjectConstructor( cat, [ obj_list[ o ] ] ) );
target_diagram := List( [ 1 .. rank ], o -> ObjectConstructor( cat, [ unit_tensor_obj_list[ o ] ] ) );

return DirectSumFunctorialWithGivenDirectSums( cat,
obj,
source_diagram,
List( [ 1 .. rank ], o ->
MorphismConstructor( cat,
source_diagram[ o ],
[ [ LeftUnitorInverseWithGivenTensorProduct( underlying_category,
obj_list[ o ],
unit_tensor_obj_list[ o ] ) ] ],
target_diagram[ o ] ) ),
target_diagram,
unit_tensor_obj );

end );

AddRightUnitorWithGivenTensorProduct( category,
function( cat, obj, obj_tensor_unit )
local underlying_category, obj_tensor_unit_list, obj_list, rank, source_diagram, target_diagram;

underlying_category := UnderlyingCategory( cat );
obj_tensor_unit_list := ObjectDatum( cat, obj_tensor_unit );
obj_list := ObjectDatum( cat, obj );
rank := Length( obj_list );
source_diagram := List( [ 1 .. rank ], o -> ObjectConstructor( cat, [ obj_tensor_unit_list[ o ] ] ) );
target_diagram := List( [ 1 .. rank ], o -> ObjectConstructor( cat, [ obj_list[ o ] ] ) );

return DirectSumFunctorialWithGivenDirectSums( cat,
obj_tensor_unit,
source_diagram,
List( [ 1 .. rank ], o ->
MorphismConstructor( cat,
source_diagram[ o ],
[ [ RightUnitorWithGivenTensorProduct( underlying_category,
obj_list[ o ],
obj_tensor_unit_list[ o ] ) ] ],
target_diagram[ o ] ) ),
target_diagram,
obj );

end );

AddRightUnitorInverseWithGivenTensorProduct( category,
function( cat, obj, obj_tensor_unit )
local underlying_category, obj_tensor_unit_list, obj_list, rank, source_diagram, target_diagram;

underlying_category := UnderlyingCategory( cat );
obj_tensor_unit_list := ObjectDatum( cat, obj_tensor_unit );
obj_list := ObjectDatum( cat, obj );
rank := Length( obj_list );
source_diagram := List( [ 1 .. rank ], o -> ObjectConstructor( cat, [ obj_list[ o ] ] ) );
target_diagram := List( [ 1 .. rank ], o -> ObjectConstructor( cat, [ obj_tensor_unit_list[ o ] ] ) );

return DirectSumFunctorialWithGivenDirectSums( cat,
obj,
source_diagram,
List( [ 1 .. rank ], o ->
MorphismConstructor( cat,
source_diagram[ o ],
[ [ RightUnitorInverseWithGivenTensorProduct( underlying_category,
obj_list[ o ],
obj_tensor_unit_list[ o ] ) ] ],
target_diagram[ o ] ) ),
target_diagram,
obj_tensor_unit );

end );

AddAssociatorLeftToRightWithGivenTensorProducts( category,
function( cat, source, obj_1, obj_2, obj_3, target )
local underlying_category, source_list, target_list, obj_list_1, obj_list_2, obj_list_3, len_1,
len_2, len_3, rank, source_diagram, target_diagram;

underlying_category := UnderlyingCategory( cat );
source_list := ObjectDatum( cat, source );
target_list := ObjectDatum( cat, target );
obj_list_1 := ObjectDatum( cat, obj_1 );
obj_list_2 := ObjectDatum( cat, obj_2 );
obj_list_3 := ObjectDatum( cat, obj_3 );
len_1 := Length( obj_list_1 );
len_2 := Length( obj_list_2 );
len_3 := Length( obj_list_3 );
rank := len_1 * len_2 * len_3;
source_diagram := List( [ 1 .. rank ], o ->
ObjectConstructor( cat, [ source_list[ o ] ] ) );
target_diagram := List( [ 1 .. rank ], o ->
ObjectConstructor( cat, [ target_list[ o ] ] ) );

return DirectSumFunctorialWithGivenDirectSums( cat,
source,
source_diagram,
List( [ 0 .. rank - 1 ], o ->
MorphismConstructor( cat,
source_diagram[1 + o],
[ [ AssociatorLeftToRightWithGivenTensorProducts( underlying_category,
source_list[1 + o],
obj_list_1[1 + QuoInt( o, len_2 * len_3 )],
obj_list_2[1 + RemInt( QuoInt( o, len_3 ), len_2 )],
obj_list_3[1 + RemInt( o, len_3 )],
target_list[1 + o] ) ] ],
target_diagram[1 + o] ) ),
target_diagram,
target );

end );

AddAssociatorRightToLeftWithGivenTensorProducts( category,
function( cat, source, obj_1, obj_2, obj_3, target )
local underlying_category, source_list, target_list, obj_list_1, obj_list_2, obj_list_3, len_1,
len_2, len_3, rank, source_diagram, target_diagram;

underlying_category := UnderlyingCategory( cat );
source_list := ObjectDatum( cat, source );
target_list := ObjectDatum( cat, target );
obj_list_1 := ObjectDatum( cat, obj_1 );
obj_list_2 := ObjectDatum( cat, obj_2 );
obj_list_3 := ObjectDatum( cat, obj_3 );
len_1 := Length( obj_list_1 );
len_2 := Length( obj_list_2 );
len_3 := Length( obj_list_3 );
rank := len_1 * len_2 * len_3;
source_diagram := List( [ 1 .. rank ], o ->
ObjectConstructor( cat, [ source_list[ o ] ] ) );
target_diagram := List( [ 1 .. rank ], o ->
ObjectConstructor( cat, [ target_list[ o ] ] ) );

return DirectSumFunctorialWithGivenDirectSums( cat,
source,
source_diagram,
List( [ 0 .. rank - 1 ], o ->
MorphismConstructor( cat,
source_diagram[1 + o],
[ [ AssociatorRightToLeftWithGivenTensorProducts( underlying_category,
source_list[1 + o],
obj_list_1[1 + QuoInt( o, len_2 * len_3 )],
obj_list_2[1 + RemInt( QuoInt( o, len_3 ), len_2 )],
obj_list_3[1 + RemInt( o, len_3 )],
target_list[1 + o] ) ] ],
target_diagram[1 + o] ) ),
target_diagram,
target );

end );

fi;

fi;

INSTALL_FUNCTIONS_OF_RANDOM_METHODS_FOR_ADDITIVE_CLOSURE( category );

end );
Expand Down

0 comments on commit 0ef4253

Please sign in to comment.