GAP (FinSetsForCAP) - Chapter 2: The category of skeletal finite sets

The integer defining the skeletal finite set M, i.e., Length( FinSet( n ) ) = n.

2.2-2 AsList

The list associated to a skeletal finite set, i.e., AsList( FinSet( n ) ) = [ 0 .. n - 1 ].

2.2-3 AsList

The graph defining the skeletal finite set morphism phi, see MapOfFinSets (2.3-5).

2.3 Constructors

2.3-1 SkeletalCategoryOfFiniteSets

2.3-2 SkeletalFinSets

The default instance of the category of skeletal finite sets. It is automatically created while loading this package.

2.3-3 FinSet

Construct a skeletal finite set residing in the default instance of the category of skeletal finite sets SkeletalFinSets of order given by the nonnegative integer n.

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 7 );
|7|
gap> Display( m );
{ 0,..., 6 }
gap> IsWellDefined( m );
true
gap> String( m );
"FinSet( SkeletalFinSets, 7 )"
gap> Display( List( m, x -> x^2 ) );
[ 0, 1, 4, 9, 16, 25, 36 ]
gap> L := ObjectDatum( m );
7
gap> mm := ObjectConstructor( SkeletalFinSets, BigInt( 7 ) );
|7|
gap> m = mm;
true
gap> n := FinSet( -2 );
|-2|
gap> IsWellDefined( n );
false
gap> n := FinSet( 3 );
|3|
gap> IsWellDefined( n );
true
gap> p := FinSet( 4 );
|4|
gap> IsWellDefined( p );
true
gap> IsEqualForObjects( m, n );
false

2.3-4 FinSet

Construct a skeletal finite set residing in the given category of skeletal finite sets C of order given by the nonnegative integer n.

2.3-5 MapOfFinSets

Construct a map \phi:s\tot of the skeletal finite sets s and t, i.e., a morphism in the CAP category of s, where G is a list of integers in t describing the graph of \phi.

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> s := FinSet( 3 );
|3|
gap> t := FinSet( 7 );
|7|
gap> phi := MapOfFinSets( s, [ 6, 4, 4 ], t );
|3| → |7|
gap> Display( AsList( phi ) );
[ 6, 4, 4 ]
gap> IsWellDefined( phi );
true
gap> Display( phi );
{ 0, 1, 2 } ⱶ[ 6, 4, 4 ]→ { 0,..., 6 }
gap> String( phi );
"MapOfFinSets( SkeletalFinSets, FinSet( SkeletalFinSets, 3 ), [ 6, 4, 4 ], Fin\
Set( SkeletalFinSets, 7 ) )"
gap> s := ObjectConstructor( SkeletalFinSets, BigInt( 3 ) );
|3|
gap> t := ObjectConstructor( SkeletalFinSets, BigInt( 7 ) );
|7|
gap> phi := MorphismConstructor(
>     s,
>     [ BigInt( 6 ), BigInt( 4 ), BigInt( 4 ) ],
>     t
> );
|3| → |7|
gap> Display( MorphismDatum( phi ) );
[ 6, 4, 4 ]
gap> IsWellDefined( phi );
true
gap> Display( phi );
{ 0, 1, 2 } ⱶ[ 6, 4, 4 ]→ { 0,..., 6 }

2.4 Tools

2.4-1 ListOp

2.4-2 EmbeddingOfFinSets

Construct the embedding \iota:s\tot of the finite sets s and t, where s must be subset of t.

2.4-3 Preimage

2.4-4 ImageObject

2.4-5 CallFuncList

Returns the image of L[1] under the map phi assuming L[1] is a nonnegative integer smaller than Length( Source( phi ) ).

2.4-6 GeometricSum

Returns (q^n-1)/(q-1) = Sum( [ 0 .. n - 1 ], i -> q^i ), taking the corner case q= 1 into account.

2.4-7 GeometricSumDiff1

Returns (1+((n-1)*q-n)*q^(n-1))/(q-1)^2 = Sum( [ 0 .. n - 1 ], i -> i * q^(i - 1) ), taking the corner case q= 1 into account.

2.4-8 RemIntWithDomain

Return the remainder of the natural number v less than ab modulo a, where ab is a multiple of a.

2.4-9 QuoIntWithDomain

Return the quotient of the natural number v less than ab modulo a, where ab is a multiple of a.

2.4-10 DivIntWithGivenQuotient

2.4-11 DigitInPositionalNotation

Return the digit of index i in the b-adic expansion of length l of the natural number v.

2.5 Examples

2.5-1 SkeletalIsHomSetInhabited

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> L := FinSet( 0 );
|0|
gap> M := FinSet( 2 );
|2|
gap> N := FinSet( 3 );
|3|
gap> IsHomSetInhabited( L, L );
true
gap> IsHomSetInhabited( M, L );
false
gap> IsHomSetInhabited( L, M );
true
gap> IsHomSetInhabited( M, N );
true

