[MathJax on]

1 Toposes

An elementary topos is a finite complete, cartesian closed category with a subobject classifier. It follows that an elementary topos is also a finitely cocomplete Heyting category.

The doctrines of (co)cartesian (co)closed categories and their variations are implemented in the CAP-based package CartesianCategories.

1.1 Exact cover with global elements

1.1-1 ExactCoverWithGlobalElements

Returns: a list of morphisms in \mathrm{Hom}( t, a )

The argument is an object a of a category \mathbf{C} which is enriched over itself, i.e., \mathbf{C} = RangeCategoryOfHomomorphismStructure( \mathbf{C} ). The output is a list D of global elements of a (i.e., morphisms from the distinguished object t :=DistinguishedObjectOfHomomorphismStructure( \mathbf{C} ) to a), such that UniversalMorphismFromCoproduct(a, D) is an isomorphism.

1.1-2 IndexOfNonliftableMorphismFromDistinguishedObject

Returns: a morphism in \mathrm{Hom}( t, \mathrm{Target}( \iota ) )

The argument is a nonepimorphic monomorphism iota of a category \mathbf{C} which is enriched over itself, i.e., \mathbf{C} = RangeCategoryOfHomomorphismStructure( \mathbf{C} ). The output is a positive integer, namely the position of a morphism \tau in the list ExactCoverWithGlobalElements( Range( iota ) ) of morphisms from the distinguished object t :=DistinguishedObjectOfHomomorphismStructure( \mathbf{C} ) to Range( iota ), such that IsLiftableAlongMonomorphism( iota, \tau ) = false.

1.1-3 NonliftableMorphismFromDistinguishedObject

Returns: a morphism in \mathrm{Hom}( t, \mathrm{Target}( \iota ) )

The argument is a nonepimorphic monomorphism iota of a category \mathbf{C} which is enriched over itself, i.e., \mathbf{C} = RangeCategoryOfHomomorphismStructure( \mathbf{C} ). The output is a morphism \tau from the distinguished object t :=DistinguishedObjectOfHomomorphismStructure( \mathbf{C} ) to Range( iota ), such that IsLiftableAlongMonomorphism( iota, \tau ) = false.

1.2 Subobject classifier

1.2-1 IsElementaryTopos

Returns: true or false

The property of the category C being an elementary topos.

A subobject classifier consists of three parts:

• an object \Omega,

• a function \mathrm{true} providing a morphism \mathrm{true}: 1 \rightarrow \Omega,

• a function \chi mapping each monomorphism i : A \rightarrow S to a morphism \chi_i : S \to \Omega.

The triple (\Omega,\mathrm{true},\chi) is called a subobject classifier if for each monomorphism i : A \to S, the morphism \chi_i : S \to \Omega is the unique morphism such that \chi_i \circ i = \mathrm{true} \circ \ast determine a pullback diagram.

1.2-2 SubobjectClassifier

Returns: an object

The argument is a category C. The output is the subobject classifier object \Omega of C.

1.2-3 CartesianSquareOfSubobjectClassifier

Returns: an object

The argument is a category C. The output is the cartesian square of the subobject classifier object \Omega of C.

1.2-4 ClassifyingMorphismOfSubobject

Returns: a morphism in \mathrm{Hom}( \mathrm{Target}(m), \mathrm{SubobjectClassifier} )

The argument is a monomorphism m : A \rightarrow S. The output is its classifying morphism \chi_m : S \rightarrow \mathrm{SubobjectClassifier}.

1.2-5 ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier

Returns: a morphism in \mathrm{Hom}( \mathrm{Target}(m), \mathrm{SubobjectClassifier} )

The arguments are a monomorphism m : A \rightarrow S and the subobject classifier \Omega. The output is the classifying morphism of the monomorphism \chi_m : S \rightarrow \mathrm{SubobjectClassifier}.

1.2-6 SubobjectOfClassifyingMorphism

Returns: a monomorphism in \mathrm{Hom}( A, S )

The argument is a classifying morphism \chi : S \rightarrow \Omega. The output is the subobject monomorphism of the classifying morphism, m : A \rightarrow S.

1.2-7 ListOfSubobjects

Returns: a list of monomorphisms into A.

The argument is an object A. The output is a list of all subobjects of A.

1.3 Truth morphisms

1.3-1 TruthMorphismOfTrue

Returns: a morphism in \mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{SubobjectClassifier} )

The argument is a category C. The output is the truth morphism \mathrm{true}: \mathrm{TerminalObject} \rightarrow \mathrm{SubobjectClassifier}.

1.3-2 TruthMorphismOfTrueWithGivenObjects

Returns: a morphism in \mathrm{Hom}( T, \Omega )

The arguments are the terminal object of the category and the subobject classifier. The output is the truth morphism \mathrm{true}: T \rightarrow \Omega.

1.3-3 TruthMorphismOfFalse

Returns: a morphism in \mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{SubobjectClassifier} )

The argument is a category C. The output is the truth morphism \mathrm{false}: \mathrm{TerminalObject} \rightarrow \mathrm{SubobjectClassifier}.

1.3-4 TruthMorphismOfFalseWithGivenObjects

Returns: a morphism in \mathrm{Hom}( T, \Omega )

The arguments are the terminal object T of the category and the subobject classifier Omega. The output is the truth morphism \mathrm{false}: T \rightarrow \Omega.

1.3-5 TruthMorphismOfNot

Returns: a morphism in \mathrm{Hom}( \mathrm{SubobjectClassifier}, \mathrm{SubobjectClassifier} )

The argument is a category C. The output is the truth endomorphism \mathrm{not}: \mathrm{SubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}.

1.3-6 TruthMorphismOfNotWithGivenObjects

Returns: a morphism in \mathrm{Hom}( \Omega, \Omega )

The arguments are a subobject classifier Omega as first and as second argument. The output is the truth endomorphism \mathrm{not}: \Omega \rightarrow \Omega.

1.3-7 TruthMorphismOfAnd

Returns: a morphism in \mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )

The argument is a category C. The output is the truth morphism \mathrm{and}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}.

1.3-8 TruthMorphismOfAndWithGivenObjects

Returns: a morphism in \mathrm{Hom}( \Omega^{\times 2}, \Omega )

The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \mathrm{and}: \Omega^{\times 2} \rightarrow \Omega.

1.3-9 TruthMorphismOfOr

Returns: a morphism in \mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )

The argument is a category C. The output is the truth morphism \mathrm{or}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}.

1.3-10 TruthMorphismOfOrWithGivenObjects

