Goto Chapter: Top 1 2 3 4 5 6 7 8 9 10 11 12 13 14 Ind
 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 

8 The finite colimit completion of a category
 8.1 Attributes
 8.2 Constructors
 8.3 GAP categories
 8.4 Examples

8 The finite colimit completion of a category

8.1 Attributes

8.1-1 UnderlyingCategory
‣ UnderlyingCategory( C_hat )( attribute )

Return the category C underlying the category C_hat := FiniteColimitCompletionWithStrictCoproducts( C ).

8.1-2 FiniteStrictCoproductCompletionOfUnderlyingCategory
‣ FiniteStrictCoproductCompletionOfUnderlyingCategory( C_hat )( attribute )

Return the coproduct completion UC := FiniteStrictCoproductCompletion( C ) of the underlying category C, where C_hat := FiniteColimitCompletionWithStrictCoproducts( C ) \simeq CoequalizerCompletion( UC ).

8.1-3 PairOfObjectsAndPairOfParallelMorphisms
‣ PairOfObjectsAndPairOfParallelMorphisms( quiver )( attribute )

8.1-4 DefiningPairOfMorphismBetweenCoequalizerPairs
‣ DefiningPairOfMorphismBetweenCoequalizerPairs( quiver_morphism )( attribute )

8.1-5 CategoryOfColimitQuiversOfUnderlyingCategory
‣ CategoryOfColimitQuiversOfUnderlyingCategory( C_hat )( attribute )

Returns: a CAP category

The input is the finite colimit completion C_hat of a category C. The output is the category CategoryOfColimitQuivers( C ) of colimit quivers in C.

8.2 Constructors

8.2-1 FiniteColimitCompletionWithStrictCoproducts
‣ FiniteColimitCompletionWithStrictCoproducts( cat )( attribute )

Return the finite colimit completion of the category cat.

gap> LoadPackage( "FunctorCategories", ">= 2023.10-04", false );
true
gap> FinBouquets;
FinBouquets
gap> Display( FinBouquets );
A CAP category with name FinBouquets:

70 primitive operations were used to derive 338 operations for this category
which algorithmically
* IsCategoryWithDecidableColifts
* IsCategoryWithDecidableLifts
* IsEquippedWithHomomorphismStructure
* IsElementaryTopos
gap> C := UnderlyingCategory( FinBouquets );
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) )
gap> C_hat := FiniteColimitCompletionWithStrictCoproducts( C );
FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )
gap> ModelingCategory( C_hat );
CoequalizerCompletion( FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) )
gap> Display( C_hat );
A CAP category with name
FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ):

22 primitive operations were used to derive 64 operations for this category
which algorithmically
* IsCocartesianCategory
and not yet algorithmically
* IsFiniteCocompleteCategory
gap> MissingOperationsForConstructivenessOfCategory( C_hat, "IsFiniteCocompleteCategory" );
[ "UniversalMorphismFromCoequalizerWithGivenCoequalizer" ]
gap> P := C_hat.P;
<A projective object in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )>
gap> L := C_hat.L;
<A projective object in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )>
gap> b := C_hat.b;
<A morphism in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )>
gap> Source( b ) = P;
true
gap> Target( b ) = L;
true
gap> Display( P );
Image of <(V)>:
[ 1, [ <(P)> ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of <(A)>:
[ 0, [  ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(s)]->(A):
∅ ⱶ[  ]→ { 0 }

[  ]

A morphism in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(t)]->(A):
∅ ⱶ[  ]→ { 0 }

[  ]

A morphism in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ),
FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data

An object in FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data
gap> Display( L );
Image of <(V)>:
[ 1, [ <(L)> ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of <(A)>:
[ 0, [  ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(s)]->(A):
∅ ⱶ[  ]→ { 0 }

[  ]

A morphism in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(t)]->(A):
∅ ⱶ[  ]→ { 0 }

[  ]

A morphism in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ),
FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data

An object in FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data
gap> Display( b );
Image of <(V)>:
{ 0 } ⱶ[ 0 ]→ { 0 }

[ (P)-[(b)]->(L) ]

A morphism in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of <(A)>:
∅ ⱶ[  ]→ ∅

[  ]

A morphism in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

A morphism in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ),
FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data

A morphism in FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data
gap> inj := InjectionOfCofactorOfPushout( [ b, b ], 1 );
<A morphism in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )>
gap> IsWellDefined( inj );
true
gap> Source( inj ) = L;
true
gap> pushout := Target( inj );
<An object in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )>
gap> Display( pushout );
Image of <(V)>:
[ 3, [ <(L)>, <(L)>, <(P)> ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of <(A)>:
[ 2, [ <(P)>, <(P)> ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(s)]->(A):
{ 0, 1 } ⱶ[ 2, 2 ]→ { 0, 1, 2 }

[ (P)-[(P)]->(P), (P)-[(P)]->(P) ]

A morphism in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(t)]->(A):
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 }

[ (P)-[(b)]->(L), (P)-[(b)]->(L) ]

A morphism in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ),
FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data