2.5-2 Skeletal WellDefined

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> s := FinSet( 7 );
|7|
gap> t := FinSet( 4 );
|4|
gap> psi := MapOfFinSets( s, [ 0, 2, 1, 2, 1, 3 ], t );
|7| → |4|
gap> IsWellDefined( psi );
false
gap> psi := MapOfFinSets( s, [ 0, 2, 1, 2, 1, 3, -2 ], t );
|7| → |4|
gap> IsWellDefined( psi );
false
gap> psi := MapOfFinSets( s, [ 1, 2, 1, 4, 2, 1, 3 ], t );
|7| → |4|
gap> IsWellDefined( psi );
false
gap> psi := MapOfFinSets( s, [ 0, 2, 1, 3, 2, 1, 3 ], t );
|7| → |4|
gap> IsWellDefined( psi );
true

2.5-3 Skeletal PreCompose

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 3 );
|3|
gap> n := FinSet( 5 );
|5|
gap> p := FinSet( 7 );
|7|
gap> psi := MapOfFinSets( m, [ 1, 4, 2 ], n );
|3| → |5|
gap> phi := MapOfFinSets( n, [ 0, 3, 5, 5, 2 ], p );
|5| → |7|
gap> alpha := PreCompose( psi, phi );
|3| → |7|
gap> Display( alpha );
{ 0, 1, 2 } ⱶ[ 3, 2, 5 ]→ { 0,..., 6 }

2.5-4 Skeletal Monomophisms and Epimophisms

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 3 );
|3|
gap> n := FinSet( 5 );
|5|
gap> p := FinSet( 7 );
|7|
gap> psi := MapOfFinSets( m, [ 0, 2, 4 ], n );
|3| → |5|
gap> IsEpimorphism( psi );
false
gap> IsSplitEpimorphism( psi );
false
gap> IsMonomorphism( psi );
true
gap> IsSplitMonomorphism( psi );
true
gap> psi;
|3| ↪ |5|
gap> psi := MapOfFinSets( p, [ 0, 2, 1, 2, 2, 1, 0 ], m );
|7| → |3|
gap> IsEpimorphism( psi );
true
gap> IsSplitEpimorphism( psi );
true
gap> IsMonomorphism( psi );
false
gap> IsSplitMonomorphism( psi );
false
gap> psi;
|7| ↠ |3|
gap> id := IdentityMorphism( m );
|3| → |3|
gap> IsIsomorphism( id );
true
gap> id;
|3| ⭇ |3|

2.5-5 Skeletal Initial and Terminal Objects

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 8 );
|8|
gap> IsInitial( m );
false
gap> IsTerminal( m );
false
gap> i := InitialObject( SkeletalFinSets );
|0|
gap> Display( i );
∅
gap> IsInitial( i );
true
gap> IsTerminal( i );
false
gap> iota := UniversalMorphismFromInitialObject( m );
|0| → |8|
gap> Display( AsList( i ) );
[  ]
gap> t := TerminalObject( SkeletalFinSets );
|1|
gap> Display( AsList( t ) );
[ 0 ]
gap> IsInitial( t );
false
gap> IsTerminal( t );
true
gap> pi := UniversalMorphismIntoTerminalObject( m );
|8| → |1|
gap> IsIdenticalObj( Range( pi ), t );
true
gap> pi_t := UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( m, t );
|8| → |1|
gap> Display( AsList( pi_t ) );
[ 0, 0, 0, 0, 0, 0, 0, 0 ]
gap> pi = pi_t;
true

2.5-6 Projective and Injective Objects

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> I := FinSet( 0 );
|0|
gap> T := FinSet( 1 );
|1|
gap> M := FinSet( 2 );
|2|
gap> IsProjective( I );
true
gap> IsProjective( T );
true
gap> IsProjective( M );
true
gap> IsOne( EpimorphismFromSomeProjectiveObject( I ) );
true
gap> IsOne( EpimorphismFromSomeProjectiveObject( M ) );
true

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> I := FinSet( 0 );
|0|
gap> T := FinSet( 1 );
|1|
gap> M := FinSet( 2 );
|2|
gap> IsInjective( I );
false
gap> IsInjective( T );
true
gap> IsInjective( M );
true
gap> IsIsomorphism( MonomorphismIntoSomeInjectiveObject( I ) );
false
gap> IsMonomorphism( MonomorphismIntoSomeInjectiveObject( I ) );
true
gap> IsOne( MonomorphismIntoSomeInjectiveObject( M ) );
true

