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] 

2 Finite strict product completion
 2.1 Attributes

  2.1-1 PairOfIntAndList
  2.1-2 PairOfLists
  2.1-3 UnderlyingCategory
  2.1-4 EmbeddingOfUnderlyingCategory
  2.1-5 ExtendFunctorToFiniteStrictProductCompletion
 2.2 Constructors

  2.2-1 FiniteStrictProductCompletion
 2.3 GAP categories

  2.3-1 IsFiniteStrictProductCompletion
  2.3-2 IsCellInFiniteStrictProductCompletion
  2.3-3 IsObjectInFiniteStrictProductCompletion
  2.3-4 IsMorphismInFiniteStrictProductCompletion
 2.4 Examples

  2.4-1 Cartesian braiding
  2.4-2 Cartesian diagonal

2 Finite strict product completion

2.1 Attributes

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

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

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

Return the category C underlying the finite product completion category UC := FiniteStrictProductCompletion( C )).

2.1-4 EmbeddingOfUnderlyingCategory
‣ EmbeddingOfUnderlyingCategory( PC )( attribute )

Returns: a CAP functor

The full embedding functor from the category C underlying the finite product completion PC into PC.

2.1-5 ExtendFunctorToFiniteStrictProductCompletion
‣ ExtendFunctorToFiniteStrictProductCompletion( PC )( attribute )

Returns: a CAP functor

The full embedding functor from the category C underlying the finite product completion UC into UC.

2.2 Constructors

2.2-1 FiniteStrictProductCompletion
‣ FiniteStrictProductCompletion( cat )( attribute )

Return the finite product completion of the category cat in which the cartesian associators are given by identities.

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

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

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

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

An object in FiniteStrictProductCompletion( 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
 FiniteStrictProductCompletion( InitialCategory( ) )>
gap> fn_z := ZeroObjectFunctorial( T );
<A zero, isomorphism in FiniteStrictProductCompletion( InitialCategory( ) )>
gap> IsWellDefined( fn_z );
true
gap> IsEqualForMorphisms( id_z, fn_z );
true
gap> IsCongruentForMorphisms( id_z, fn_z );
true

2.3 GAP categories

2.3-1 IsFiniteStrictProductCompletion
‣ IsFiniteStrictProductCompletion( arg )( filter )

Returns: true or false

The GAP category of finite product completion categories.

2.3-2 IsCellInFiniteStrictProductCompletion
‣ IsCellInFiniteStrictProductCompletion( arg )( filter )

Returns: true or false

The GAP category of cells in a finite product completion category.

2.3-3 IsObjectInFiniteStrictProductCompletion
‣ IsObjectInFiniteStrictProductCompletion( arg )( filter )

Returns: true or false

The GAP category of objects in a finite product completion category.

2.3-4 IsMorphismInFiniteStrictProductCompletion
‣ IsMorphismInFiniteStrictProductCompletion( arg )( filter )

Returns: true or false

The GAP category of morphisms in a finite product completion category.

2.4 Examples

2.4-1 Cartesian 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> PC := FiniteStrictProductCompletion( C );
FiniteStrictProductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
gap> ModelingCategory( PC );
Opposite( FiniteStrictCoproductCompletion( Opposite(
FreeCategory( RightQuiver( "Q(a,b)[]" ) ) ) ) )
gap> a := PC.a;
<An object in
 FiniteStrictProductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )>
gap> b := PC.b;
<An object in
 FiniteStrictProductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )>
gap> ab := DirectProduct( a, b );
<An object in
FiniteStrictProductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )>
gap> Display( ab );
[ 2, [ C.a, C.b ] ]

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

An object in
FiniteStrictProductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
given by the above data
gap> HomStructure( ab, ba );
|1|
gap> hom := MorphismsOfExternalHom( ab, ba );
[ <A morphism in
   FiniteStrictProductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )> ]
gap> gamma := hom[1];
<A morphism in
 FiniteStrictProductCompletion( 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 }

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

A morphism in
FiniteStrictProductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) )
given by the above data
gap> gamma = CartesianBraiding( a, b );
true
gap> LPC := LazyCategory( PC );
LazyCategory(
FiniteStrictProductCompletion( FreeCategory( RightQuiver( "Q(a,b)[]" ) ) ) )
gap> Emb := EmbeddingFunctorOfUnderlyingCategory( LPC );
Embedding functor into lazy category
gap> Display( Emb );
Embedding functor into lazy category:

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

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

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

2.4-2 Cartesian diagonal
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> PC := FiniteStrictProductCompletion( C );
FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
gap> ModelingCategory( PC );
Opposite( FiniteStrictCoproductCompletion( Opposite(
PathCategory( FinQuiver( "Q(a)[]" ) ) ) ) )
gap> a := PC.a;
<An object in
 FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )>
gap> aa := DirectProduct( a, a );
<An object in
 FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )>
gap> Display( aa );
[ 2, [ C.a, C.a ] ]

An object in
FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
given by the above data
gap> a = aa;
false
gap> HomStructure( aa, a );
|2|
gap> hom_aa_a := MorphismsOfExternalHom( aa, a );
[ <A morphism in
   FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )>,
  <A morphism in
   FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )> ]
gap> hom_aa_a[1] = ProjectionInFactorOfDirectProduct( [ a, a ], 1 );
true
gap> hom_aa_a[2] = ProjectionInFactorOfDirectProduct( [ a, a ], 2 );
true
gap> HomStructure( a, aa );
|1|
gap> hom_a_aa := MorphismsOfExternalHom( a, aa );
[ <A morphism in
   FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )> ]
gap> delta := hom_a_aa[1];
<A morphism in
 FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )>
gap> Source( delta ) = a;
true
gap> Target( delta ) = aa;
true
gap> IsOne( ComponentOfMorphismIntoDirectProduct( delta, [ a, a ], 1 ) );
true
gap> IsOne( ComponentOfMorphismIntoDirectProduct( 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
FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
given by the above data
gap> id_a := IdentityMorphism( C.a );
id(a):C.a -≻ C.a
gap> delta = CartesianDiagonal( a, 2 );
true
gap> CellAsEvaluatableString( delta, [ "C", "PC" ] );
"MorphismConstructor( PC,
        ObjectConstructor( PC,
                Pair( 1, [ ObjectConstructor( C, 1 ) ] ) ),
        Pair( [ 0, 0 ],
              [ IdentityMorphism( C, ObjectConstructor( C, 1 ) ),
                IdentityMorphism( C, ObjectConstructor( C, 1 ) ) ] ),
        ObjectConstructor( PC,
                Pair( 2,
                      [ ObjectConstructor( C, 1 ),
                        ObjectConstructor( C, 1 ) ] ) ) )"
gap> LPC := LazyCategory( PC );
LazyCategory(
FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) ) )
gap> Emb := EmbeddingFunctorOfUnderlyingCategory( LPC );
Embedding functor into lazy category
gap> Display( Emb );
Embedding functor into lazy category:

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

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

FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) )
  |
  V
LazyCategory(
FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) ) )
gap> Gdelta := G( delta );
<A morphism in LazyCategory(
 FiniteStrictProductCompletion( PathCategory( FinQuiver( "Q(a)[]" ) ) ) )>
gap> IsWellDefined( Gdelta );
true
 [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