GAP (FiniteCocompletions) - Chapter 3: Finite strict coproduct completion of an object-finite category

Return the object-finite category \(C\) underlying the finite coproduct completion category UC := FiniteStrictCoproductCompletionOfObjectFiniteCategory( \(C\) )).

3.1-4 NumberOfObjectsOfUnderlyingCategory

Return the number of objects in the object-finite category \(C\) underlying the finite coproduct completion category UC := FiniteStrictCoproductCompletionOfObjectFiniteCategory( \(C\) )).

3.1-5 EmbeddingOfUnderlyingCategory

The full embedding functor from the object-finite category \(C\) underlying the finite coproduct completion PC into PC.

3.1-6 ExtendFunctorToFiniteStrictCoproductCompletionOfObjectFiniteCategory

The full embedding functor from the object-finite category \(C\) underlying the finite coproduct completion UC into UC.

3.2 Constructors

3.2-1 FiniteStrictCoproductCompletionOfObjectFiniteCategory

Return the finite coproduct completion of the object-finite category cat in which the cocartesian associators are given by identities.

gap> LoadPackage( "FiniteCocompletions", false );
true
gap> q := FinQuiver( "q(a,b,c)[m:a->b,n:b->c]" );
FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" )
gap> P := PathCategory( q : skeletal := true );
PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) )
gap> mUP := FiniteStrictCoproductCompletionOfObjectFiniteCategory( P );
FiniteStrictCoproductCompletionOfObjectFiniteCategory(
PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )
gap> a := mUP.a;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> b := mUP.b;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> c := mUP.c;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> m := mUP.m;
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> n := mUP.n;
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> PreCompose( m, n );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> x := [ 3, [ 1, 2, 0 ] ] / mUP;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> y := [ 6, [ 3, 2, 1 ] ] / mUP;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> ix := InjectionOfCofactorOfCoproduct( [ x, y ], 1 );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> iy := InjectionOfCofactorOfCoproduct( [ x, y ], 2 );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> u := UniversalMorphismFromCoproduct( [ ix, iy ] );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory(
 PathCategory( FinQuiver( "q(a,b,c)[m:a→b,n:b→c]" ) ) )>
gap> IsOne( u );
true
gap> IsWellDefined( u );
true

gap> LoadPackage( "FiniteCocompletions", false );
true
gap> q := FinQuiver( "q(M,A,B,J)[a:M->A,b:M->B,i:A->J,j:B->J]" );
FinQuiver( "q(M,A,B,J)[a:M→A,b:M→B,i:A→J,j:B→J]" )
gap> D := PathCategory( q );
PathCategory( FinQuiver( "q(M,A,B,J)[a:M→A,b:M→B,i:A→J,j:B→J]" ) )
gap> L := PosetOfCategory( D );
PosetOfCategory( PathCategory( \
FinQuiver( "q(M,A,B,J)[a:M→A,b:M→B,i:A→J,j:B→J]" ) ) )
gap> L.ai = L.bj;
true
gap> Perform( SetOfObjects( L ), Display );
(M)

An object in the poset given by the above data
(A)

An object in the poset given by the above data
(B)

An object in the poset given by the above data
(J)

An object in the poset given by the above data
gap> Ltilde := FiniteStrictCoproductCompletionOfObjectFiniteCategory( L );
FiniteStrictCoproductCompletionOfObjectFiniteCategory( PosetOfCategory( \
PathCategory( FinQuiver( "q(M,A,B,J)[a:M→A,b:M→B,i:A→J,j:B→J]" ) ) ) )
gap> Length( SetOfObjects( Ltilde ) );
16
gap> Lhat := PosetOfCategory( Ltilde );
PosetOfCategory( FiniteStrictCoproductCompletionOfObjectFiniteCategory( \
PosetOfCategory( PathCategory( \
FinQuiver( "q(M,A,B,J)[a:M→A,b:M→B,i:A→J,j:B→J]" ) ) ) ) )
gap> Display( Lhat );
A CAP category with name PosetOfCategory( \
FiniteStrictCoproductCompletionOfObjectFiniteCategory( PosetOfCategory( \
PathCategory( FinQuiver( "q(M,A,B,J)[a:M→A,b:M→B,i:A→J,j:B→J]" ) ) ) ) ):

10 primitive operations were used to derive 98 operations for this category which not yet algorithmically
* IsCategoryWithDecidableColifts
* IsCategoryWithDecidableLifts
* IsFiniteCategory
* IsEquippedWithHomomorphismStructure
* IsJoinSemiLattice

3.3 GAP categories

3.3-1 IsFiniteStrictCoproductCompletionOfObjectFiniteCategory

The GAP category of finite coproduct completions of object-finite categories.

3.3-2 IsCellInFiniteStrictCoproductCompletionOfObjectFiniteCategory

The GAP category of cells in a finite coproduct completion of an object-finite category.

3.3-3 IsObjectInFiniteStrictCoproductCompletionOfObjectFiniteCategory