2.5-7 Skeletal Product

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 7 );
|7|
gap> n := FinSet( 3 );
|3|
gap> p := FinSet( 4 );
|4|
gap> d := DirectProduct( [ m, n, p ] );
|84|
gap> Display( AsList( d ) );
[ 0 .. 83 ]
gap> pi1 := ProjectionInFactorOfDirectProduct( [ m, n, p ], 1 );
|84| → |7|
gap> Display( pi1 );
{ 0,..., 83 } ⱶ[ 0, 1, 2, 3, 4, 5, 6, 0, 1, 2, 3, 4, 5, 6,\
 0, 1, 2, 3, 4, 5, 6, 0, 1, 2, 3, 4, 5, 6,\
 0, 1, 2, 3, 4, 5, 6, 0, 1, 2, 3, 4, 5, 6,\
 0, 1, 2, 3, 4, 5, 6, 0, 1, 2, 3, 4, 5, 6,\
 0, 1, 2, 3, 4, 5, 6, 0, 1, 2, 3, 4, 5, 6,\
 0, 1, 2, 3, 4, 5, 6, 0, 1, 2, 3, 4, 5, 6 ]→ { 0,..., 6 }
gap> pi2 := ProjectionInFactorOfDirectProduct( [ m, n, p ], 2 );
|84| → |3|
gap> Display( pi2 );
{ 0,..., 83 } ⱶ[ 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1,\
 2, 2, 2, 2, 2, 2, 2, 0, 0, 0, 0, 0, 0, 0,\
 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2,\
 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1,\
 2, 2, 2, 2, 2, 2, 2, 0, 0, 0, 0, 0, 0, 0,\
 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2 ]→ { 0, 1, 2 }
gap> pi3 := ProjectionInFactorOfDirectProduct( [ m, n, p ], 3 );
|84| → |4|
gap> Display( pi3 );
{ 0,..., 83 } ⱶ[ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,\
 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1,\
 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,\
 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,\
 2, 2, 2, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3,\
 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3 ]→ { 0,..., 3 }
gap> psi := UniversalMorphismIntoDirectProduct( [ m, n, p ], [ pi1, pi2, pi3 ] );
|84| → |84|
gap> psi = IdentityMorphism( d );
true

2.5-8 Skeletal Coproduct

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 7 );
|7|
gap> n := FinSet( 3 );
|3|
gap> p := FinSet( 4 );
|4|
gap> c := Coproduct( m, n, p );
|14|
gap> Display( AsList( c ) );
[ 0 .. 13 ]
gap> iota1 := InjectionOfCofactorOfCoproduct( [ m, n, p ], 1 );
|7| → |14|
gap> IsWellDefined( iota1 );
true
gap> Display( iota1 );
{ 0,..., 6 } ⱶ[ 0 .. 6 ]→ { 0,..., 13 }
gap> iota2 := InjectionOfCofactorOfCoproduct( [ m, n, p ], 2 );
|3| → |14|
gap> IsWellDefined( iota2 );
true
gap> Display( iota2 );
{ 0, 1, 2 } ⱶ[ 7 .. 9 ]→ { 0,..., 13 }
gap> iota3 := InjectionOfCofactorOfCoproduct( [ m, n, p ], 3 );
|4| → |14|
gap> IsWellDefined( iota3 );
true
gap> Display( iota3 );
{ 0,..., 3 } ⱶ[ 10 .. 13 ]→ { 0,..., 13 }
gap> psi := UniversalMorphismFromCoproduct(
>                [ m, n, p ], [ iota1, iota2, iota3 ] );
|14| → |14|
gap> id := IdentityMorphism( Coproduct( [ m, n, p ] ) );
|14| → |14|
gap> psi = id;
true

2.5-9 Skeletal Image

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 7 );
|7|
gap> n := FinSet( 3 );
|3|
gap> phi := MapOfFinSets( n, [ 6, 4, 4 ], m );
|3| → |7|
gap> IsWellDefined( phi );
true
gap> ImageObject( phi );
|2|
gap> Length( ImageObject( phi ) );
2
gap> s := FinSet( 2 );
|2|
gap> I := ImageObject( phi, s );
|2|
gap> Length( I );
2

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 7 );
|7|
gap> n := FinSet( 3 );
|3|
gap> phi := MapOfFinSets( n, [ 6, 4, 4 ], m );
|3| → |7|
gap> pi := ImageEmbedding( phi );
|2| → |7|
gap> Display( pi );
{ 0, 1 } ⱶ[ 4, 6 ]→ { 0,..., 6 }

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 7 );
|7|
gap> n := FinSet( 3 );
|3|
gap> phi := MapOfFinSets( n, [ 6, 4, 4 ], m );
|3| → |7|
gap> IsWellDefined( phi );
true
gap> f := CoastrictionToImage( phi );
|3| → |2|
gap> Display( f );
{ 0, 1, 2 } ⱶ[ 1, 0, 0 ]→ { 0, 1 }
gap> IsWellDefined( f );
true
gap> IsEpimorphism( f );
true
gap> IsSplitEpimorphism( f );
true
gap> m := FinSet( 77 );
|77|
gap> n := FinSet( 4 );
|4|
gap> phi := MapOfFinSets( n, [ 76, 1, 24, 1 ], m );
|4| → |77|
gap> IsWellDefined( phi );
true
gap> iota := ImageEmbedding( phi );
|3| → |77|
gap> pi := CoastrictionToImage( phi );
|4| → |3|
gap> Display( pi );
{ 0,..., 3 } ⱶ[ 2, 0, 1, 0 ]→ { 0, 1, 2 }
gap> IsWellDefined( pi );
true
gap> IsEpimorphism( pi );
true
gap> IsSplitEpimorphism( pi );
true
gap> PreCompose( pi, iota ) = phi;
true

