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 336 operations for this category
which algorithmically
* IsCategoryWithDecidableColifts
* IsCategoryWithDecidableLifts
* IsEquippedWithHomomorphismStructure
* IsElementaryTopos
gap> C := UnderlyingCategory( FinBouquets );
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) )
gap> C_hat := FiniteColimitCompletionWithStrictCoproducts( C );
FiniteColimitCompletionWithStrictCoproducts(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )
gap> ModelingCategory( C_hat );
CoequalizerCompletion( FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) )
gap> Display( C_hat );
A CAP category with name
FiniteColimitCompletionWithStrictCoproducts(
PathCategory( FinQuiver( "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(
 PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )>
gap> L := C_hat.L;
<A projective object in FiniteColimitCompletionWithStrictCoproducts(
 PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )>
gap> b := C_hat.b;
<A morphism in FiniteColimitCompletionWithStrictCoproducts(
 PathCategory( FinQuiver( "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(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

[  ]

A morphism in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

[  ]

A morphism in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

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

An object in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

[  ]

A morphism in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

[  ]

A morphism in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteColimitCompletionWithStrictCoproducts(
PathCategory( FinQuiver( "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(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

[  ]

A morphism in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

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

An object in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "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(
PathCategory( FinQuiver( "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(
PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteColimitCompletionWithStrictCoproducts(
PathCategory( FinQuiver( "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", ">= 2024.09-09", false );
true
gap> FinBouquets;
FinBouquets
gap> Chat := ModelingCategory( FinBouquets );
FiniteCocompletion( PathCategory( FinQuiver( "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( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ), SkeletalFinSets )>
gap> source_coeq_pair := CoYonedaLemmaOnObjects( source_presheaf );
<An object in FiniteColimitCompletionWithStrictCoproducts(
 PathCategory( FinQuiver( "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( PathCategory(
FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteStrictCoproductCompletion( PathCategory(
FinQuiver( "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( PathCategory(
FinQuiver( "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( PathCategory(
FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteColimitCompletionWithStrictCoproducts(
PathCategory( FinQuiver( "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( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ), SkeletalFinSets )>
gap> target_coeq_pair := CoYonedaLemmaOnObjects( target_presheaf );
<An object in FiniteColimitCompletionWithStrictCoproducts(
 PathCategory( FinQuiver( "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( PathCategory(
FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteStrictCoproductCompletion( PathCategory(
FinQuiver( "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( PathCategory(
FinQuiver( "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( PathCategory(
FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

An object in FiniteColimitCompletionWithStrictCoproducts(
PathCategory( FinQuiver( "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( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ), SkeletalFinSets )>
gap> coeq_pair_morphism := CoYonedaLemmaOnMorphisms( presheaf_morphism );
<A morphism in FiniteColimitCompletionWithStrictCoproducts(
 PathCategory( FinQuiver( "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( PathCategory(
FinQuiver( "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( PathCategory(
FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data

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

A morphism in FiniteColimitCompletionWithStrictCoproducts(
PathCategory( FinQuiver( "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 );
PathCategory( FinQuiver(
"Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = id(C0) ]
gap> Size( Delta1 );
7
gap> PSh := PreSheaves( Delta1 );
PreSheaves( PathCategory( FinQuiver(
  "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
  / [ s⋅id = id(C0), t⋅id = id(C0) ],
SkeletalFinSets )
gap> Display( PSh.C1 );
Image of (C0):
{ 0, 1 }

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

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

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

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

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

An object in FiniteStrictCoproductCompletion( PathCategory(
FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data

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

An object in FiniteStrictCoproductCompletion( PathCategory(
FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data

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

[ [id(C1)]:(C1) -≻ (C1), [id(C1)]:(C1) -≻ (C1), [id(C0)]:(C0) -≻ (C0),
  [id(C0)]:(C0) -≻ (C0), [id(C0)]:(C0) -≻ (C0), [id(C0)]:(C0) -≻ (C0),
  [id(C0)]:(C0) -≻ (C0), [id(C0)]:(C0) -≻ (C0) ]

A morphism in FiniteStrictCoproductCompletion( PathCategory(
FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data

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

[ [id]:(C1) -≻ (C0), [id]:(C1) -≻ (C0), [s]:(C0) -≻ (C1), [s]:(C0) -≻ (C1),
  [s]:(C0) -≻ (C1), [t]:(C0) -≻ (C1), [t]:(C0) -≻ (C1), [t]:(C0) -≻ (C1) ]

A morphism in FiniteStrictCoproductCompletion( PathCategory(
FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data

An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ),
FiniteStrictCoproductCompletion( PathCategory(
FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = id(C0) ] ) ) given by the above data

An object in FiniteColimitCompletionWithStrictCoproducts(
PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = 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( PathCategory( FinQuiver(
 "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
 / [ s⋅id = id(C0), t⋅id = id(C0) ],
 SkeletalFinSets )>
gap> Display( coeq );
Image of (C0):
{ 0, 1 }

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

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

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

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

An object in PreSheaves( PathCategory( FinQuiver(
"Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = id(C0) ],
SkeletalFinSets ) given by the above data
gap> iso := Filtered( MorphismsOfExternalHom( PSh.C1, coeq ), IsIsomorphism )[1];
<An isomorphism in PreSheaves( PathCategory( FinQuiver(
 "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
 / [ s⋅id = id(C0), t⋅id = 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( PathCategory( FinQuiver(
"Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) )
/ [ s⋅id = id(C0), t⋅id = 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 166 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