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] 

1 Finite strict coproduct cocompletion
 1.1 Attributes
 1.2 Constructors
 1.3 GAP categories
 1.4 Examples

1 Finite strict coproduct cocompletion

1.1 Attributes

1.1-1 PairOfIntAndList
‣ PairOfIntAndList( arg )( attribute )

1.1-2 PairOfLists
‣ PairOfLists( arg )( attribute )

1.1-3 UnderlyingCategory
‣ UnderlyingCategory( UC )( attribute )

Return the category \(C\) underlying the finite coproduct cocompletion category UC := FiniteStrictCoproductCompletion( \(C\) ).

1.1-4 EmbeddingOfUnderlyingCategory
‣ EmbeddingOfUnderlyingCategory( UC )( attribute )

Returns: a CAP functor

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

1.1-5 ExtendFunctorToFiniteStrictCoproductCompletion
‣ ExtendFunctorToFiniteStrictCoproductCompletion( UC )( attribute )

Returns: a CAP functor

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

1.1-6 ExtendEmbeddingToFiniteStrictCoproductCompletion
‣ ExtendEmbeddingToFiniteStrictCoproductCompletion( C )( attribute )

Returns: a CAP functor

Extend (i.e., lift) the (full) embedding the category C into PreSheaves( C ) to the full embedding of FiniteStrictCoproductCompletion( C ) into PreSheaves( C ).

1.2 Constructors

1.2-1 FiniteStrictCoproductCompletion
‣ FiniteStrictCoproductCompletion( cat )( attribute )

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

gap> LoadPackage( "FiniteCocompletions" );
true
gap> T := FiniteStrictCoproductCompletion( InitialCategory( ) );
FiniteStrictCoproductCompletion( InitialCategory( ) )
gap> Display( T );
A CAP category with name FiniteStrictCoproductCompletion( InitialCategory( ) ):

126 primitive operations were used to derive 687 operations for this category
which algorithmically
* IsCategoryWithDecidableColifts
* IsCategoryWithDecidableLifts
* IsFiniteCategory
* IsEquippedWithHomomorphismStructure
* IsLinearCategoryOverCommutativeRing
* IsLeftClosedMonoidalCategory
* IsLeftCoclosedMonoidalCategory
* IsRigidSymmetricClosedMonoidalCategory
* IsRigidSymmetricCoclosedMonoidalCategory
* IsAbelianCategoryWithEnoughInjectives
* IsAbelianCategoryWithEnoughProjectives
* IsAdditiveMonoidalCategory
* IsElementaryTopos
* IsSymmetricClosedMonoidalLattice
* IsSymmetricCoclosedMonoidalLattice
* IsBooleanAlgebra
and not yet algorithmically
* IsLinearCategoryOverCommutativeRingWithFinitelyGeneratedFreeExternalHoms
and furthermore mathematically
* IsFinitelyPresentedLinearCategory
* IsLinearClosureOfACategory
* IsLocallyOfFiniteInjectiveDimension
* IsLocallyOfFiniteProjectiveDimension
* IsStableProset
* IsSymmetricMonoidalCategoryStructureGivenByCoproduct
* IsSymmetricMonoidalCategoryStructureGivenByDirectProduct
* IsTerminalCategory
* IsTotalOrderCategory
gap> i := InitialObject( T );
<A zero object in FiniteStrictCoproductCompletion( InitialCategory( ) )>
gap> t := TerminalObject( T );
<A zero object in FiniteStrictCoproductCompletion( InitialCategory( ) )>
gap> z := ZeroObject( T );
<A zero object in FiniteStrictCoproductCompletion( InitialCategory( ) )>
gap> Display( i );
[ 0, [  ] ]

An object in FiniteStrictCoproductCompletion( InitialCategory( ) )
given by the above data
gap> Display( t );
[ 0, [  ] ]

An object in FiniteStrictCoproductCompletion( InitialCategory( ) )
given by the above data
gap> Display( z );
[ 0, [  ] ]