An object in FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

8.2-2 CategoryOfPreSheavesOfUnderlyingCategory
‣ CategoryOfPreSheavesOfUnderlyingCategory( C_hat )( attribute )

Returns: a CAP category

Given the finite colimit completion category C_hat=FiniteColimitCompletionWithStrictCoproducts( C ) of a V-enriched category C, return the associated category PreSheaves( C, V ) of presheaves.

8.2-3 AssociatedColimitQuiver
‣ AssociatedColimitQuiver( coequalizer_object )( attribute )

Returns: a colimit quiver

The input is an object coequalizer_object in the category of finite colimit completion of a category. The output is the corresponding colimit quiver.

8.3 GAP categories

8.3-1 IsFiniteColimitCompletionWithStrictCoproducts
‣ IsFiniteColimitCompletionWithStrictCoproducts( arg )( filter )

Returns: true or false

The GAP category of colimit completions of categories.

8.3-2 IsCellInFiniteColimitCompletionWithStrictCoproducts
‣ IsCellInFiniteColimitCompletionWithStrictCoproducts( arg )( filter )

Returns: true or false

The GAP category of cells in the colimit completion of a category.

8.3-3 IsObjectInFiniteColimitCompletionWithStrictCoproducts
‣ IsObjectInFiniteColimitCompletionWithStrictCoproducts( arg )( filter )

Returns: true or false

The GAP category of objects in the colimit completion of a category.

8.3-4 IsMorphismInFiniteColimitCompletionWithStrictCoproducts
‣ IsMorphismInFiniteColimitCompletionWithStrictCoproducts( arg )( filter )

Returns: true or false

The GAP category of morphisms in the colimit completion of a category.

8.4 Examples

8.4-1 FinBouquets as finite colimit completion
gap> LoadPackage( "FunctorCategories", ">= 2023.11-07", false );
true
gap> FinBouquets;
FinBouquets
gap> Chat := ModelingCategory( FinBouquets );
FiniteCocompletion( FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )
gap> source_bouquet := CreateBouquet( 3, [ 0, 0, 1 ] );
<An object in FinBouquets>
gap> Display( source_bouquet );
( { 0, 1, 2 }, { 0 ↦ 0, 1 ↦ 0, 2 ↦ 1 } )
gap> source_presheaf := ModelingObject( Chat,
>                            ModelingObject( FinBouquets, source_bouquet ) );
<An object in
 PreSheaves( FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ), SkeletalFinSets )>
gap> source_coeq_pair := CoYonedaLemmaOnObjects( source_presheaf );
<An object in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )>
gap> IsWellDefined( source_coeq_pair );
true
gap> Display( source_coeq_pair );
Image of <(V)>:
[ 6, [ <(P)>, <(P)>, <(P)>, <(L)>, <(L)>, <(L)> ] ]

An object in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of <(A)>:
[ 3, [ <(P)>, <(P)>, <(P)> ] ]

An object in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(s)]->(A):
{ 0, 1, 2 } ⱶ[ 0, 0, 1 ]→ { 0,..., 5 }

[ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P) ]

A morphism in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(t)]->(A):
{ 0, 1, 2 } ⱶ[ 3, 4, 5 ]→ { 0,..., 5 }

[ (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L) ]

A morphism in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ),
FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data

An object in FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data
gap> target_bouquet := CreateBouquet( 2, [ 0, 0, 0, 0, 1 ] );
<An object in FinBouquets>
gap> Display( target_bouquet );
( { 0, 1 }, { 0 ↦ 0, 1 ↦ 0, 2 ↦ 0, 3 ↦ 0, 4 ↦ 1 } )
gap> target_presheaf := ModelingObject( Chat,
>                            ModelingObject( FinBouquets, target_bouquet ) );
<An object in
 PreSheaves( FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ), SkeletalFinSets )>