Returns: a morphism in \mathrm{Hom}( \Omega^{\times 2}, \Omega )

The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \mathrm{or}: \Omega^{\times 2} \rightarrow \Omega.

1.3-11 TruthMorphismOfImplies

Returns: a morphism in \mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )

The argument is a category C. The output is the truth morphism \mathrm{implies}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}.

1.3-12 TruthMorphismOfImpliesWithGivenObjects

Returns: a morphism in \mathrm{Hom}( \Omega^{\times 2}, \Omega )

The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \mathrm{implies}: \Omega^{\times 2} \rightarrow \Omega.

1.4 Power object

1.4-1 PowerObject

Returns: an object

The argument is an object a. The output is the power object P(a) of a.

1.4-2 PowerObjectFunctorial

Returns: a morphism in \mathrm{Hom}( \mathrm{PowerObject}(b), \mathrm{PowerObject}(a) )

The argument is a morphism f:a \to b. The output is the power morphism of P(f): P(b) \to P(a).

gap> LoadPackage( "FinSetsForCAP" );
true
gap> a := FinSet( 3 );
|3|
gap> b := FinSet( 4 );
|4|
gap> f := MapOfFinSets( a, [ 0, 1, 1 ], b );
|3| → |4|
gap> Pf := PowerObjectFunctorial( f );
|16| → |8|
gap> Display( Pf );
{ 0,..., 15 } ⱶ[ 0, 1, 6, 7, 0, 1, 6, 7, 0, 1, 6, 7, 0, 1, 6, 7 ]→ { 0,..., 7 }

1.4-3 PowerObjectFunctorialWithGivenPowerObjects

Returns: a morphism in \mathrm{Hom}( Pb, Pa )

The arguments are an object Pb, a morphism f:a \to b, and object Pa, such that Pa= P(a) and Pb= P(b). The output is the power morphism of P(f): Pb \to Pa.

1.4-4 PowerObjectRightEvaluationMorphism

Returns: a morphism in \mathrm{Hom}( a \times \mathrm{PowerObject}(a), \Omega )

The argument is an object a. The output is the power object right evaluation morphism of \epsilon_a: a \times P(a) \to \Omega, where \Omega is the subobject classifier of CapCategory(a).

1.4-5 PowerObjectRightEvaluationMorphismWithGivenObjects

Returns: a morphism in \mathrm{Hom}( axPa, Omega )

The arguments are three objects Pa_xa, a, and Omega, such that axPa= a \times P(a) and Omega the subobject classifier of CapCategory(a). The output is the power object right evaluation morphism of \epsilon_a: axPa \to Omega.

1.4-6 PowerObjectLeftEvaluationMorphism

Returns: a morphism in \mathrm{Hom}( \mathrm{PowerObject}(a) \times a, \Omega )

The argument is an object a. The output is the power object left evaluation morphism of \epsilon_a: P(a) \times a \to \Omega, where \Omega is the subobject classifier of CapCategory(a).

1.4-7 PowerObjectLeftEvaluationMorphismWithGivenObjects

Returns: a morphism in \mathrm{Hom}( Pa_xa, Omega )

The arguments are three objects Pa_xa, a, and Omega, such that Pa_xa= P(a) \times a and Omega the subobject classifier of CapCategory(a). The output is the power object left evaluation morphism of \epsilon_a: Pa_xa \to Omega.

1.4-8 PRightTransposeMorphism

Returns: a morphism in \mathrm{Hom}( b, P(a) )

The arguments are two objects a, b, a morphism f: a \times b \to \Omega, where \Omega is the subobject classifier of CapCategory(f). The output is the P-right-transpose morphism b \to P(a), where P(a) = PowerObject( a ).

1.4-9 PRightTransposeMorphismWithGivenRange

Returns: a morphism in \mathrm{Hom}( b, Pa )

The arguments are two objects a, b, a morphism f: a \times b \to \Omega, and an object Pa, where \Omega is the subobject classifier of CapCategory(f) and Pa = PowerObject( a ). The output is the P-right-transpose morphism b \to Pa.

1.4-10 PLeftTransposeMorphism

Returns: a morphism in \mathrm{Hom}( a, P(b) )

The arguments are two objects a, b, a morphism f: a \times b \to \Omega, where \Omega is the subobject classifier of CapCategory(f). The output is the P-left-transpose morphism a \to P(b), where P(b) = PowerObject( b ).

1.4-11 PLeftTransposeMorphismWithGivenRange

Returns: a morphism in \mathrm{Hom}( a, Pb )

The arguments are two objects a, b, a morphism f: a \times b \to \Omega, and an object Pb, where \Omega is the subobject classifier of CapCategory(f) and Pb = PowerObject( b ). The output is the P-left-transpose morphism a \to Pb.

1.4-12 UpperSegmentOfRelation

Returns: a morphism in \mathrm{Hom}( a, \mathrm{PowerObject}( b ) )

The arguments are two objects a, b in a category C and a monomorphism mu: r \hookrightarrow a \times b defining a relation on a \times b. The output is the upper segment of the relation which is a morphism a \to Pb given by the adjunction, where Pb := PowerObject( b ) is the the power object of b.

1.4-13 UpperSegmentOfRelationWithGivenRange

Returns: a morphism in \mathrm{Hom}( a, Pb )

The arguments are two objects a, b in a category C, a monomorphism mu: r \hookrightarrow a \times b defining a relation on a \times b, and the power object Pb := PowerObject( b ) of b. The output is the upper segment of the relation which is a morphism a \to Pb given by the adjunction.

1.4-14 LowerSegmentOfRelation

Returns: a morphism in \mathrm{Hom}( b, \mathrm{PowerObject}( a ) )

The arguments are two objects a, b in a category C and a monomorphism mu:r \hookrightarrow a \times b defining a relation on a \times b. The output is the lower segment of the relation which is a morphism b \to Pa given by the adjunction, where Pa := PowerObject( a ) is the the power object of a.

1.4-15 LowerSegmentOfRelationWithGivenRange

Returns: a morphism in \mathrm{Hom}( b, Pa )

The arguments are two objects a, b in a category C, a monomorphism mu:r \hookrightarrow a \times b defining a relation on a \times b, and the power object Pa := PowerObject( a ) of a. The output is the lower segment of the relation which is a morphism b \to Pa given by the adjunction.

1.4-16 SingletonMorphism

Returns: a morphism in \mathrm{Hom}( a, \mathrm{PowerObject}(a) )

The argument is an object a. The output is the singleton morphism from a to the power object \mathrm{PowerObject}(a).