An object in FiniteStrictCoproductCompletion( InitialCategory( ) )
given by the above data
gap> IsEqualForObjects( i, z );
true
gap> IsIdenticalObj( i, z );
false
gap> IsEqualForObjects( t, z );
true
gap> IsIdenticalObj( t, z );
false
gap> IsWellDefined( z );
true
gap> id_z := IdentityMorphism( z );
<A zero, identity morphism in
 FiniteStrictCoproductCompletion( InitialCategory( ) )>
gap> fn_z := ZeroObjectFunctorial( T );
<A zero, isomorphism in FiniteStrictCoproductCompletion( InitialCategory( ) )>
gap> IsWellDefined( fn_z );
true
gap> IsEqualForMorphisms( id_z, fn_z );
true
gap> IsCongruentForMorphisms( id_z, fn_z );
true
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> UC := FiniteStrictCoproductCompletion(
>                  UnderlyingCategory( FinBouquets ) );
FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) )
gap> P := UC.P;
<An object in FiniteStrictCoproductCompletion(
 PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) )>
gap> Display( P );
[ 1, [ <(P)> ] ]

An object in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) ) given by the above data
gap> L := UC.L;
<An object in FiniteStrictCoproductCompletion(
 PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) )>
gap> Display( L );
[ 1, [ <(L)> ] ]

An object in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) ) given by the above data
gap> b := UC.b;
<A morphism in FiniteStrictCoproductCompletion(
 PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) )>
gap> Display( b );
{ 0 } ⱶ[ 0 ]→ { 0 }

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

A morphism in FiniteStrictCoproductCompletion(
PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) ) given by the above data
gap> HomStructure( UC );
|1|
gap> HomStructure( P, L );
|1|
gap> homPL := MorphismsOfExternalHom( P, L );
[ <A morphism in FiniteStrictCoproductCompletion(
   PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) )> ]
gap> List( homPL, m -> HomStructure( P, L, HomStructure( m ) ) = m );
[ true ]
gap> HomStructure( b, b );
|0| → |1|
gap> HomStructure( b, L );
|1| → |1|
gap> HomStructure( P, b );
|1| → |1|
gap> M := Coproduct( P, L, P );
<An object in FiniteStrictCoproductCompletion(
 PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) )>
gap> N := Coproduct( L, P, L );
<An object in FiniteStrictCoproductCompletion(
 PathCategory( FinQuiver( "q(P,L)[b:P→L]" ) ) )>
gap> HomStructure( M, N );
|18|
gap> HomStructure( P, L );
|1|
gap> homMN := MorphismsOfExternalHom( M, N );;
gap> List( homMN, m -> HomStructure( M, N, HomStructure( m ) ) = m );
[ true, true, true, true, true, true, true, true, true,
  true, true, true, true, true, true, true, true, 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 := FiniteStrictCoproductCompletion( L );
FiniteStrictCoproductCompletion( 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( FiniteStrictCoproductCompletion( PosetOfCategory( \
PathCategory( FinQuiver( "q(M,A,B,J)[a:M→A,b:M→B,i:A→J,j:B→J]" ) ) ) ) )
gap> Lhat_objs := SetOfObjects( Lhat );; Length( Lhat_objs );
6
gap> M := Lhat.M;
An object in the poset given by: \
<An object in FiniteStrictCoproductCompletion( PosetOfCategory( \
PathCategory( FinQuiver( "q(M,A,B,J)[a:M→A,b:M→B,i:A→J,j:B→J]" ) ) ) )>
gap> A := Lhat.A;;
gap> B := Lhat.B;;
gap> J := Lhat.J;;
gap> I := InitialObject( Lhat );;
gap> C := Coproduct( Lhat.A, Lhat.B );;
gap> I = M;
false
gap> C = J;
false
gap> Lhat_objs = [ I, M, A, B, J, C ];
true

1.3 GAP categories

1.3-1 IsFiniteStrictCoproductCompletion
‣ IsFiniteStrictCoproductCompletion( arg )( filter )

Returns: true or false

The GAP category of finite coproduct cocompletion categories.

1.3-2 IsCellInFiniteStrictCoproductCompletion
‣ IsCellInFiniteStrictCoproductCompletion( arg )( filter )

Returns: true or false

The GAP category of cells in a finite coproduct cocompletion category.

1.3-3 IsObjectInFiniteStrictCoproductCompletion
‣ IsObjectInFiniteStrictCoproductCompletion( arg )( filter )

Returns: true or false

The GAP category of objects in a finite coproduct cocompletion category.

1.3-4 IsMorphismInFiniteStrictCoproductCompletion
‣ IsMorphismInFiniteStrictCoproductCompletion( arg )( filter )

Returns: true or false

The GAP category of morphisms in a finite coproduct cocompletion category.

1.4 Examples

1.4-1 Cocartesian associator
gap> LoadPackage( "FiniteCocompletions" );
true
gap> LoadPackage( "Algebroids" );
true
gap> LoadPackage( "LazyCategories", ">= 2023.01-02" );
true
gap> Q := RightQuiver( "Q(a,b,c)[]" );
Q(a,b,c)[]
gap> C := FreeCategory( Q );
FreeCategory( RightQuiver( "Q(a,b,c)[]" ) )
gap> UC := FiniteStrictCoproductCompletion( C );
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )
gap> a := UC.a;
<An object in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )>
gap> b := UC.b;
<An object in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )>
gap> c := UC.c;
<An object in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )>
gap> ab_c := Coproduct( Coproduct( a, b ), c );
<An object in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )>
gap> a_bc := Coproduct( a, Coproduct( b, c ) );
<An object in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )>
gap> ab_c = a_bc;
true
gap> HomStructure( ab_c, a_bc );
|1|
gap> hom := MorphismsOfExternalHom( ab_c, a_bc );
[ <A morphism in FiniteStrictCoproductCompletion(
   FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )> ]