gap> target_coeq_pair := CoYonedaLemmaOnObjects( target_presheaf );
<An object in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )>
gap> Display( target_coeq_pair );
Image of <(V)>:
[ 7, [ <(P)>, <(P)>, <(L)>, <(L)>, <(L)>, <(L)>, <(L)> ] ]

An object in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of <(A)>:
[ 5, [ <(P)>, <(P)>, <(P)>, <(P)>, <(P)> ] ]

An object in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(s)]->(A):
{ 0,..., 4 } ⱶ[ 0, 0, 0, 0, 1 ]→ { 0,..., 6 }

[ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P) ]

A morphism in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of (V)-[(t)]->(A):
{ 0,..., 4 } ⱶ[ 2, 3, 4, 5, 6 ]→ { 0,..., 6 }

[ (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L) ]

A morphism in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ),
FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data

An object in FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data
gap> bouquet_morphism := CreateBouquetMorphism(
>                             source_bouquet,
>                             [ 0, 1, 1 ], [ 1, 3, 4 ],
>                             target_bouquet );
<A morphism in FinBouquets>
gap> IsWellDefined( bouquet_morphism );
true
gap> presheaf_morphism := ModelingMorphism( Chat,
>                              ModelingMorphism( FinBouquets, bouquet_morphism ) );
<A morphism in
 PreSheaves( FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ), SkeletalFinSets )>
gap> coeq_pair_morphism := CoYonedaLemmaOnMorphisms( presheaf_morphism );
<A morphism in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) )>
gap> IsWellDefined( coeq_pair_morphism );
true
gap> Display( coeq_pair_morphism );
Image of <(V)>:
{ 0,..., 5 } ⱶ[ 0, 1, 1, 3, 5, 6 ]→ { 0,..., 6 }

[ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P),
  (L)-[(L)]->(L), (L)-[(L)]->(L), (L)-[(L)]->(L) ]

A morphism in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

Image of <(A)>:
{ 0, 1, 2 } ⱶ[ 1, 3, 4 ]→ { 0,..., 4 }

[ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P) ]

A morphism in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

A morphism in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ),
FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data

A morphism in FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data

8.4-2 FinReflexiveQuivers as finite colimit completion
gap> LoadPackage( "FunctorCategories", ">= 2023.11-07", false );
true
gap> Delta1 := SimplicialCategoryTruncatedInDegree( 1 );
FreeCategory( RightQuiver(
"Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ]
gap> Size( Delta1 );
7
gap> PSh := PreSheaves( Delta1 );
PreSheaves( FreeCategory( RightQuiver(
  "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ],
SkeletalFinSets )
gap> Display( PSh.C1 );
Image of <(C0)>:
{ 0, 1 }

Image of <(C1)>:
{ 0, 1, 2 }

Image of (C1)-[(id)]->(C0):
{ 0, 1 } ⱶ[ 1, 2 ]→ { 0, 1, 2 }

Image of (C0)-[(s)]->(C1):
{ 0, 1, 2 } ⱶ[ 0, 0, 1 ]→ { 0, 1 }

Image of (C0)-[(t)]->(C1):
{ 0, 1, 2 } ⱶ[ 1, 0, 1 ]→ { 0, 1 }

An object in PreSheaves( FreeCategory( RightQuiver(
"Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ],
SkeletalFinSets ) given by the above data
gap> coeq_pair := CoYonedaLemmaOnObjects( PSh.C1 );
<An object in FiniteColimitCompletionWithStrictCoproducts(
 FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) )
 / [ s*id = C0, t*id = C0 ] )>
gap> Display( coeq_pair );
Image of <(V)>:
[ 5, [ <(C0)>, <(C0)>, <(C1)>, <(C1)>, <(C1)> ] ]

An object in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) )
/ [ s*id = C0, t*id = C0 ] ) given by the above data

Image of <(A)>:
[ 8, [ <(C1)>, <(C1)>, <(C0)>, <(C0)>, <(C0)>, <(C0)>, <(C0)>, <(C0)> ] ]

An object in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) )
/ [ s*id = C0, t*id = C0 ] ) given by the above data

Image of (V)-[(s)]->(A):
{ 0,..., 7 } ⱶ[ 3, 4, 0, 0, 1, 1, 0, 1 ]→ { 0,..., 4 }

[ (C1)-[(C1)]->(C1), (C1)-[(C1)]->(C1), (C0)-[(C0)]->(C0), (C0)-[(C0)]->(C0),
  (C0)-[(C0)]->(C0), (C0)-[(C0)]->(C0), (C0)-[(C0)]->(C0), (C0)-[(C0)]->(C0) ]