gap> LoadPackage( "FinSetsForCAP" );
true
gap> sFinSets := SkeletalCategoryOfFiniteSets( : no_precompiled_code := true );
SkeletalFinSets
gap> a := BigInt( 3 ) / sFinSets;
|3|
gap> sa := SingletonMorphism( a );
|3| ↪ |8|
gap> Display( sa );
{ 0, 1, 2 } ⱶ[ 1, 2, 4 ]→ { 0,..., 7 }
gap> sa = UpperSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) );
true
gap> sa = LowerSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) );
true

1.4-17 SingletonMorphismWithGivenPowerObject

Returns: a morphism in \mathrm{Hom}( a, Pa )

The arguments are an object a and an object Pa which is equal to the power object \mathrm{PowerObject}(a). The output is the singleton morphism from a to Pa.

1.4-18 IsomorphismOntoCartesianSquareOfPowerObject

Returns: a morphism in \mathrm{Hom}( \mathrm{Exponential}( a, \mathrm{CartesianSquareOfSubobjectClassifier}( C ) ), \mathrm{DirectProduct}( \mathrm{PowerObject}(a), \mathrm{PowerObject}(a) ) )

The argument is an object a in a category C. The output is the isomorphism \mathrm{Exponential}( a, \mathrm{CartesianSquareOfSubobjectClassifier}( C ) ) \rightarrow \mathrm{DirectProduct}( \mathrm{PowerObject}(a), \mathrm{PowerObject}(a) ).

gap> LoadPackage( "FinSetsForCAP" );
true
gap> a := FinSet( 2 );
|2|
gap> ia := IsomorphismOntoCartesianSquareOfPowerObject( a );
|16| ⭇ |16|
gap> Display( ia );
{ 0,..., 15 }\
 ⱶ[ 0, 1, 4, 5, 2, 3, 6, 7, 8, 9, 12, 13, 10, 11, 14, 15 ]→ { 0,..., 15 }

1.4-19 IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects

Returns: a morphism in \mathrm{Hom}( Exp\_a\_Omega2, PaxPa )

The arguments are an object the exponential Exp_a_Omega2 = Exponential( a, CartesianSquareOfSubobjectClassifier ), an object a in a category C, and the cartesian squre PaxPa of the power object PowerObject( a ). The output is the isomorphism Exp\_a\_Omega2 \stackrel{\sim}{\rightarrow} PaxPa

1.4-20 IntersectWithPreimagesWithGivenObjects

Returns: a morphism \mathrm{Hom}( PAxB, PA )

The input is the direct product PAxB = PA \times B, a morphism f: A \to B, and the power object PA = PowerObject(A). The output is the morphism PAxB \rightarrow PA, (T, b) \mapsto T \cap f^{-1}(b).

1.4-21 EmbeddingOfRelativePowerObject

Returns: a monomorphism \mathrm{Hom}( P_fa, Pa \times b )

The input is a morphism f: a \to b. The output is the embedding of the relative power object P_fa \hookrightarrow Pa \times b, where Pa = PowerObject(a).

1.4-22 RelativePowerObjectFibrationMorphism

Returns: a monomorphism \mathrm{Hom}( P_fa, b )

The input is a morphism f: a \to b. The output is the fibration morphism P_f: P_fa \rightarrow \times b, where is P_fa the relative power object of f.

1.4-23 RelativePowerObjectLeftEvaluationMorphism

Returns: a monomorphism \mathrm{Hom}( P_fa \times a, \Omega \times b )

The input is a morphism f: a \to b. The output is the evaluation morphism P_fa \times a \rightarrow \Omega \times b, where P_fa is the relative power object of f.

1.4-24 RightFiberMorphism

Returns: a morphism in \mathrm{Hom}( c \times P(b \times c), P(b) )

The arguments are two objects b, c. The output is the morphism c \times PowerObject(b \times c) \to PowerObject( b ) that for a given relation R \subseteq b \times c and an element y in the base c computes the fiber over y as subset of b.

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> a := FinSet( 3 );
|3|
gap> b := FinSet( 2 );
|2|
gap> right := RightFiberMorphism( a, b );
|128| → |8|
gap> LoadPackage( "LazyCategories", false );
true
gap> L := LazyCategory( SkeletalFinSets : primitive_operations := true );
LazyCategory( SkeletalFinSets )
gap> lazy_right := RightFiberMorphism( a / L, b / L );
<A morphism in LazyCategory( SkeletalFinSets )>

1.4-25 RightFiberMorphismWithGivenObjects

Returns: a morphism in \mathrm{Hom}( cxPbxc, Pb )

The arguments are four objects cxPbxc, b, c, Pb, where cxPbxc = c \times P(b \times c) and Pb = PowerObject( b ). The output is the morphism that for a given relation R \subseteq b \times c and an element y in the base c computes the fiber over y as subset of b.

1.4-26 LeftFiberMorphism

Returns: a morphism in \mathrm{Hom}( P(b \times c) \times b, P(c) )

The arguments are two objects b, c. The output is the morphism PowerObject(b \times c) \times b \to PowerObject( c ) that for a given relation R \subseteq b \times c and an element x in the base b computes the fiber over x as subset of c.

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> a := FinSet( 2 );
|2|
gap> b := FinSet( 3 );
|3|
gap> left := LeftFiberMorphism( a, b );
|128| → |8|
gap> LoadPackage( "LazyCategories", false );
true
gap> L := LazyCategory( SkeletalFinSets : primitive_operations := true );
LazyCategory( SkeletalFinSets )
gap> lazy_left := LeftFiberMorphism( a / L, b / L );
<A morphism in LazyCategory( SkeletalFinSets )>

1.4-27 LeftFiberMorphismWithGivenObjects

Returns: a morphism in \mathrm{Hom}( Pbxc_xb, Pc )

The arguments are four objects Pbxc_xb, b, c, Pc, where Pbxc_xb = P(b \times c) \times b and Pc = PowerObject( c ). The output is the morphism that for a given relation R \subseteq b \times c and an element x in the base b computes the fiber over x as subset of c.

1.4-28 SingletonSupportOfRelationsWithGivenObjects

Returns: a morphism in \mathrm{Hom}( Pbxc, Pb )

Return the morphism that for a given relation R \subseteq b \times c computes the subset of b over which R is a singleton.

1.5 Relative truth morphisms

1.5-1 RelativeTruthMorphismOfTrue

Returns: a morphism in \mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{PowerObect}( a ) )