2.5-10 Skeletal Coimage

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 3 );
|3|
gap> n := FinSet( 3 );
|3|
gap> phi := MapOfFinSets( m, [ 1, 0, 1 ], n );
|3| → |3|
gap> I := CoimageObject( phi );
|2|
gap> IsMonomorphism( phi );
false
gap> IsSplitMonomorphism( phi );
false
gap> IsEpimorphism( phi );
false
gap> IsSplitEpimorphism( phi );
false
gap> pi := CoimageProjection( phi );
|3| → |2|
gap> iota := AstrictionToCoimage( phi );
|2| → |3|
gap> PreCompose( pi, iota ) = phi;
true
gap> Display( iota );
{ 0, 1 } ⱶ[ 1, 0 ]→ { 0, 1, 2 }
gap> Display( ImageEmbedding( phi ) );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 }

2.5-11 Skeletal Preimage

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 7 );
|7|
gap> n := FinSet( 3 );
|3|
gap> phi := MapOfFinSets( n, [ 6, 4, 4 ], m );
|3| → |7|
gap> P := Preimage( phi, [ 2 ] );;
gap> Display( P );
[  ]
gap> P := Preimage( phi, AsList( FinSet( 5 ) ) );;
gap> Display( P );
[ 1, 2 ]

2.5-12 Skeletal Equalizer

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> S := FinSet( 5 );
|5|
gap> T := FinSet( 3 );
|3|
gap> f1 := MapOfFinSets( S, [ 2, 2, 0, 1, 1 ], T );
|5| → |3|
gap> f2 := MapOfFinSets( S, [ 2, 1, 2, 0, 1 ], T );
|5| → |3|
gap> f3 := MapOfFinSets( S, [ 2, 0, 1, 0, 1 ], T );
|5| → |3|
gap> D := [ f1, f2, f3 ];;
gap> Eq := Equalizer( D );
|2|
gap> iota := EmbeddingOfEqualizer( D );
|2| → |5|
gap> Display( iota );
{ 0, 1 } ⱶ[ 0, 4 ]→ { 0,..., 4 }
gap> phi := MapOfFinSets( FinSet( 2 ), [ 4, 0 ], S );;
gap> IsWellDefined( phi );
true
gap> psi := UniversalMorphismIntoEqualizer( D, phi );
|2| → |2|
gap> IsWellDefined( psi );
true
gap> Display( psi );
{ 0, 1 } ⱶ[ 1, 0 ]→ { 0, 1 }
gap> PreCompose( psi, iota ) = phi;
true
gap> D := [ f2, f3 ];;
gap> Eq := Equalizer( D );
|3|
gap> psi := EmbeddingOfEqualizer( D );
|3| → |5|
gap> Display( psi );
{ 0, 1, 2 } ⱶ[ 0, 3, 4 ]→ { 0,..., 4 }

2.5-13 Skeletal Pullback

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 5 );
|5|
gap> n1 := FinSet( 3 );
|3|
gap> iota1 := EmbeddingOfFinSets( n1, m );
|3| ↪ |5|
gap> Display( iota1 );
{ 0, 1, 2 } ⱶ[ 0 .. 2 ]→ { 0,..., 4 }
gap> n2 := FinSet( 4 );
|4|
gap> iota2 := EmbeddingOfFinSets( n2, m );
|4| ↪ |5|
gap> Display( iota2 );
{ 0,..., 3 } ⱶ[ 0 .. 3 ]→ { 0,..., 4 }
gap> D := [ iota1, iota2 ];;
gap> Fib := FiberProduct( D );
|3|
gap> pi1 := ProjectionInFactorOfFiberProduct( D, 1 );
|3| → |3|
gap> Display( pi1 );
{ 0, 1, 2 } ⱶ[ 0, 1, 2 ]→ { 0, 1, 2 }
gap> int1 := ImageObject( pi1 );
|3|
gap> pi2 := ProjectionInFactorOfFiberProduct( D, 2 );
|3| → |4|
gap> Display( pi2 );
{ 0, 1, 2 } ⱶ[ 0, 1, 2 ]→ { 0,..., 3 }
gap> int2 := ImageObject( pi2 );
|3|
gap> omega1 := PreCompose( pi1, iota1 );
|3| → |5|
gap> omega2 := PreCompose( pi2, iota2 );
|3| → |5|
gap> omega1 = omega2;
true
gap> Display( omega1 );
{ 0, 1, 2 } ⱶ[ 0, 1, 2 ]→ { 0,..., 4 }