gap> alpha := hom[1];
<A morphism in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )>
gap> Source( alpha ) = ab_c;
true
gap> IsOne( alpha );
true
gap> IsWellDefined( alpha );
true
gap> alpha = CocartesianAssociatorLeftToRight( a, b, c );
true
gap> LUC := LazyCategory( UC );
LazyCategory(
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) ) )
gap> Emb := EmbeddingFunctorOfUnderlyingCategory( LUC );
Embedding functor into lazy category
gap> Display( Emb );
Embedding functor into lazy category:

FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )
  |
  V
LazyCategory(
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) ) )
gap> F := PreCompose( EmbeddingOfUnderlyingCategory( UC ), Emb );
Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category
gap> Display( F );
Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category:

FreeCategory( RightQuiver( "Q(a,b,c)[]" ) )
  |
  V
LazyCategory(
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) ) )
gap> G := ExtendFunctorToFiniteStrictCoproductCompletion( F );
Extension to FiniteStrictCoproductCompletion( Source( Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category ) )
gap> Display( G );
Extension to FiniteStrictCoproductCompletion( Source( Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category ) ):

FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) )
  |
  V
LazyCategory( FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) ) )
gap> Galpha := G( alpha );
<A morphism in LazyCategory( FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(a,b,c)[]" ) ) ) )>
gap> IsWellDefined( Galpha );
true

1.4-2 Cocartesian braiding
gap> LoadPackage( "FiniteCocompletions" );
true
gap> LoadPackage( "Algebroids" );
true
gap> LoadPackage( "LazyCategories", ">= 2023.01-02" );
true
gap> Q := RightQuiver( "Q(a,b)[]" );
Q(a,b)[]
gap> C := FreeCategory( Q );
FreeCategory( RightQuiver( "Q(a,b)[]" ) )
gap> SetName( C.a, "C.a" ); SetName( C.b, "C.b" );
gap> UC := FiniteStrictCoproductCompletion( C );
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
gap> a := UC.a;
<An object in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )>
gap> b := UC.b;
<An object in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )>
gap> ab := Coproduct( a, b );
<An object in
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )>
gap> Display( ab );
[ 2, [ C.a, C.b ] ]

An object in
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
given by the above data
gap> ba := Coproduct( b, a );
<An object in
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )>
gap> Display( ba );
[ 2, [ C.b, C.a ] ]

An object in
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
given by the above data
gap> HomStructure( ab, ba );
|1|
gap> hom := MorphismsOfExternalHom( ab, ba );
[ <A morphism in FiniteStrictCoproductCompletion(
   FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )> ]