The argument is an object a in a category C. The output is the relative truth morphism \mathrm{true}: \mathrm{TerminalObject} \rightarrow \mathrm{PowerObject}( a ).

1.5-2 RelativeTruthMorphismOfTrueWithGivenObjects

Returns: a morphism in \mathrm{Hom}( T, Pa )

The arguments are the terminal object of the category C, an object a, and the power object Pa of a. The output is the relative truth morphism \mathrm{true}: T \rightarrow Pa.

1.5-3 RelativeTruthMorphismOfFalse

Returns: a morphism in \mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{PowerObect}( a ) )

The argument is an object a in a category C. The output is the relative truth morphism \mathrm{false}: \mathrm{TerminalObject} \rightarrow \mathrm{PowerObject}( a ).

1.5-4 RelativeTruthMorphismOfFalseWithGivenObjects

Returns: a morphism in \mathrm{Hom}( T, Pa )

The arguments are the terminal object of the category C, an object a, and the power object Pa of a. The output is the relative truth morphism \mathrm{false}: T \rightarrow Pa.

1.5-5 RelativeTruthMorphismOfNot

Returns: a morphism in \mathrm{Hom}( \mathrm{PowerObject}( a ), \mathrm{PowerObect}( a ) )

The argument is an object a in a category C. The output is the relative truth endomorphism \mathrm{not}: \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a ).

1.5-6 RelativeTruthMorphismOfNotWithGivenObjects

Returns: a morphism in \mathrm{Hom}( Pa, Pa )

The arguments are the power object Pa of a, the object a, and Pa. The output is the relative truth endomorphism \mathrm{not}: Pa \rightarrow Pa.

1.5-7 RelativeTruthMorphismOfAnd

Returns: a morphism in \mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )

The argument is an object a in a category C. The output is the relative truth morphism \mathrm{and}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a ).

1.5-8 RelativeTruthMorphismOfAndWithGivenObjects

Returns: a morphism in \mathrm{Hom}( PaxPa, Pa )

The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \mathrm{and}: PaxPa \rightarrow Pa.

1.5-9 RelativeTruthMorphismOfOr

Returns: a morphism in \mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )

The argument is an object a in a category C. The output is the relative truth morphism \mathrm{or}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a ).

1.5-10 RelativeTruthMorphismOfOrWithGivenObjects

Returns: a morphism in \mathrm{Hom}( PaxPa, Pa )

The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \mathrm{or}: PaxPa \rightarrow Pa.

1.5-11 RelativeTruthMorphismOfImplies

Returns: a morphism in \mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )

The argument is an object a in a category C. The output is the relative truth morphism \mathrm{implies}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a ).

1.5-12 RelativeTruthMorphismOfImpliesWithGivenObjects

Returns: a morphism in \mathrm{Hom}( PaxPa, Pa )

The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \mathrm{implies}: PaxPa \rightarrow Pa.

gap> LoadPackage( "FinSetsForCAP" );
true
gap> sFinSets := SkeletalFinSets;
SkeletalFinSets
gap> t := TerminalObject( sFinSets );
|1|
gap> TruthMorphismOfFalse( sFinSets ) = RelativeTruthMorphismOfFalse( t );
true
gap> TruthMorphismOfTrue( sFinSets ) = RelativeTruthMorphismOfTrue( t );
true
gap> TruthMorphismOfNot( sFinSets ) = RelativeTruthMorphismOfNot( t );
true
gap> TruthMorphismOfAnd( sFinSets ) = RelativeTruthMorphismOfAnd( t );
true
gap> TruthMorphismOfOr( sFinSets ) = RelativeTruthMorphismOfOr( t );
true
gap> TruthMorphismOfImplies( sFinSets ) = RelativeTruthMorphismOfImplies( t );
true
gap> a := FinSet( 2 );
|2|
gap> fPa := RelativeTruthMorphismOfFalse( a );
|1| → |4|
gap> Display( fPa );
{ 0 } ⱶ[ 0 ]→ { 0,..., 3 }
gap> tPa := RelativeTruthMorphismOfTrue( a );
|1| → |4|
gap> Display( tPa );
{ 0 } ⱶ[ 3 ]→ { 0,..., 3 }
gap> nPa := RelativeTruthMorphismOfNot( a );
|4| → |4|
gap> Display( nPa );
{ 0,..., 3 } ⱶ[ 3, 2, 1, 0 ]→ { 0,..., 3 }
gap> aPa := RelativeTruthMorphismOfAnd( a );
|16| → |4|
gap> Display( aPa );
{ 0,..., 15 } ⱶ[ 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 2, 2, 0, 1, 2, 3 ]→ { 0,..., 3 }
gap> oPa := RelativeTruthMorphismOfOr( a );
|16| → |4|
gap> Display( oPa );
{ 0,..., 15 } ⱶ[ 0, 1, 2, 3, 1, 1, 3, 3, 2, 3, 2, 3, 3, 3, 3, 3 ]→ { 0,..., 3 }
gap> iPa := RelativeTruthMorphismOfImplies( a );
|16| → |4|
gap> Display( iPa );
{ 0,..., 15 } ⱶ[ 3, 2, 1, 0, 3, 3, 1, 1, 3, 2, 3, 2, 3, 3, 3, 3 ]→ { 0,..., 3 }

1.6 Heyting algebra of subobjects

1.6-1 PseudoComplementSubobject

Returns: an object

The argument is a monomorphism \iota: S \hookrightarrow A. The output is the pseudo-complement of S in A, i.e., the pseudo-complement object of \iota.

1.6-2 EmbeddingOfPseudoComplementSubobject

Returns: an object

The argument is a monomorphism \iota: S \hookrightarrow A. The output is the embedding PseudoComplementSubobject(\iota) \hookrightarrow A of pseudo-complement object of \iota.

1.6-3 EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement

Returns: an object

The argument is a monomorphism \iota: S \hookrightarrow A and an object T with IsEqualForObjects(T, PseudoComplementSubobject(\iota)). The output is the embedding of \iota:T \hookrightarrow A of pseudo-complement object T of \iota.

1.6-4 IntersectionSubobject

Returns: an object

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2. The output is the intersection of S_1 and S_2, which is naturally isomorphic to the pullback of \iota_1 and \iota_2.

1.6-5 EmbeddingOfIntersectionSubobject

Returns: a monomorphism into A

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2. The output is the embedding IntersectionSubobject(\iota) \hookrightarrow A of their intersection subobject.

1.6-6 EmbeddingOfIntersectionSubobjectWithGivenIntersection

