Added monoidal structure to AdditiveClosure

FreydCategoriesForCAP/gap/AdditiveClosure.gi

@@ -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 );
 
@@ -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_tensor_unit_list[ o ],
+                            obj_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 );