‣ UnderlyingCategory( C_hat ) | ( attribute ) |
Return the category \(C\) underlying the category C_hat := FiniteColimitCompletionWithStrictCoproducts( \(C\) ).
‣ FiniteStrictCoproductCompletionOfUnderlyingCategory( C_hat ) | ( attribute ) |
Return the coproduct completion \(UC :=\) FiniteStrictCoproductCompletion( \(C\) ) of the underlying category \(C\), where C_hat := FiniteColimitCompletionWithStrictCoproducts( \(C\) ) \(\simeq\) CoequalizerCompletion( \(UC\) ).
‣ PairOfObjectsAndPairOfParallelMorphisms( quiver ) | ( attribute ) |
‣ DefiningPairOfMorphismBetweenCoequalizerPairs( quiver_morphism ) | ( attribute ) |
‣ 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\).
‣ 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 330 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
‣ 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.
‣ 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.
‣ IsFiniteColimitCompletionWithStrictCoproducts( arg ) | ( filter ) |
Returns: true or false
The GAP category of colimit completions of categories.
‣ IsCellInFiniteColimitCompletionWithStrictCoproducts( arg ) | ( filter ) |
Returns: true or false
The GAP category of cells in the colimit completion of a category.
‣ IsObjectInFiniteColimitCompletionWithStrictCoproducts( arg ) | ( filter ) |
Returns: true or false
The GAP category of objects in the colimit completion of a category.
‣ IsMorphismInFiniteColimitCompletionWithStrictCoproducts( arg ) | ( filter ) |
Returns: true or false
The GAP category of morphisms in the colimit completion of a category.
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
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
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
generated by GAPDoc2HTML