Returns: a monomorphism in \mathrm{Hom}( T, A )

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2 and an object T with IsEqualForObjects(T, IntersectionSubobject(iota1, iota2)). The output is the embedding T \hookrightarrow A of their intersection subobject T.

1.6-7 UnionSubobject

Returns: an object

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2. The output is the union of S_1 and S_2, which is naturally isomorphic to the image object of the coproduct morphism of \iota_1 and \iota_2.

1.6-8 EmbeddingOfUnionSubobject

Returns: a monomorphism into A

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2. The output is the embedding UnionSubobject(iota1, iota2) \hookrightarrow A of their union subobject.

1.6-9 EmbeddingOfUnionSubobjectWithGivenUnion

Returns: a monomorphism in \mathrm{Hom}( U, A )

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2 and an object U with IsEqualForObjects(U, UnionSubobject(iota1, iota2)). The output is the embedding U \hookrightarrow A of their union subobject U.

1.6-10 RelativePseudoComplementSubobject

Returns: an object

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2. The output is the relative pseudo-complement of S_1 relative to S_2.

1.6-11 EmbeddingOfRelativePseudoComplementSubobject

Returns: a monomorphism into A

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2. The output is the embedding RelativePseudoComplementSubobject(iota1, iota2) \hookrightarrow A of their relative pseudo-complement into A.

1.6-12 EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication

Returns: a monomorphism in \mathrm{Hom}( I, A )

The arguments are two monomorphisms \iota_i: S_i \hookrightarrow A for i=1,2 and an object I with IsEqualForObjects(I, RelativePseudoComplementSubobject(iota1, iota2)). The output is the embedding I \hookrightarrow A of their relative pseudo-complement I into A.

1.7 Pushout complements

1.7-1 Example in FinSets

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

gap> LoadPackage( "FinSetsForCAP" );
true
gap> K := FinSet( [ 2, 3, 5 ] );;
gap> Display( K );
[ 2, 3, 5 ]
gap> L := FinSet( [ 0, 1, 2, 3, 5, 6 ] );;
gap> Display( L );
[ 0, 1, 2, 3, 5, 6 ]
gap> l := EmbeddingOfFinSets( K, L );
<A monomorphism in FinSets>
gap> G := FinSet( [ 0, 1, 2, 3, 4, 5, 6, 10 ] );;
gap> Display( G );
[ 0, 1, 2, 3, 4, 5, 6, 10 ]
gap> m := EmbeddingOfFinSets( L, G );
<A monomorphism in FinSets>

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

gap> HasPushoutComplement( l, m );
true
gap> c := PushoutComplement( l, m );
<A monomorphism in FinSets>
gap> D := Source( c );;
gap> Display( D );
[ 2, 3, 4, 5, 10 ]

1.7-2 Example in SkeletalFinSets

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

gap> LoadPackage( "FinSetsForCAP" );
true
gap> K := FinSet( 3 );
|3|
gap> L := FinSet( 6 );
|6|
gap> l := MapOfFinSets( K, [ 2, 3, 4 ], L );; IsMonomorphism( l );; l;
|3| ↪ |6|
gap> Display( l );
{ 0, 1, 2 } ⱶ[ 2, 3, 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:

gap> HasPushoutComplement( l, m );
true
gap> c := PushoutComplement( l, m );
|5| → |8|
gap> Display( c );
{ 0,..., 4 } ⱶ[ 2, 3, 4, 5, 7 ]→ { 0,..., 7 }

1.7-3 HasPushoutComplement

Returns: a boolean

The arguments are two composable morphisms l: K \rightarrow L, m: L \rightarrow G. The output is true if there exists a morphism d: K \rightarrow D and a morphism g: D \rightarrow G such that the four morphisms l,d,m,g form a pushout diagram, i.e., such that m=InjectionOfCofactorOfPushoutWithGivenPushout([l,d], 1) and g=InjectionOfCofactorOfPushoutWithGivenPushout([l,d], 2). Otherwise the output is false.

1.7-4 PushoutComplement

Returns: a morphism

The arguments are two composable morphisms l: K \rightarrow L, m: L \rightarrow G. The output is a morphism d: K \rightarrow D such that there exists a morphism g: D \rightarrow G turing the four morphisms l,d,m,g into a pushout diagram, i.e., such that m=InjectionOfCofactorOfPushoutWithGivenPushout([l,d], 1) and g=InjectionOfCofactorOfPushoutWithGivenPushout([l,d], 2).

1.8 Double-pushout rewriting

1.8-1 DPO

Returns: a pair of morhpisms

Compute the double-pushout of m along the rule given by [ l, r ].

We start by defining a linear rewriting rule as a span of two monos L \stackrel{l}{\hookleftarrow} K \stackrel{r}{\hookrightarrow} R in FinSets:

gap> LoadPackage( "FinSetsForCAP" );
true
gap> K := FinSet( [ 2, 3, 5 ] );;
gap> Length( K );
3
gap> Display( K );
[ 2, 3, 5 ]
gap> L := FinSet( [ 0, 1, 2, 3, 5, 6 ] );;
gap> Length( L );
6
gap> Display( L );
[ 0, 1, 2, 3, 5, 6 ]
gap> R := FinSet( [ 2, 3, 4, 5, 7 ] );;
gap> Length( R );
5
gap> Display( R );
[ 2, 3, 4, 5, 7 ]
gap> l := EmbeddingOfFinSets( K, L );
<A monomorphism in FinSets>
gap> r := EmbeddingOfFinSets( K, R );
<A monomorphism in FinSets>

Then we define an object within the context of the rule and a matching L \stackrel{m}{\hookrightarrow} G:

gap> G := FinSet( [ 0, 1, 2, 3, 4, 5, 6, 10 ] );;
gap> Length( G );
8
gap> Display( G );
[ 0, 1, 2, 3, 4, 5, 6, 10 ]
gap> m := EmbeddingOfFinSets( L, G );
<A monomorphism in FinSets>

The double-pushout rewriting now applies the linear rule (l,r) to the matriching m:

gap> p := DPO( m, l, r );;
gap> h := p[1];
<A monomorphism in FinSets>
gap> p := p[2];
<A monomorphism in FinSets>
gap> H := Target( p );;
gap> Length( H );
7
gap> Display( H );
[ [ [ 1, 2 ], [ 2, 2 ] ],\
 [ [ 1, 3 ], [ 2, 3 ] ],\
 [ [ 1, 4 ] ],\
 [ [ 1, 5 ], [ 2, 5 ] ],\
 [ [ 1, 10 ] ],\
 [ [ 2, 4 ] ],\
 [ [ 2, 7 ] ] ]

This means

• 2, 3, 5 are in K and hence in both G and R;

• 10 is only in G;

• 7 are only in R;

• 4 is in G but it must be duplicated since it is also in R but not in K.

1.9 Lawvere-Tierney topologies

Compute the Lawvere-Tierney topologies of SkeletalFinSets:

gap> LoadPackage( "FinSetsForCAP" );
true
gap> LTI := LawvereTierneyLocalModalityOperators( SkeletalFinSets );;
gap> Perform( LTI, Display );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 }
{ 0, 1 } ⱶ[ 1, 1 ]→ { 0, 1 }
gap> LTS := LawvereTierneySubobjects( SkeletalFinSets );;
gap> Perform( LTS, Display );
{ 0 } ⱶ[ 1 ]→ { 0, 1 }
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 }
gap> LTC := LawvereTierneyEmbeddingsOfSubobjectClassifiers( SkeletalFinSets );;
gap> Perform( LTC, Display );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 }
{ 0 } ⱶ[ 1 ]→ { 0, 1 }