2.5-14 Skeletal Coequalizer

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> s := FinSet( 5 );
|5|
gap> t := FinSet( 4 );
|4|
gap> f := MapOfFinSets( s, [ 2, 3, 3, 1, 3 ], t );
|5| → |4|
gap> g := MapOfFinSets( s, [ 2, 2, 3, 1, 3 ], t );
|5| → |4|
gap> D := [ f, g ];;
gap> C := Coequalizer( D );
|3|
gap> pi := ProjectionOntoCoequalizer( D );
|4| → |3|
gap> Display( pi );
{ 0,..., 3 } ⱶ[ 0, 1, 2, 2 ]→ { 0, 1, 2 }
gap> tau := MapOfFinSets( t, [ 1, 0, 1, 1 ], FinSet( 2 ) );
|4| → |2|
gap> phi := UniversalMorphismFromCoequalizer( D, tau );
|3| → |2|
gap> Display( phi );
{ 0, 1, 2 } ⱶ[ 1, 0, 1 ]→ { 0, 1 }
gap> PreCompose( pi, phi ) = tau;
true
gap> s := FinSet( 5 );
|5|
gap> t := FinSet( 4 );
|4|
gap> f := MapOfFinSets( s, [ 1, 2, 2, 1, 3 ], t );
|5| → |4|
gap> g := MapOfFinSets( s, [ 1, 2, 1, 1, 3 ], t );
|5| → |4|
gap> D := [ f, g ];;
gap> C := Coequalizer( D );
|3|
gap> pi := ProjectionOntoCoequalizer( D );
|4| → |3|
gap> Display( pi );
{ 0,..., 3 } ⱶ[ 0, 1, 1, 2 ]→ { 0, 1, 2 }
gap> PreCompose( f, pi ) = PreCompose( g, pi );
true
gap> tau := MapOfFinSets( t, [ 0, 1, 1, 0 ], FinSet( 2 ) );
|4| → |2|
gap> phi := UniversalMorphismFromCoequalizer( D, tau );
|3| → |2|
gap> Display( phi );
{ 0, 1, 2 } ⱶ[ 0, 1, 0 ]→ { 0, 1 }
gap> PreCompose( pi, phi ) = tau;
true
gap> s := FinSet( 2 );;
gap> t := FinSet( 3 );;
gap> f := MapOfFinSets( s, [ 0, 1 ], t );;
gap> IsWellDefined( f );
true
gap> g := MapOfFinSets( s, [ 1, 2 ], t );;
gap> IsWellDefined( g );
true
gap> C := Coequalizer( [ f, g ] );
|1|

2.5-15 Skeletal Pushout

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> M := FinSet( 5 );
|5|
gap> N1 := FinSet( 3 );
|3|
gap> iota1 := EmbeddingOfFinSets( N1, M );
|3| ↪ |5|
gap> Display( iota1 );
{ 0, 1, 2 } ⱶ[ 0 .. 2 ]→ { 0,..., 4 }
gap> N2 := FinSet( 2 );
|2|
gap> iota2 := EmbeddingOfFinSets( N2, M );
|2| ↪ |5|
gap> Display( iota2 );
{ 0, 1 } ⱶ[ 0 .. 1 ]→ { 0,..., 4 }
gap> D := [ iota1, iota2 ];;
gap> Fib := FiberProduct( D );
|2|
gap> pi1 := ProjectionInFactorOfFiberProduct( D, 1 );
|2| → |3|
gap> Display( pi1 );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 }
gap> pi2 := ProjectionInFactorOfFiberProduct( D, 2 );
|2| → |2|
gap> Display( pi2 );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 }

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> D := [ pi1, pi2 ];;
gap> UU := Pushout( D );
|3|
gap> kappa1 := InjectionOfCofactorOfPushout( D, 1 );
|3| → |3|
gap> Display( kappa1 );
{ 0, 1, 2 } ⱶ[ 0, 1, 2 ]→ { 0, 1, 2 }
gap> kappa2 := InjectionOfCofactorOfPushout( D, 2 );
|2| → |3|
gap> Display( kappa2 );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 }
gap> PreCompose( pi1, kappa1 ) = PreCompose( pi2, kappa2 );
true

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> Co := Coproduct( N1, N2 );
|5|
gap> Display( Co );
{ 0,..., 4 }
gap> iota_1 := InjectionOfCofactorOfCoproduct( [ N1, N2 ], 1 );
|3| → |5|
gap> Display( iota_1 );
{ 0, 1, 2 } ⱶ[ 0 .. 2 ]→ { 0,..., 4 }
gap> iota_2 := InjectionOfCofactorOfCoproduct( [ N1, N2 ], 2 );
|2| → |5|
gap> Display( iota_2 );
{ 0, 1 } ⱶ[ 3 .. 4 ]→ { 0,..., 4 }
gap> alpha := PreCompose( pi1, iota_1 );
|2| → |5|
gap> Display( alpha );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0,..., 4 }
gap> beta := PreCompose( pi2, iota_2 );
|2| → |5|
gap> Display( beta );
{ 0, 1 } ⱶ[ 3, 4 ]→ { 0,..., 4 }
gap> Cq := Coequalizer( [ alpha, beta ] );
|3|
gap> psi := ProjectionOntoCoequalizer( [ alpha, beta ] );
|5| → |3|
gap> Display( psi );
{ 0,..., 4 } ⱶ[ 0, 1, 2, 0, 1 ]→ { 0, 1, 2 }
gap> Display( PreCompose( iota_1, psi ) );
{ 0, 1, 2 } ⱶ[ 0, 1, 2 ]→ { 0, 1, 2 }
gap> Display( PreCompose( iota_2, psi ) );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 }
gap> PreCompose( alpha, psi ) = PreCompose( beta, psi );
true