A morphism in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) )
/ [ s*id = C0, t*id = C0 ] ) given by the above data

Image of (V)-[(t)]->(A):
{ 0,..., 7 } ⱶ[ 0, 1, 2, 3, 4, 2, 3, 4 ]→ { 0,..., 4 }

[ (C1)-[(id)]->(C0), (C1)-[(id)]->(C0), (C0)-[(s)]->(C1), (C0)-[(s)]->(C1),
  (C0)-[(s)]->(C1), (C0)-[(t)]->(C1), (C0)-[(t)]->(C1), (C0)-[(t)]->(C1) ]

A morphism in FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) )
/ [ s*id = C0, t*id = C0 ] ) given by the above data

An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ),
FiniteStrictCoproductCompletion( FreeCategory(
RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) )
/ [ s*id = C0, t*id = C0 ] ) ) given by the above data

An object in FiniteColimitCompletionWithStrictCoproducts(
FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) )
/ [ s*id = C0, t*id = C0 ] ) given by the above data
gap> IsWellDefined( coeq_pair );
true
gap> coeq_pair_in_presheaves := CoYonedaLemmaCoequalizerPair( PSh.C1 );;
gap> coeq := Coequalizer( coeq_pair_in_presheaves[2] );
<An object in PreSheaves( FreeCategory( RightQuiver(
 "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ],
 SkeletalFinSets )>
gap> Display( coeq );
Image of <(C0)>:
{ 0, 1 }

Image of <(C1)>:
{ 0, 1, 2 }

Image of (C1)-[(id)]->(C0):
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 }

Image of (C0)-[(s)]->(C1):
{ 0, 1, 2 } ⱶ[ 0, 1, 0 ]→ { 0, 1 }

Image of (C0)-[(t)]->(C1):
{ 0, 1, 2 } ⱶ[ 0, 1, 1 ]→ { 0, 1 }

An object in PreSheaves( FreeCategory( RightQuiver(
"Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ],
SkeletalFinSets ) given by the above data
gap> iso := Filtered( MorphismsOfExternalHom( PSh.C1, coeq ), IsIsomorphism )[1];
<An isomorphism in PreSheaves( FreeCategory( RightQuiver(
 "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ],
 SkeletalFinSets )>
gap> Display( iso );
Image of <(C0)>:
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 }

Image of <(C1)>:
{ 0, 1, 2 } ⱶ[ 2, 0, 1 ]→ { 0, 1, 2 }

A morphism in PreSheaves( FreeCategory( RightQuiver(
"Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ],
SkeletalFinSets ) given by the above data

8.4-3 Free elementary topos on one object
gap> LoadPackage( "FunctorCategories" );
true
gap> SkeletalFinBool := Opposite( SkeletalFinSets );
Opposite( SkeletalFinSets )
gap> FreeTopos1 := FiniteColimitCompletionWithStrictCoproducts( SkeletalFinBool );
FiniteColimitCompletionWithStrictCoproducts( Opposite( SkeletalFinSets ) )
gap> Display( FreeTopos1 );
A CAP category with name
FiniteColimitCompletionWithStrictCoproducts( Opposite( SkeletalFinSets ) ):

27 primitive operations were used to derive 103 operations for this category
which algorithmically
* IsBicartesianCategory
and not yet algorithmically
* IsFiniteCocompleteCategory
gap> MissingOperationsForConstructivenessOfCategory( FreeTopos1, "IsFiniteCocompleteCategory" );
[ "UniversalMorphismFromCoequalizerWithGivenCoequalizer" ]
gap> Poly := FiniteStrictCoproductCompletionOfUnderlyingCategory( FreeTopos1 );
FiniteStrictCoproductCompletion( Opposite( SkeletalFinSets ) )
gap> Display( Poly );
A CAP category with name
FiniteStrictCoproductCompletion( Opposite( SkeletalFinSets ) ):

33 primitive operations were used to derive 173 operations for this category
which algorithmically
* IsCategoryWithDecidableColifts
* IsCategoryWithDecidableLifts
* IsEquippedWithHomomorphismStructure
* IsFiniteCompleteCategory
* IsDistributiveCategory
and furthermore mathematically
* IsStrictCartesianCategory
* IsStrictCocartesianCategory
 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 
Goto Chapter: Top 1 2 3 4 5 6 7 8 9 10 11 12 13 14 Ind

generated by GAPDoc2HTML