1.9-1 LawvereTierneyLocalModalityOperators

Returns: a list of endomorphisms in \mathrm{Hom}( \mathrm{SubobjectClassifier}( T ), \mathrm{SubobjectClassifier}( T ) )

The input is an elementary topos T. The output is the list of Lawvere-Tierney idempotents of the subobject classifier of the topos T.

1.9-2 LawvereTierneySubobjects

Returns: a list of monomorphisms into \mathrm{SubobjectClassifier}( T )

The input is an elementary topos T. The output is the list of Lawvere-Tierney subobjects of the subobject classifier of the topos T.

1.9-3 LawvereTierneyEmbeddingsOfSubobjectClassifiers

Returns: a list of monomorphisms \mathrm{SubobjectClassifier}( T )

The input is an elementary topos T. The output is the list of embeddings of the subobject classifiers of full sheaf subtoposes (with respect to the Lawvere-Tierney topologies of the topos T) into the subobject classifier of T.

1.10 Add-methods

1.10-1 AddCartesianSquareOfSubobjectClassifier

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianSquareOfSubobjectClassifier. F: ( ) \mapsto \mathtt{CartesianSquareOfSubobjectClassifier}().

1.10-2 AddClassifyingMorphismOfSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClassifyingMorphismOfSubobject. F: ( alpha ) \mapsto \mathtt{ClassifyingMorphismOfSubobject}(alpha).

1.10-3 AddClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier. F: ( alpha, Omega ) \mapsto \mathtt{ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier}(alpha, Omega).

1.10-4 AddCoproductComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoproductComplement. F: ( iota ) \mapsto \mathtt{CoproductComplement}(iota).

1.10-5 AddDirectProductComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductComplement. F: ( pi ) \mapsto \mathtt{DirectProductComplement}(pi).

1.10-6 AddEmbeddingOfIntersectionSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation EmbeddingOfIntersectionSubobject. F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfIntersectionSubobject}(iota1, iota2).

1.10-7 AddEmbeddingOfIntersectionSubobjectWithGivenIntersection

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation EmbeddingOfIntersectionSubobjectWithGivenIntersection. F: ( iota1, iota2, intersection ) \mapsto \mathtt{EmbeddingOfIntersectionSubobjectWithGivenIntersection}(iota1, iota2, intersection).

1.10-8 AddEmbeddingOfPseudoComplementSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation EmbeddingOfPseudoComplementSubobject. F: ( iota ) \mapsto \mathtt{EmbeddingOfPseudoComplementSubobject}(iota).

1.10-9 AddEmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement. F: ( iota, complement ) \mapsto \mathtt{EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement}(iota, complement).

1.10-10 AddEmbeddingOfRelativePseudoComplementSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation EmbeddingOfRelativePseudoComplementSubobject. F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfRelativePseudoComplementSubobject}(iota1, iota2).

1.10-11 AddEmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication. F: ( iota1, iota2, implication ) \mapsto \mathtt{EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication}(iota1, iota2, implication).

1.10-12 AddEmbeddingOfUnionSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation EmbeddingOfUnionSubobject. F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfUnionSubobject}(iota1, iota2).

1.10-13 AddEmbeddingOfUnionSubobjectWithGivenUnion

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation EmbeddingOfUnionSubobjectWithGivenUnion. F: ( iota1, iota2, union ) \mapsto \mathtt{EmbeddingOfUnionSubobjectWithGivenUnion}(iota1, iota2, union).

1.10-14 AddExactCoverWithGlobalElements

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExactCoverWithGlobalElements. F: ( arg2 ) \mapsto \mathtt{ExactCoverWithGlobalElements}(arg2).

1.10-15 AddHasPushoutComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation HasPushoutComplement. F: ( arg2, arg3 ) \mapsto \mathtt{HasPushoutComplement}(arg2, arg3).

1.10-16 AddIndexOfNonliftableMorphismFromDistinguishedObject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IndexOfNonliftableMorphismFromDistinguishedObject. F: ( iota ) \mapsto \mathtt{IndexOfNonliftableMorphismFromDistinguishedObject}(iota).

1.10-17 AddInjectionOfCoproductComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InjectionOfCoproductComplement. F: ( iota ) \mapsto \mathtt{InjectionOfCoproductComplement}(iota).

1.10-18 AddInjectionOfCoproductComplementWithGivenCoproductComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InjectionOfCoproductComplementWithGivenCoproductComplement. F: ( iota, complement ) \mapsto \mathtt{InjectionOfCoproductComplementWithGivenCoproductComplement}(iota, complement).

1.10-19 AddIntersectionSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IntersectionSubobject. F: ( arg2, arg3 ) \mapsto \mathtt{IntersectionSubobject}(arg2, arg3).

1.10-20 AddIsomorphismOntoCartesianSquareOfPowerObject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismOntoCartesianSquareOfPowerObject. F: ( a ) \mapsto \mathtt{IsomorphismOntoCartesianSquareOfPowerObject}(a).

1.10-21 AddIsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects. F: ( ExpaOmega2, a, PaxPa ) \mapsto \mathtt{IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects}(ExpaOmega2, a, PaxPa).

1.10-22 AddLawvereTierneyEmbeddingsOfSubobjectClassifiers

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LawvereTierneyEmbeddingsOfSubobjectClassifiers. F: ( ) \mapsto \mathtt{LawvereTierneyEmbeddingsOfSubobjectClassifiers}().