2.5-16 Skeletal Cartesian Lambda Introduction

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> S := FinSet( 3 );
|3|
gap> R := FinSet( 2 );
|2|
gap> f := MapOfFinSets( S, [ 1, 1, 0 ], R );
|3| → |2|
gap> IsWellDefined( f );
true
gap> T := TerminalObject( SkeletalFinSets );
|1|
gap> IsTerminal( T );
true
gap> IsOne( CartesianLambdaIntroduction( IdentityMorphism( T ) ) );
true
gap> lf := CartesianLambdaIntroduction( f );
|1| → |8|
gap> Source( lf ) = T;
true
gap> Display( Range( lf ) );
{ 0,..., 7 }
gap> Display( lf );
{ 0 } ⱶ[ 3 ]→ { 0,..., 7 }
#@if ValueOption( "no_precompiled_code" ) <> true
gap> SkeletalFinSets!.cached_precompiled_functions.
>     CartesianLambdaIntroduction( SkeletalFinSets, f );
|1| → |8|
#@fi
gap> elf := CartesianLambdaElimination( S, R, lf );
|3| → |2|
gap> elf = f;
true
gap> L := MorphismsOfExternalHom( S, R );;
gap> Display( L );
[ { 0, 1, 2 } ⱶ[ 0, 0, 0 ]→ { 0, 1 },\
 { 0, 1, 2 } ⱶ[ 1, 0, 0 ]→ { 0, 1 },\
 { 0, 1, 2 } ⱶ[ 0, 1, 0 ]→ { 0, 1 },\
 { 0, 1, 2 } ⱶ[ 1, 1, 0 ]→ { 0, 1 },\
 { 0, 1, 2 } ⱶ[ 0, 0, 1 ]→ { 0, 1 },\
 { 0, 1, 2 } ⱶ[ 1, 0, 1 ]→ { 0, 1 },\
 { 0, 1, 2 } ⱶ[ 0, 1, 1 ]→ { 0, 1 },\
 { 0, 1, 2 } ⱶ[ 1, 1, 1 ]→ { 0, 1 } ]
gap> Li := List( L, phi -> CartesianLambdaIntroduction( phi ) );;
gap> Display( Li );
[ { 0 } ⱶ[ 0 ]→ { 0,..., 7 }, { 0 } ⱶ[ 1 ]→ { 0,..., 7 },\
 { 0 } ⱶ[ 2 ]→ { 0,..., 7 }, { 0 } ⱶ[ 3 ]→ { 0,..., 7 },\
 { 0 } ⱶ[ 4 ]→ { 0,..., 7 }, { 0 } ⱶ[ 5 ]→ { 0,..., 7 },\
 { 0 } ⱶ[ 6 ]→ { 0,..., 7 }, { 0 } ⱶ[ 7 ]→ { 0,..., 7 } ]
gap> List( L, phi ->
>       DirectProductToExponentialLeftAdjunctMorphism( T, S, phi ) ) = Li;
true
gap> List( Li, psi -> CartesianLambdaElimination( S, R, psi ) ) = L;
true
gap> List( Li, psi ->
>       ExponentialToDirectProductLeftAdjunctMorphism( S, R, psi ) ) = L;
true

2.5-17 Skeletal Lift

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> m := FinSet( 3 );
|3|
gap> n := FinSet( 4 );
|4|
gap> f := MapOfFinSets( m, [ 1, 1, 0 ], m );
|3| → |3|
gap> g := MapOfFinSets( n, [ 2, 1, 0, 1 ], m );
|4| → |3|
gap> IsLiftable( f, g );
true
gap> chi := Lift( f, g );
|3| → |4|
gap> Display( chi );
{ 0, 1, 2 } ⱶ[ 1, 1, 2 ]→ { 0,..., 3 }
gap> PreCompose( Lift( f, g ), g ) = f;
true
gap> IsLiftable( g, f );
false
gap> k := FinSet( 100000 );
|100000|
gap> h := ListWithIdenticalEntries( Length( k ) - 3, 2 );;
gap> h := Concatenation( h, [ 1, 0, 1 ] );;
gap> h := MapOfFinSets( k, h, m );
|100000| → |3|
gap> IsLiftable( f, h );
true
gap> IsLiftable( h, f );
false