The GAP category of objects in a finite coproduct completion of an object-finite category.

3.3-4 IsMorphismInFiniteStrictCoproductCompletionOfObjectFiniteCategory

The GAP category of morphisms in a finite coproduct completion of an object-finite category.

3.4 Examples

3.4-1 Colift along epimorphism

gap> LoadPackage( "FiniteCocompletions", false );
true
gap> T := TerminalCategoryWithSingleObject( );
TerminalCategoryWithSingleObject( )
gap> id_T := SetOfMorphisms( T )[1];;
gap> UTm := FiniteStrictCoproductCompletionOfObjectFiniteCategory( T );
FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalCategoryWithSin\
gleObject( ) )
gap> x := Pair( 5, [ 5 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> y := Pair( 3, [ 3 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> t := Pair( 2, [ 2 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> pi := MorphismConstructor(
>               x,
>               [ [ [ [ 0, 0, 0, 0, 0 ], [ 0, 0, 2, 1, 1 ] ] ],
>                 [ [ id_T, id_T, id_T, id_T, id_T ] ] ],
>               y );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> phi := MorphismConstructor(
>                x,
>                [ [ [ [ 0, 0, 0, 0, 0 ], [ 1, 1, 1, 0, 0 ] ] ],
>                  [ [ id_T, id_T, id_T, id_T, id_T ] ] ],
>                t );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> IsColiftableAlongEpimorphism( pi, phi );
true
gap> psi := ColiftAlongEpimorphism( pi, phi );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> Display( psi );
{ 0, 1, 2 } ⱶ[ [ [ 0, 0, 0 ], [ 1, 0, 1 ] ] ]→ { 0, 1 }

[ [ A morphism in TerminalCategoryWithSingleObject( ), 
    A morphism in TerminalCategoryWithSingleObject( ), 
    A morphism in TerminalCategoryWithSingleObject( ) ] ]
A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) ) given by the above data
gap> PreCompose( pi, psi ) = phi;
true
gap> x := Pair( 4, [ 4 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> y := Pair( 3, [ 3 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> pi := MorphismConstructor(
>               x,
>               [ [ [ [ 0, 0, 0, 0 ], [ 1, 0, 1, 2 ] ] ],
>                 [ [ id_T, id_T, id_T, id_T ] ] ],
>               y );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> IsColiftableAlongEpimorphism( pi, pi );
true
gap> psi := ColiftAlongEpimorphism( pi, pi );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> psi = IdentityMorphism( y );
true
gap> x := Pair( 4, [ 4 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> f := MorphismConstructor(
>              x,
>              [ [ [ [ 0, 0, 0, 0 ], [ 1, 3, 0, 2 ] ] ],
>                [ [ id_T, id_T, id_T, id_T ] ] ],
>              x );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> id_x := IdentityMorphism( x );
<An identity morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory\
( TerminalCategoryWithSingleObject( ) )>
gap> IsColiftableAlongEpimorphism( f, id_x );
true
gap> f_inv := ColiftAlongEpimorphism( f, id_x );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> PreCompose( f, f_inv ) = IdentityMorphism( x );
true
gap> x_1 := Pair( 4, [ 4 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> y_1 := Pair( 3, [ 3 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> t_1 := Pair( 2, [ 2 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> pi_1 := MorphismConstructor(
>                 x_1,
>                 [ [ [ [ 0, 0, 0, 0 ], [ 0, 0, 1, 2 ] ] ],
>                   [ [ id_T, id_T, id_T, id_T ] ] ],
>                 y_1 );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> phi_1 := MorphismConstructor(
>                  x_1,
>                  [ [ [ [ 0, 0, 0, 0 ], [ 1, 1, 0, 0 ] ] ],
>                    [ [ id_T, id_T, id_T, id_T ] ] ],
>                  t_1 );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> psi_1 := ColiftAlongEpimorphism( pi_1, phi_1 );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> x_2 := Pair( 2, [ 2 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> pi_2 := MorphismConstructor(
>                 x_2,
>                 [ [ [ [ 0, 0 ], [ 1, 0 ] ] ], [ [ id_T, id_T ] ] ],
>                 x_2 );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> phi_2 := IdentityMorphism( x_2 );
<An identity morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory\
( TerminalCategoryWithSingleObject( ) )>
gap> psi_2 := ColiftAlongEpimorphism( pi_2, phi_2 );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> pi := CoproductFunctorial( [ x_1, x_2 ], [ pi_1, pi_2 ], [ y_1, x_2 ] );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> phi := CoproductFunctorial( [ x_1, x_2 ], [ phi_1, phi_2 ], [ t_1, x_2 ] );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> psi_to_be :=
>   CoproductFunctorial( [ y_1, x_2 ], [ psi_1, psi_2 ], [ t_1, x_2 ] );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> psi_to_be = ColiftAlongEpimorphism( pi, phi );
true

3.4-2 Equalizer

gap> LoadPackage( "FiniteCocompletions", false );
true
gap> T := TerminalCategoryWithSingleObject( );
TerminalCategoryWithSingleObject( )
gap> id_T := SetOfMorphisms( T )[1];;
gap> UTm := FiniteStrictCoproductCompletionOfObjectFiniteCategory( T );
FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalCategoryWithSin\
gleObject( ) )
gap> x := Pair( 3, [ 3 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> f_1 := MorphismConstructor(
>                x,
>                [ [ [ [ 0, 0, 0 ], [ 1, 0, 2 ] ] ], [ [ id_T, id_T, id_T ] ] ],
>                x );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> f_2 := MorphismConstructor(
>                x,
>                [ [ [ [ 0, 0, 0 ], [ 0, 2, 1 ] ] ], [ [ id_T, id_T, id_T ] ] ],
>                x );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> D := [ f_1, f_2 ];;
gap> eq := Equalizer( D );
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> PairOfIntAndList( eq );
[ 0, [ 0 ] ]
gap> IsInitial( eq );
true
gap> i := EmbeddingOfEqualizer( x, D );
<A monomorphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Term\
inalCategoryWithSingleObject( ) )>
gap> IsCongruentForMorphisms( i, UniversalMorphismFromInitialObject( x ) );
true
gap> x := Pair( 3, [ 3 ] ) / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> f_1 := MorphismConstructor(
>                x,
>                [ [ [ [ 0, 0, 0 ], [ 1, 0, 2 ] ] ], [ [ id_T, id_T, id_T ] ] ],
>                x );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> f_2 := MorphismConstructor(
>                x,
>                [ [ [ [ 0, 0, 0 ], [ 1, 0, 1 ] ] ], [ [ id_T, id_T, id_T ] ] ],
>                x );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> D := [ f_1, f_2 ];;
gap> eq := Equalizer( D );
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> PairOfIntAndList( eq );
[ 2, [ 2 ] ]
gap> i := EmbeddingOfEqualizer( x, D );
<A monomorphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Term\
inalCategoryWithSingleObject( ) )>
gap> PairOfLists( i )[1];
[ [ [ 0, 0 ], [ 0, 1 ] ] ]
gap> t := [ 1, [ 1 ] ] / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> tau := MorphismConstructor( t, [ [ [ [ 0 ], [ 1 ] ] ], [ [ id_T ] ] ], x );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> l := UniversalMorphismIntoEqualizer( x, D, t, tau );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> PairOfLists( l )[1];
[ [ [ 0 ], [ 1 ] ] ]
gap> PreCompose( l, i ) = tau;
true
gap> x := [ 4, [ 4 ] ] / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> y := [ 3, [ 3 ] ] / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> f_1 := MorphismConstructor(
>                x,
>                [ [ [ [ 0, 0, 0, 0 ], [ 0, 0, 1, 2 ] ] ],
>                  [ [ id_T, id_T, id_T, id_T ] ] ],
>                y );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> f_2 := MorphismConstructor(
>                x,
>                [ [ [ [ 0, 0, 0, 0 ], [ 0, 0, 2, 2 ] ] ],
>                  [ [ id_T, id_T, id_T, id_T ] ] ],
>                y );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> f_3 := MorphismConstructor(
>                x,
>                [ [ [ [ 0, 0, 0, 0 ], [ 0, 0, 0, 2 ] ] ],
>                  [ [ id_T, id_T, id_T, id_T ] ] ],
>                y );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> D := [ f_1, f_2, f_3 ];;
gap> eq := Equalizer( D );
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> PairOfIntAndList( eq );
[ 3, [ 3 ] ]
gap> i := EmbeddingOfEqualizer( x, D );
<A monomorphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Term\
inalCategoryWithSingleObject( ) )>
gap> iD := List( D, m -> PreCompose( i, m ) );;
gap> ForAll( iD, m -> IsCongruentForMorphisms( m, First( iD ) ) );
true
gap> t := [ 2, [ 2 ] ] / UTm;
<An object in FiniteStrictCoproductCompletionOfObjectFiniteCategory( TerminalC\
ategoryWithSingleObject( ) )>
gap> tau := MorphismConstructor(
>                t,
>                [ [ [ [ 0, 0 ], [ 3, 1 ] ] ], [ [ id_T, id_T ] ] ],
>                x );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> l := UniversalMorphismIntoEqualizer( x, D, t, tau );
<A morphism in FiniteStrictCoproductCompletionOfObjectFiniteCategory( Terminal\
CategoryWithSingleObject( ) )>
gap> PairOfLists( l )[1];
[ [ [ 0, 0 ], [ 2, 1 ] ] ]
gap> PreCompose( l, i ) = tau;
true

3 Finite strict coproduct completion of an object-finite category

3.1 Attributes

3.1-1 PairOfIntAndList

3.1-2 PairOfLists

3.1-3 UnderlyingCategory