1.10-23 AddLawvereTierneyLocalModalityOperators

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LawvereTierneyLocalModalityOperators. F: ( ) \mapsto \mathtt{LawvereTierneyLocalModalityOperators}().

1.10-24 AddLawvereTierneySubobjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LawvereTierneySubobjects. F: ( ) \mapsto \mathtt{LawvereTierneySubobjects}().

1.10-25 AddLeftFiberMorphism

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftFiberMorphism. F: ( b, c ) \mapsto \mathtt{LeftFiberMorphism}(b, c).

1.10-26 AddLeftFiberMorphismWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftFiberMorphismWithGivenObjects. F: ( Pbxc_b, b, c, Pc ) \mapsto \mathtt{LeftFiberMorphismWithGivenObjects}(Pbxc_b, b, c, Pc).

1.10-27 AddListOfSubobjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ListOfSubobjects. F: ( arg2 ) \mapsto \mathtt{ListOfSubobjects}(arg2).

1.10-28 AddLowerSegmentOfRelation

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LowerSegmentOfRelation. F: ( a, b, mu ) \mapsto \mathtt{LowerSegmentOfRelation}(a, b, mu).

1.10-29 AddLowerSegmentOfRelationWithGivenRange

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LowerSegmentOfRelationWithGivenRange. F: ( a, b, mu, Pa ) \mapsto \mathtt{LowerSegmentOfRelationWithGivenRange}(a, b, mu, Pa).

1.10-30 AddNonliftableMorphismFromDistinguishedObject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation NonliftableMorphismFromDistinguishedObject. F: ( iota ) \mapsto \mathtt{NonliftableMorphismFromDistinguishedObject}(iota).

1.10-31 AddPLeftTransposeMorphism

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PLeftTransposeMorphism. F: ( a, b, f ) \mapsto \mathtt{PLeftTransposeMorphism}(a, b, f).

1.10-32 AddPLeftTransposeMorphismWithGivenRange

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PLeftTransposeMorphismWithGivenRange. F: ( a, b, f, Pb ) \mapsto \mathtt{PLeftTransposeMorphismWithGivenRange}(a, b, f, Pb).

1.10-33 AddPRightTransposeMorphism

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PRightTransposeMorphism. F: ( a, b, f ) \mapsto \mathtt{PRightTransposeMorphism}(a, b, f).

1.10-34 AddPRightTransposeMorphismWithGivenRange

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PRightTransposeMorphismWithGivenRange. F: ( a, b, f, Pa ) \mapsto \mathtt{PRightTransposeMorphismWithGivenRange}(a, b, f, Pa).

1.10-35 AddPowerObject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PowerObject. F: ( arg2 ) \mapsto \mathtt{PowerObject}(arg2).

1.10-36 AddPowerObjectFunctorial

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PowerObjectFunctorial. F: ( f ) \mapsto \mathtt{PowerObjectFunctorial}(f).

1.10-37 AddPowerObjectFunctorialWithGivenPowerObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PowerObjectFunctorialWithGivenPowerObjects. F: ( Pb, f, Pa ) \mapsto \mathtt{PowerObjectFunctorialWithGivenPowerObjects}(Pb, f, Pa).

1.10-38 AddPowerObjectLeftEvaluationMorphism

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PowerObjectLeftEvaluationMorphism. F: ( a ) \mapsto \mathtt{PowerObjectLeftEvaluationMorphism}(a).

1.10-39 AddPowerObjectLeftEvaluationMorphismWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PowerObjectLeftEvaluationMorphismWithGivenObjects. F: ( Pa_xa, a, Omega ) \mapsto \mathtt{PowerObjectLeftEvaluationMorphismWithGivenObjects}(Pa_xa, a, Omega).

1.10-40 AddPowerObjectRightEvaluationMorphism

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PowerObjectRightEvaluationMorphism. F: ( a ) \mapsto \mathtt{PowerObjectRightEvaluationMorphism}(a).

1.10-41 AddPowerObjectRightEvaluationMorphismWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PowerObjectRightEvaluationMorphismWithGivenObjects. F: ( axPa, a, Omega ) \mapsto \mathtt{PowerObjectRightEvaluationMorphismWithGivenObjects}(axPa, a, Omega).

1.10-42 AddProjectionInDirectProductComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ProjectionInDirectProductComplement. F: ( pi ) \mapsto \mathtt{ProjectionInDirectProductComplement}(pi).

1.10-43 AddProjectionInDirectProductComplementWithGivenDirectProductComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ProjectionInDirectProductComplementWithGivenDirectProductComplement. F: ( pi, complement ) \mapsto \mathtt{ProjectionInDirectProductComplementWithGivenDirectProductComplement}(pi, complement).

1.10-44 AddPseudoComplementSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PseudoComplementSubobject. F: ( arg2 ) \mapsto \mathtt{PseudoComplementSubobject}(arg2).

1.10-45 AddPushoutComplement

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation PushoutComplement. F: ( l, m ) \mapsto \mathtt{PushoutComplement}(l, m).

1.10-46 AddRelativePseudoComplementSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativePseudoComplementSubobject. F: ( arg2, arg3 ) \mapsto \mathtt{RelativePseudoComplementSubobject}(arg2, arg3).

1.10-47 AddRelativeTruthMorphismOfAnd

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfAnd. F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfAnd}(a).

1.10-48 AddRelativeTruthMorphismOfAndWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfAndWithGivenObjects. F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfAndWithGivenObjects}(PaxPa, a, Pa).

1.10-49 AddRelativeTruthMorphismOfFalse

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfFalse. F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfFalse}(a).

1.10-50 AddRelativeTruthMorphismOfFalseWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfFalseWithGivenObjects. F: ( T, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfFalseWithGivenObjects}(T, a, Pa).

1.10-51 AddRelativeTruthMorphismOfImplies

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfImplies. F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfImplies}(a).

1.10-52 AddRelativeTruthMorphismOfImpliesWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfImpliesWithGivenObjects. F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfImpliesWithGivenObjects}(PaxPa, a, Pa).

1.10-53 AddRelativeTruthMorphismOfNot

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfNot. F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfNot}(a).

1.10-54 AddRelativeTruthMorphismOfNotWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfNotWithGivenObjects. F: ( Pa, a, Pa1 ) \mapsto \mathtt{RelativeTruthMorphismOfNotWithGivenObjects}(Pa, a, Pa1).