2.5-18 Skeletal Colift

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> I := InitialObject( SkeletalFinSets );
|0|
gap> iota := UniversalMorphismIntoTerminalObject( I );
|0| → |1|
gap> id := IdentityMorphism( I );
|0| → |0|
gap> IsColiftable( iota, id );
false
gap> m := FinSet( 5 );
|5|
gap> n := FinSet( 4 );
|4|
gap> f := MapOfFinSets( m, [ 1, 1, 0, 0, 2 ], n );
|5| → |4|
gap> g := MapOfFinSets( m, [ 4, 4, 3, 3, 4 ], m );
|5| → |5|
gap> IsColiftable( f, g );
true
gap> chi := Colift( f, g );
|4| → |5|
gap> Display( chi );
{ 0,..., 3 } ⱶ[ 3, 4, 4, 0 ]→ { 0,..., 4 }
gap> PreCompose( f, Colift( f, g ) ) = g;
true
gap> IsColiftable( g, f );
false

2.5-19 Skeletal singleton morphism

gap> LoadPackage( "FinSetsForCAP" );
true
gap> a := FinSet( 3 );
|3|
gap> sa := SingletonMorphism( a );;
gap> Display( sa );
{ 0, 1, 2 } ⱶ[ 1, 2, 4 ]→ { 0,..., 7 }
gap> sa = LowerSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) );
true
gap> sa = UpperSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) );
true

2.5-20 Skeletal topos properties

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> T := TerminalObject( SkeletalFinSets );;
gap> M := FinSet( 4 );;
gap> N := FinSet( 3 );;
gap> P := FinSet( 4 );;
gap> G_f := [ 0, 1, 0, 2 ];;
gap> f := MapOfFinSets( M, G_f, N );;
gap> IsWellDefined( f );
true
gap> G_g := [ 2, 2, 1, 0 ];;
gap> g := MapOfFinSets( M, G_g, N );;
gap> IsWellDefined( g );
true
gap> DirectProduct( M, N );;
gap> DirectProductOnMorphisms( f, g );;
gap> CartesianAssociatorLeftToRight( M, N, P );;
gap> CartesianAssociatorRightToLeft( M, N, P );;
gap> TerminalObject( FinSets );;
gap> CartesianLeftUnitor( M );;
gap> CartesianLeftUnitorInverse( M );;
gap> CartesianRightUnitor( M );;
gap> CartesianRightUnitorInverse( M );;
gap> CartesianBraiding( M, N );;
gap> CartesianBraidingInverse( M, N );;
#@if ValueOption( "no_precompiled_code" ) <> true
gap> SkeletalFinSets!.cached_precompiled_functions.
>     CartesianBraidingWithGivenDirectProducts( SkeletalFinSets,
>         DirectProduct( M, N ),
>         M, N,
>         DirectProduct( N, M )
> );;
gap> SkeletalFinSets!.cached_precompiled_functions.
>     CartesianBraidingInverseWithGivenDirectProducts( SkeletalFinSets,
>         DirectProduct( N, M ),
>         M, N,
>         DirectProduct( M, N )
> );;
#@fi
gap> ExponentialOnObjects( M, N );;
gap> ExponentialOnMorphisms( f, g );;
#@if ValueOption( "no_precompiled_code" ) <> true
gap> SkeletalFinSets!.cached_precompiled_functions.
>     ExponentialOnMorphismsWithGivenExponentials( SkeletalFinSets,
>         ExponentialOnObjects( Range( f ), Source( g ) ),
>         f, g,
>         ExponentialOnObjects( Source( f ), Range( g ) )
> );;
#@fi
gap> CartesianRightEvaluationMorphism( M, N );;
gap> ExponentialToDirectProductRightAdjunctMorphism( M, N,
>     UniversalMorphismFromInitialObject( ExponentialOnObjects( M, N ) )
> );;
gap> CartesianLeftEvaluationMorphism( M, N );;
gap> CartesianLeftCoevaluationMorphism( N, M );;
gap> CartesianLeftCoevaluationMorphism( T, T );;
gap> DirectProductToExponentialLeftAdjunctMorphism( M, N,
>     UniversalMorphismIntoTerminalObject( DirectProduct( M, N ) )
> );;
gap> ExponentialToDirectProductLeftAdjunctMorphism( M, N,
>     UniversalMorphismFromInitialObject( ExponentialOnObjects( M, N ) )
> );;
gap> M := FinSet( 2 );;
gap> N := FinSet( 2 );;
gap> P := FinSet( 1 );;
gap> Q := FinSet( 2 );;
gap> CartesianPreComposeMorphism( M, N, P );;
gap> CartesianPostComposeMorphism( M, N, P );;
gap> DirectProductExponentialCompatibilityMorphism( [ M, N, P, Q ] );;