gap> gamma := hom[1];
<A morphism in
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )>
gap> Source( gamma ) = ab;
true
gap> Target( gamma ) = ba;
true
gap> IsWellDefined( gamma );
true
gap> Display( gamma );
{ 0, 1 } ⱶ[ 1, 0 ]→ { 0, 1 }

[ (a)-[(a)]->(a), (b)-[(b)]->(b) ]

A morphism in
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
given by the above data
gap> LUC := LazyCategory( UC );
LazyCategory(
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) ) )
gap> Emb := EmbeddingFunctorOfUnderlyingCategory( LUC );
Embedding functor into lazy category
gap> Display( Emb );
Embedding functor into lazy category:

FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
  |
  V
LazyCategory(
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) ) )
gap> F := PreCompose( EmbeddingOfUnderlyingCategory( UC ), Emb );
Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category
gap> Display( F );
Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category:

FreeCategory( RightQuiver( "Q(a,b)[]" ) )
  |
  V
LazyCategory(
FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) ) )
gap> G := ExtendFunctorToFiniteStrictCoproductCompletion( F );
Extension to FiniteStrictCoproductCompletion( Source( Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category ) )
gap> Display( G );
Extension to FiniteStrictCoproductCompletion( Source( Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category ) ):

FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
  |
  V
LazyCategory( FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "Q(a,b)[]" ) ) ) )
gap> Ggamma := G( gamma );
<A morphism in LazyCategory(
 FiniteStrictCoproductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) ) )>
gap> IsWellDefined( Ggamma );
true

1.4-3 Cocartesian codiagonal
gap> LoadPackage( "FiniteCocompletions" );
true
gap> LoadPackage( "Algebroids" );
true
gap> LoadPackage( "LazyCategories", ">= 2023.01-02" );
true
gap> Q := FinQuiver( "Q(a)[]" );
FinQuiver( "Q(a)[]" )
gap> C := PathCategory( Q );
PathCategory( FinQuiver( "Q(a)[]" ) )
gap> SetName( C.a, "C.a" );
gap> UC := FiniteStrictCoproductCompletion( C );
FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
gap> a := UC.a;
<An object in
 FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )>
gap> aa := Coproduct( a, a );
<An object in
 FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )>
gap> Display( aa );
[ 2, [ C.a, C.a ] ]

An object in
FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
given by the above data
gap> a = aa;
false
gap> HomStructure( a, aa );
|2|
gap> hom_a_aa := MorphismsOfExternalHom( a, aa );
[ <A morphism in
   FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )>,
  <A morphism in
   FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )> ]
gap> hom_a_aa[1] = InjectionOfCofactorOfCoproduct( [ a, a ], 1 );
true
gap> hom_a_aa[2] = InjectionOfCofactorOfCoproduct( [ a, a ], 2 );
true
gap> HomStructure( aa, a );
|1|
gap> hom_aa_a := MorphismsOfExternalHom( aa, a );
[ <A morphism in
   FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )> ]
gap> delta := hom_aa_a[1];
<A morphism in
 FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )>
gap> Source( delta ) = aa;
true
gap> Target( delta ) = a;
true
gap> IsOne( ComponentOfMorphismFromCoproduct( delta, [ a, a ], 1 ) );
true
gap> IsOne( ComponentOfMorphismFromCoproduct( delta, [ a, a ], 2 ) );
true
gap> IsWellDefined( delta );
true
gap> Display( delta );
{ 0, 1 } ⱶ[ 0, 0 ]→ { 0 }

[ id(a):C.a → C.a, id(a):C.a → C.a ]

A morphism in
FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
given by the above data
gap> id_a := IdentityMorphism( C.a );
id(a):C.a → C.a
gap> delta = CocartesianCodiagonal( a, 2 );
true
gap> CellAsEvaluatableString( delta, [ "C", "UC" ] );
"MorphismConstructor( UC,
        ObjectConstructor( UC,
                Pair( 2,
                      [ ObjectConstructor( C, 1 ),
                        ObjectConstructor( C, 1 ) ] ) ),
        Pair( [ 0, 0 ],
              [ IdentityMorphism( C, ObjectConstructor( C, 1 ) ),
                IdentityMorphism( C, ObjectConstructor( C, 1 ) ) ] ),
        ObjectConstructor( UC,
                Pair( 1, [ ObjectConstructor( C, 1 ) ] ) ) )"