1.10-55 AddRelativeTruthMorphismOfOr

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfOr. F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfOr}(a).

1.10-56 AddRelativeTruthMorphismOfOrWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfOrWithGivenObjects. F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfOrWithGivenObjects}(PaxPa, a, Pa).

1.10-57 AddRelativeTruthMorphismOfTrue

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfTrue. F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfTrue}(a).

1.10-58 AddRelativeTruthMorphismOfTrueWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RelativeTruthMorphismOfTrueWithGivenObjects. F: ( T, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfTrueWithGivenObjects}(T, a, Pa).

1.10-59 AddRightFiberMorphism

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RightFiberMorphism. F: ( b, c ) \mapsto \mathtt{RightFiberMorphism}(b, c).

1.10-60 AddRightFiberMorphismWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RightFiberMorphismWithGivenObjects. F: ( cxPbxc, b, c, Pb ) \mapsto \mathtt{RightFiberMorphismWithGivenObjects}(cxPbxc, b, c, Pb).

1.10-61 AddSingletonMorphism

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation SingletonMorphism. F: ( a ) \mapsto \mathtt{SingletonMorphism}(a).

1.10-62 AddSingletonMorphismWithGivenPowerObject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation SingletonMorphismWithGivenPowerObject. F: ( a, Pa ) \mapsto \mathtt{SingletonMorphismWithGivenPowerObject}(a, Pa).

1.10-63 AddSubobjectClassifier

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation SubobjectClassifier. F: ( ) \mapsto \mathtt{SubobjectClassifier}().

1.10-64 AddSubobjectOfClassifyingMorphism

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation SubobjectOfClassifyingMorphism. F: ( alpha ) \mapsto \mathtt{SubobjectOfClassifyingMorphism}(alpha).

1.10-65 AddTruthMorphismOfAnd

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfAnd. F: ( ) \mapsto \mathtt{TruthMorphismOfAnd}().

1.10-66 AddTruthMorphismOfAndWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfAndWithGivenObjects. F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfAndWithGivenObjects}(Omega2, Omega).

1.10-67 AddTruthMorphismOfFalse

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfFalse. F: ( ) \mapsto \mathtt{TruthMorphismOfFalse}().

1.10-68 AddTruthMorphismOfFalseWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfFalseWithGivenObjects. F: ( T, Omega ) \mapsto \mathtt{TruthMorphismOfFalseWithGivenObjects}(T, Omega).

1.10-69 AddTruthMorphismOfImplies

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfImplies. F: ( ) \mapsto \mathtt{TruthMorphismOfImplies}().

1.10-70 AddTruthMorphismOfImpliesWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfImpliesWithGivenObjects. F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfImpliesWithGivenObjects}(Omega2, Omega).

1.10-71 AddTruthMorphismOfNot

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfNot. F: ( ) \mapsto \mathtt{TruthMorphismOfNot}().

1.10-72 AddTruthMorphismOfNotWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfNotWithGivenObjects. F: ( Omega, Omega1 ) \mapsto \mathtt{TruthMorphismOfNotWithGivenObjects}(Omega, Omega1).

1.10-73 AddTruthMorphismOfOr

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfOr. F: ( ) \mapsto \mathtt{TruthMorphismOfOr}().

1.10-74 AddTruthMorphismOfOrWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfOrWithGivenObjects. F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfOrWithGivenObjects}(Omega2, Omega).

1.10-75 AddTruthMorphismOfTrue

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfTrue. F: ( ) \mapsto \mathtt{TruthMorphismOfTrue}().

1.10-76 AddTruthMorphismOfTrueWithGivenObjects

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TruthMorphismOfTrueWithGivenObjects. F: ( T, Omega ) \mapsto \mathtt{TruthMorphismOfTrueWithGivenObjects}(T, Omega).

1.10-77 AddUnionSubobject

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation UnionSubobject. F: ( arg2, arg3 ) \mapsto \mathtt{UnionSubobject}(arg2, arg3).

1.10-78 AddUpperSegmentOfRelation

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation UpperSegmentOfRelation. F: ( a, b, mu ) \mapsto \mathtt{UpperSegmentOfRelation}(a, b, mu).

1.10-79 AddUpperSegmentOfRelationWithGivenRange

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation UpperSegmentOfRelationWithGivenRange. F: ( a, b, mu, Pb ) \mapsto \mathtt{UpperSegmentOfRelationWithGivenRange}(a, b, mu, Pb).

1.11 Coproduct and direct product complements

1.11-1 CoproductComplement

Returns: an object

The argument is a morphism iota: S \to T which is a coproduct injection of some binary coproduct. The output is an object C such that S \sqcup C \cong T.

1.11-2 InjectionOfCoproductComplement

Returns: a morphism in \mathrm{Hom}( C, \mathrm{Target}( \iota ) )

The argument is a morphism iota: S \to T which is a coproduct injection of some binary coproduct. The output is a coproduct injection \iota_2: C \to T such that UniversalMorphismFromCoproduct( iota, \iota_2 ): S \sqcup C \to T is an isomorphism.

1.11-3 InjectionOfCoproductComplementWithGivenCoproductComplement

Returns: a morphism in \mathrm{Hom}( C, \mathrm{Target}( \iota ) )

The argument is a morphism iota: S \to T which is a coproduct injection of some binary coproduct and a coproduct complement C. The output is a coproduct injection \iota_2: C \to T such that UniversalMorphismFromCoproduct( iota, \iota_2 ): S \sqcup C \to T is an isomorphism.

1.11-4 DirectProductComplement

Returns: an object

The argument is a morphism pi: S \to T which is a product projection of some binary direct product. The output is an object C such that S \times C \cong T.

1.11-5 ProjectionInDirectProductComplement

Returns: a morphism in \mathrm{Hom}( C, \mathrm{Target}( \pi ) )

The argument is a morphism pi: S \to T which is a direct product projection of some binary direct product. The output is a direct product projection \pi_2: C \to T such that UniversalMorphismIntoDirectProduct( pi, \pi_2 ): T \to S \times C is an isomorphism.

1.11-6 ProjectionInDirectProductComplementWithGivenDirectProductComplement

Returns: a morphism in \mathrm{Hom}( C, \mathrm{Target}( \pi ) )

The argument is a morphism pi: S \to T which is a direct product projection of some binary direct product and a coproduct complement C. The output is a direct product projection \pi_2: C \to T such that UniversalMorphismIntoDirectProduct( pi, \pi_2 ): T \to S \times C is an isomorphism.

generated by GAPDoc2HTML