2.5-21 Skeletal Subobject Classifier

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> SubobjectClassifier( SkeletalFinSets );
|2|
gap> Display( TruthMorphismOfFalse( SkeletalFinSets ) );
{ 0 } ⱶ[ 0 ]→ { 0, 1 }
gap> Display( TruthMorphismOfTrue( SkeletalFinSets ) );
{ 0 } ⱶ[ 1 ]→ { 0, 1 }
gap> Display( TruthMorphismOfNot( SkeletalFinSets ) );
{ 0, 1 } ⱶ[ 1, 0 ]→ { 0, 1 }
gap> CartesianSquareOfSubobjectClassifier( SkeletalFinSets );
|4|
gap> Display( TruthMorphismOfAnd( SkeletalFinSets ) );
{ 0,..., 3 } ⱶ[ 0, 0, 0, 1 ]→ { 0, 1 }
gap> Display( TruthMorphismOfOr( SkeletalFinSets ) );
{ 0,..., 3 } ⱶ[ 0, 1, 1, 1 ]→ { 0, 1 }
gap> Display( TruthMorphismOfImplies( SkeletalFinSets ) );
{ 0,..., 3 } ⱶ[ 1, 0, 1, 1 ]→ { 0, 1 }
gap> S := FinSet( 5 );
|5|
gap> A := FinSet( 2 );
|2|
gap> m := MapOfFinSets( A, [ 0, 4 ], S );
|2| → |5|
gap> Display( ClassifyingMorphismOfSubobject( m ) );
{ 0,..., 4 } ⱶ[ 1, 0, 0, 0, 1 ]→ { 0, 1 }

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> M := FinSet( 7 );
|7|
gap> N := FinSet( 3 );
|3|
gap> iotaN := MapOfFinSets( N, [ 1, 2, 4 ], M );
|3| → |7|
gap> NC := PseudoComplementSubobject( iotaN );
|4|
gap> tauN := EmbeddingOfPseudoComplementSubobject( iotaN );
|4| ↪ |7|
gap> Display( tauN );
{ 0,..., 3 } ⱶ[ 0, 3, 5, 6 ]→ { 0,..., 6 }
gap> L := FinSet( 4 );
|4|
gap> iotaL := MapOfFinSets( L, [ 1, 3, 4, 6 ], M );
|4| → |7|
gap> NIL := IntersectionSubobject( iotaN, iotaL );
|2|
gap> iotaNiL := EmbeddingOfIntersectionSubobject( iotaN, iotaL );
|2| ↪ |7|
gap> Display( iotaNiL );
{ 0, 1 } ⱶ[ 1, 4 ]→ { 0,..., 6 }
gap> NUL := UnionSubobject( iotaN, iotaL );
|5|
gap> iotaNuL := EmbeddingOfUnionSubobject( iotaN, iotaL );
|5| → |7|
gap> Display( iotaNuL );
{ 0,..., 4 } ⱶ[ 1, 2, 3, 4, 6 ]→ { 0,..., 6 }
gap> NPL := RelativePseudoComplementSubobject( iotaN, iotaL );
|6|
gap> iotaNpL := EmbeddingOfRelativePseudoComplementSubobject( iotaN, iotaL );
|6| ↪ |7|
gap> Display( iotaNpL );
{ 0,..., 5 } ⱶ[ 0, 1, 3, 4, 5, 6 ]→ { 0,..., 6 }

2.5-22 Skeletal Pushout Complement

Define two composable monos K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G in SkeletalFinSets:

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> K := FinSet( 3 );
|3|
gap> L := FinSet( 6 );
|6|
gap> l := MapOfFinSets( K, [ 2 .. 4 ], L );; IsMonomorphism( l );; l;
|3| ↪ |6|
gap> Display( l );
{ 0, 1, 2 } ⱶ[ 2 .. 4 ]→ { 0,..., 5 }
gap> G := FinSet( 8 );
|8|
gap> Display( G );
{ 0,..., 7 }
gap> m := MapOfFinSets( L, [ 0, 1, 2, 3, 5, 6 ], G );
|6| → |8|
gap> Display( m );
{ 0,..., 5 } ⱶ[ 0, 1, 2, 3, 5, 6 ]→ { 0,..., 7 }

Now we compute the pushout complement D \stackrel{c}{\hookrightarrow} G of K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G:

2 The category of skeletal finite sets

2.1 GAP Categories

2.1-1 IsSkeletalCategoryOfFiniteSets

2.1-2 IsObjectInSkeletalCategoryOfFiniteSets

2.1-3 IsMorphismInSkeletalCategoryOfFiniteSets

2.2 Attributes

2.2-1 Length