gap> LUC := LazyCategory( UC );
LazyCategory(
FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) ) )
gap> Emb := EmbeddingFunctorOfUnderlyingCategory( LUC );
Embedding functor into lazy category
gap> Display( Emb );
Embedding functor into lazy category:

FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
  |
  V
LazyCategory(
FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) ) )
gap> F := PreCompose( EmbeddingOfUnderlyingCategory( UC ), Emb );
Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category
gap> Display( F );
Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category:

PathCategory( FinQuiver( "Q(a)[]" ) )
  |
  V
LazyCategory(
FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) ) )
gap> G := ExtendFunctorToFiniteStrictCoproductCompletion( F );
Extension to FiniteStrictCoproductCompletion( Source( Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category ) )
gap> Display( G );
Extension to FiniteStrictCoproductCompletion( Source( Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category ) ):

FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
  |
  V
LazyCategory(
FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) ) )
gap> Gdelta := G( delta );
<A morphism in LazyCategory(
 FiniteStrictCoproductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) ) )>
gap> IsWellDefined( Gdelta );
true

1.4-4 Homomorphism structure
gap> LoadPackage( "FiniteCocompletions" );
true
gap> T := TerminalCategoryWithMultipleObjects( );
TerminalCategoryWithMultipleObjects( )
gap> sFinSets := FiniteStrictCoproductCompletion( T );
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
gap> Display( sFinSets );
A CAP category with name
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) ):

35 primitive operations were used to derive 165 operations for this category
which algorithmically
* IsCategoryWithDecidableColifts
* IsCategoryWithDecidableLifts
* IsEquippedWithHomomorphismStructure
* IsFiniteCompleteCategory
* IsDistributiveCategory
and furthermore mathematically
* IsStrictCocartesianCategory
gap> t := TerminalObject( sFinSets );
<An object in
 FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )>
gap> IsTerminal( t );
true
gap> IsInitial( t );
false
gap> Display( t );
[ 1, [ TerminalObject( ) ] ]

An object in
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
given by the above data
gap> i := InitialObject( sFinSets );
<An object in
 FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )>
gap> IsTerminal( i );
false
gap> IsInitial( i );
true
gap> Display( i );
[ 0, [  ] ]

An object in
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
given by the above data
gap> UniversalMorphismFromInitialObject(t) = UniversalMorphismIntoTerminalObject(i);
true
gap> A := [ 3, [ "A0" / T, "A1" / T, "A2" / T ] ] / sFinSets;
<An object in
 FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )>
gap> Display( A );
[ 3, [ A0, A1, A2 ] ]

An object in
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
given by the above data
gap> B := [ 2, [ "B0" / T, "B1" / T ] ] / sFinSets;
<An object in
 FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )>
gap> Display( B );
[ 2, [ B0, B1 ] ]

An object in
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
given by the above data
gap> piA := ProjectionInFactorOfDirectProduct( [ A, B ], 1 );
<A morphism in
 FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )>
gap> Display( piA );
{ 0,..., 5 } ⱶ[ 0, 1, 2, 0, 1, 2 ]→ { 0, 1, 2 }

[ ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A0, B0 ], 1,
  DirectProduct( [ A0, B0 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A1, B0 ], 1,
  DirectProduct( [ A1, B0 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A2, B0 ], 1,
  DirectProduct( [ A2, B0 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A0, B1 ], 1,
  DirectProduct( [ A0, B1 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A1, B1 ], 1,
  DirectProduct( [ A1, B1 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A2, B1 ], 1,
  DirectProduct( [ A2, B1 ] ) ) ]

A morphism in
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
given by the above data
gap> piB := ProjectionInFactorOfDirectProduct( [ A, B ], 2 );
<A morphism in
 FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )>
gap> Display( piB );
{ 0,..., 5 } ⱶ[ 0, 0, 0, 1, 1, 1 ]→ { 0, 1 }

[ ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A0, B0 ], 2,
  DirectProduct( [ A0, B0 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A1, B0 ], 2,
  DirectProduct( [ A1, B0 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A2, B0 ], 2,
  DirectProduct( [ A2, B0 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A0, B1 ], 2,
  DirectProduct( [ A0, B1 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A1, B1 ], 2,
  DirectProduct( [ A1, B1 ] ) ),
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( [ A2, B1 ], 2,
  DirectProduct( [ A2, B1 ] ) ) ]

A morphism in
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
given by the above data
gap> IsOne( UniversalMorphismIntoDirectProduct( [ piA, piB ] ) );
true
gap> I := HomStructure( sFinSets );
<An object in
 FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>
gap> Display( I );
[ 1, [ An object in TerminalCategoryWithSingleObject( ) ] ]

An object in
FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )
given by the above data
gap> U := ObjectDatum( I )[2][1];
<A zero object in TerminalCategoryWithSingleObject( )>
gap> HomAB := HomStructure( A, B );
<An object in
 FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>
gap> L := ObjectDatum( HomAB );
[ 8, [ <A zero object in TerminalCategoryWithSingleObject( )>,
       <A zero object in TerminalCategoryWithSingleObject( )>,
       <A zero object in TerminalCategoryWithSingleObject( )>,
       <A zero object in TerminalCategoryWithSingleObject( )>,
       <A zero object in TerminalCategoryWithSingleObject( )>,
       <A zero object in TerminalCategoryWithSingleObject( )>,
       <A zero object in TerminalCategoryWithSingleObject( )>,
       <A zero object in TerminalCategoryWithSingleObject( )> ] ]
gap> homAB := List( MorphismsOfExternalHom( A, B ), HomStructure );
[ <A morphism in
   FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>,
  <A morphism in
   FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>,
  <A morphism in
   FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>,
  <A morphism in
   FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>,
  <A morphism in
   FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>,
  <A morphism in
   FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>,
  <A morphism in
   FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>,
  <A morphism in
   FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )> ]
gap> List( homAB, IsWellDefined );
[ true, true, true, true, true, true, true, true ]
gap> List( homAB, m -> HomStructure( HomStructure( A, B, m ) ) ) = homAB;
true
gap> alpha := HomStructure( A, B, homAB[6] );
<A morphism in
 FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )>
gap> Display( alpha );
{ 0, 1, 2 } ⱶ[ 1, 0, 1 ]→ { 0, 1 }

[ InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism,
  InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism,
  InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism ]

A morphism in
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
given by the above data
gap> gamma := HomStructure( A, B, homAB[2] );
<A morphism in
 FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )>
gap> Display( gamma );
{ 0, 1, 2 } ⱶ[ 1, 0, 0 ]→ { 0, 1 }

[ InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism,
  InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism,
  InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism ]

A morphism in
FiniteStrictCoproductCompletion( TerminalCategoryWithMultipleObjects( ) )
given by the above data
gap> hom_alpha_gamma := HomStructure( alpha, gamma );
<A morphism in
 FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )>
gap> Display( hom_alpha_gamma );
{ 0,..., 8 } ⱶ[ 7, 5, 5, 2, 0, 0, 2, 0, 0 ]→ { 0,..., 7 }

[ A morphism in TerminalCategoryWithSingleObject( ),
  A morphism in TerminalCategoryWithSingleObject( ),
  A morphism in TerminalCategoryWithSingleObject( ),
  A morphism in TerminalCategoryWithSingleObject( ),
  A morphism in TerminalCategoryWithSingleObject( ),
  A morphism in TerminalCategoryWithSingleObject( ),
  A morphism in TerminalCategoryWithSingleObject( ),
  A morphism in TerminalCategoryWithSingleObject( ),
  A morphism in TerminalCategoryWithSingleObject( ) ]

A morphism in
FiniteStrictCoproductCompletion( TerminalCategoryWithSingleObject( ) )
given by the above data
gap> IsWellDefined( hom_alpha_gamma );
true

1.4-5 Reflexive pair
gap> LoadPackage( "FiniteCocompletions" );
true
gap> LoadPackage( "Algebroids" );
true
gap> LoadPackage( "LazyCategories", ">= 2023.01-02" );
true
gap> Q := RightQuiver( "Q(A,B)[f:A->B,g:A->B]" );
Q(A,B)[f:A->B,g:A->B]
gap> C := FreeCategory( Q );
FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) )
gap> SetName( C.A, "C.A" ); SetName( C.B, "C.B" );
gap> UC := FiniteStrictCoproductCompletion( C );
FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )
gap> A := UC.A;
<An object in FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>
gap> B := UC.B;
<An object in FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>
gap> Display( A );
[ 1, [ C.A ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )
given by the above data
gap> Display( B );
[ 1, [ C.B ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )
given by the above data
gap> f := UC.f;
<A morphism in FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>
gap> g := UC.g;
<A morphism in FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>
gap> MorphismDatum( f );
[ [ 0 ], [ (A)-[(f)]->(B) ] ]
gap> MorphismDatum( g );
[ [ 0 ], [ (A)-[(g)]->(B) ] ]
gap> IsSplitEpimorphism( f );
false
gap> IsSplitEpimorphism( g );
false
gap> AuB := Coproduct( A, B );
<An object in FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>
gap> Display( AuB );
[ 2, [ C.A, C.B ] ]

An object in FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )
given by the above data
gap> HomStructure( AuB, B );
|2|
gap> hom := MorphismsOfExternalHom( AuB, B );
[ <A morphism in FiniteStrictCoproductCompletion(
   FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>,
  <A morphism in FiniteStrictCoproductCompletion(
   FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )> ]
gap> ff := hom[1];
<A morphism in FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>
gap> gg := hom[2];
<A morphism in FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>
gap> ff = gg;
false
gap> IsSplitEpimorphism( ff );
true
gap> IsSplitEpimorphism( gg );
true
gap> MorphismDatum( ff );
[ [ 0, 0 ], [ (A)-[(f)]->(B), (B)-[(B)]->(B) ] ]
gap> MorphismDatum( gg );
[ [ 0, 0 ], [ (A)-[(g)]->(B), (B)-[(B)]->(B) ] ]
gap> HomStructure( B, AuB );
|1|
gap> ii := MorphismsOfExternalHom( B, AuB )[1];
<A morphism in FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )>
gap> ii = InjectionOfCofactorOfCoproduct( [ A, B ], 2 );
true
gap> f = ComponentOfMorphismFromCoproduct( ff, [ A, B ], 1 );
true
gap> IsOne( ComponentOfMorphismFromCoproduct( ff, [ A, B ], 2 ) );
true
gap> g = ComponentOfMorphismFromCoproduct( gg, [ A, B ], 1  );
true
gap> IsOne( ComponentOfMorphismFromCoproduct( gg, [ A, B ], 2 ) );
true
gap> LUC := LazyCategory( UC );
LazyCategory( FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) ) )
gap> Emb := EmbeddingFunctorOfUnderlyingCategory( LUC );
Embedding functor into lazy category
gap> Display( Emb );
Embedding functor into lazy category:

FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )
  |
  V
LazyCategory( FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) ) )
gap> F := PreCompose( EmbeddingOfUnderlyingCategory( UC ), Emb );
Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category
gap> Display( F );
Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category:

FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) )
  |
  V
LazyCategory( FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) ) )
gap> G := ExtendFunctorToFiniteStrictCoproductCompletion( F );
Extension to FiniteStrictCoproductCompletion( Source( Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category ) )
gap> Display( G );
Extension to FiniteStrictCoproductCompletion( Source( Precomposition of
Embedding functor into a finite strict coproduct cocompletion category and
Embedding functor into lazy category ) ):

FiniteStrictCoproductCompletion(
FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) )
  |
  V
LazyCategory( FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) ) )
gap> Gff := G( ff );
<A morphism in LazyCategory( FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) ) )>
gap> IsWellDefined( Gff );
true
gap> Ggg := G( gg );
<A morphism in LazyCategory( FiniteStrictCoproductCompletion(
 FreeCategory( RightQuiver( "Q(A,B)[f:A->B,g:A->B]" ) ) ) )>
gap> IsWellDefined( Ggg );
true
gap> MorphismDatum( EvaluatedCell( Gff ) );
[ [ 0, 0 ], [ (A)-[(f)]->(B), (B)-[(B)]->(B) ] ]
gap> MorphismDatum( EvaluatedCell( Ggg ) );
[ [ 0, 0 ], [ (A)-[(g)]->(B), (B)-[(B)]->(B) ] ]
 [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