Goto Chapter: Top 1 2 3 Ind

### 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
 ‣ ExactCoverWithGlobalElements( a ) ( attribute )

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
 ‣ IndexOfNonliftableMorphismFromDistinguishedObject( iota ) ( attribute )

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
 ‣ NonliftableMorphismFromDistinguishedObject( iota ) ( attribute )

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
 ‣ IsElementaryTopos( C ) ( property )

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
 ‣ SubobjectClassifier( C ) ( attribute )

Returns: an object

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

##### 1.2-3 CartesianSquareOfSubobjectClassifier
 ‣ CartesianSquareOfSubobjectClassifier( C ) ( attribute )

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
 ‣ ClassifyingMorphismOfSubobject( m ) ( attribute )

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
 ‣ ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier( m, omega ) ( operation )

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
 ‣ SubobjectOfClassifyingMorphism( chi ) ( attribute )

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
 ‣ ListOfSubobjects( A ) ( attribute )

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
 ‣ TruthMorphismOfTrue( C ) ( attribute )

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
 ‣ TruthMorphismOfTrueWithGivenObjects( T, Omega ) ( operation )

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
 ‣ TruthMorphismOfFalse( C ) ( attribute )

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
 ‣ TruthMorphismOfFalseWithGivenObjects( T, Omega ) ( operation )

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
 ‣ TruthMorphismOfNot( C ) ( attribute )

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
 ‣ TruthMorphismOfNotWithGivenObjects( Omega, Omega ) ( operation )

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
 ‣ TruthMorphismOfAnd( C ) ( attribute )

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
 ‣ TruthMorphismOfAndWithGivenObjects( Omega2, Omega ) ( operation )

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
 ‣ TruthMorphismOfOr( C ) ( attribute )

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
 ‣ TruthMorphismOfOrWithGivenObjects( Omega2, Omega ) ( operation )

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
 ‣ TruthMorphismOfImplies( C ) ( attribute )

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
 ‣ TruthMorphismOfImpliesWithGivenObjects( Omega2, Omega ) ( operation )

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
 ‣ PowerObject( a ) ( attribute )

Returns: an object

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

##### 1.4-2 PowerObjectFunctorial
 ‣ PowerObjectFunctorial( f ) ( attribute )

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
 ‣ PowerObjectFunctorialWithGivenPowerObjects( Pb, f, Pa ) ( operation )

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
 ‣ PowerObjectRightEvaluationMorphism( a ) ( attribute )

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
 ‣ PowerObjectRightEvaluationMorphismWithGivenObjects( axPa, a, Omega ) ( operation )

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
 ‣ PowerObjectLeftEvaluationMorphism( a ) ( attribute )

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
 ‣ PowerObjectLeftEvaluationMorphismWithGivenObjects( Pa_xa, a, Omega ) ( operation )

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
 ‣ PRightTransposeMorphism( a, b, f ) ( operation )

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
 ‣ PRightTransposeMorphismWithGivenRange( a, b, f, Pa ) ( operation )

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
 ‣ PLeftTransposeMorphism( a, b, f ) ( operation )

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
 ‣ PLeftTransposeMorphismWithGivenRange( a, b, f, Pb ) ( operation )

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
 ‣ UpperSegmentOfRelation( a, b, mu ) ( operation )

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
 ‣ UpperSegmentOfRelationWithGivenRange( a, b, mu, Pb ) ( operation )

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
 ‣ LowerSegmentOfRelation( a, b, mu ) ( operation )

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
 ‣ LowerSegmentOfRelationWithGivenRange( a, b, mu, Pa ) ( operation )

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
 ‣ SingletonMorphism( a ) ( attribute )

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
 ‣ SingletonMorphismWithGivenPowerObject( a, Pa ) ( operation )

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
 ‣ IsomorphismOntoCartesianSquareOfPowerObject( a ) ( attribute )

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
 ‣ IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects( Exp_a_Omega2, a, PaxPa ) ( operation )

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
 ‣ IntersectWithPreimagesWithGivenObjects( PAxB, f, PA ) ( operation )

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
 ‣ EmbeddingOfRelativePowerObject( f ) ( attribute )

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
 ‣ RelativePowerObjectFibrationMorphism( f ) ( attribute )

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
 ‣ RelativePowerObjectLeftEvaluationMorphism( f ) ( attribute )

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
 ‣ RightFiberMorphism( b, c ) ( operation )

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|
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
 ‣ RightFiberMorphismWithGivenObjects( cxPbxc, b, c, Pb ) ( operation )

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
 ‣ LeftFiberMorphism( b, c ) ( operation )

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|
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
 ‣ LeftFiberMorphismWithGivenObjects( Pbxc_xb, b, c, Pc ) ( operation )

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
 ‣ SingletonSupportOfRelationsWithGivenObjects( Pbxc, b, c, Pb ) ( operation )

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
 ‣ RelativeTruthMorphismOfTrue( a ) ( attribute )

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
 ‣ RelativeTruthMorphismOfTrueWithGivenObjects( T, a, Pa ) ( operation )

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
 ‣ RelativeTruthMorphismOfFalse( a ) ( attribute )

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
 ‣ RelativeTruthMorphismOfFalseWithGivenObjects( T, a, Pa ) ( operation )

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
 ‣ RelativeTruthMorphismOfNot( a ) ( attribute )

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
 ‣ RelativeTruthMorphismOfNotWithGivenObjects( Pa, a, Pa ) ( operation )

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
 ‣ RelativeTruthMorphismOfAnd( a ) ( attribute )

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
 ‣ RelativeTruthMorphismOfAndWithGivenObjects( PaxPa, a, Pa ) ( operation )

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
 ‣ RelativeTruthMorphismOfOr( a ) ( attribute )

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
 ‣ RelativeTruthMorphismOfOrWithGivenObjects( PaxPa, a, Pa ) ( operation )

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
 ‣ RelativeTruthMorphismOfImplies( a ) ( attribute )

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
 ‣ RelativeTruthMorphismOfImpliesWithGivenObjects( PaxPa, a, Pa ) ( operation )

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
 ‣ PseudoComplementSubobject( iota ) ( operation )

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
 ‣ EmbeddingOfPseudoComplementSubobject( iota ) ( operation )

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
 ‣ EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement( iota ) ( operation )

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
 ‣ IntersectionSubobject( iota1, iota2 ) ( operation )

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
 ‣ EmbeddingOfIntersectionSubobject( iota1, iota2 ) ( operation )

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
 ‣ EmbeddingOfIntersectionSubobjectWithGivenIntersection( iota1, iota2, T ) ( operation )

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
 ‣ UnionSubobject( iota1, iota2 ) ( operation )

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
 ‣ EmbeddingOfUnionSubobject( iota1, iota2 ) ( operation )

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
 ‣ EmbeddingOfUnionSubobjectWithGivenUnion( iota1, iota2, U ) ( operation )

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
 ‣ RelativePseudoComplementSubobject( iota1, iota2 ) ( operation )

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
 ‣ EmbeddingOfRelativePseudoComplementSubobject( iota1, iota2 ) ( operation )

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
 ‣ EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication( iota1, iota2, I ) ( operation )

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
 ‣ HasPushoutComplement( l, m ) ( operation )

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
 ‣ PushoutComplement( l, m ) ( operation )

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
 ‣ DPO( m, l, r ) ( operation )

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
 ‣ LawvereTierneyLocalModalityOperators( T ) ( attribute )

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
 ‣ LawvereTierneySubobjects( T ) ( attribute )

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
 ‣ LawvereTierneyEmbeddingsOfSubobjectClassifiers( T ) ( attribute )

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.

 ‣ AddCartesianSquareOfSubobjectClassifier( C, F ) ( operation )

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}().

 ‣ AddClassifyingMorphismOfSubobject( C, F ) ( operation )

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).

 ‣ AddClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier( C, F ) ( operation )

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).

 ‣ AddCoproductComplement( C, F ) ( operation )

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).

 ‣ AddDirectProductComplement( C, F ) ( operation )

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).

 ‣ AddEmbeddingOfIntersectionSubobject( C, F ) ( operation )

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).

 ‣ AddEmbeddingOfIntersectionSubobjectWithGivenIntersection( C, F ) ( operation )

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).

 ‣ AddEmbeddingOfPseudoComplementSubobject( C, F ) ( operation )

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).

 ‣ AddEmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement( C, F ) ( operation )

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).

 ‣ AddEmbeddingOfRelativePseudoComplementSubobject( C, F ) ( operation )

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).

 ‣ AddEmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication( C, F ) ( operation )

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).

 ‣ AddEmbeddingOfUnionSubobject( C, F ) ( operation )

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).

 ‣ AddEmbeddingOfUnionSubobjectWithGivenUnion( C, F ) ( operation )

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).

 ‣ AddExactCoverWithGlobalElements( C, F ) ( operation )

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).

 ‣ AddHasPushoutComplement( C, F ) ( operation )

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).

 ‣ AddIndexOfNonliftableMorphismFromDistinguishedObject( C, F ) ( operation )

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).

 ‣ AddInjectionOfCoproductComplement( C, F ) ( operation )

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).

 ‣ AddInjectionOfCoproductComplementWithGivenCoproductComplement( C, F ) ( operation )

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).

 ‣ AddIntersectionSubobject( C, F ) ( operation )

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).

 ‣ AddIsomorphismOntoCartesianSquareOfPowerObject( C, F ) ( operation )

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).

 ‣ AddIsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddLawvereTierneyEmbeddingsOfSubobjectClassifiers( C, F ) ( operation )

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}().

 ‣ AddLawvereTierneyLocalModalityOperators( C, F ) ( operation )

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}().

 ‣ AddLawvereTierneySubobjects( C, F ) ( operation )

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}().

 ‣ AddLeftFiberMorphism( C, F ) ( operation )

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).

 ‣ AddLeftFiberMorphismWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddListOfSubobjects( C, F ) ( operation )

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).

 ‣ AddLowerSegmentOfRelation( C, F ) ( operation )

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).

 ‣ AddLowerSegmentOfRelationWithGivenRange( C, F ) ( operation )

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).

 ‣ AddNonliftableMorphismFromDistinguishedObject( C, F ) ( operation )

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).

 ‣ AddPLeftTransposeMorphism( C, F ) ( operation )

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).

 ‣ AddPLeftTransposeMorphismWithGivenRange( C, F ) ( operation )

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).

 ‣ AddPRightTransposeMorphism( C, F ) ( operation )

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).

 ‣ AddPRightTransposeMorphismWithGivenRange( C, F ) ( operation )

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).

 ‣ AddPowerObject( C, F ) ( operation )

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).

 ‣ AddPowerObjectFunctorial( C, F ) ( operation )

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).

 ‣ AddPowerObjectFunctorialWithGivenPowerObjects( C, F ) ( operation )

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).

 ‣ AddPowerObjectLeftEvaluationMorphism( C, F ) ( operation )

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).

 ‣ AddPowerObjectLeftEvaluationMorphismWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddPowerObjectRightEvaluationMorphism( C, F ) ( operation )

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).

 ‣ AddPowerObjectRightEvaluationMorphismWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddProjectionInDirectProductComplement( C, F ) ( operation )

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).

 ‣ AddProjectionInDirectProductComplementWithGivenDirectProductComplement( C, F ) ( operation )

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).

 ‣ AddPseudoComplementSubobject( C, F ) ( operation )

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).

 ‣ AddPushoutComplement( C, F ) ( operation )

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).

 ‣ AddRelativePseudoComplementSubobject( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfAnd( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfAndWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfFalse( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfFalseWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfImplies( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfImpliesWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfNot( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfNotWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfOr( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfOrWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfTrue( C, F ) ( operation )

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).

 ‣ AddRelativeTruthMorphismOfTrueWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddRightFiberMorphism( C, F ) ( operation )

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).

 ‣ AddRightFiberMorphismWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddSingletonMorphism( C, F ) ( operation )

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).

 ‣ AddSingletonMorphismWithGivenPowerObject( C, F ) ( operation )

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).

 ‣ AddSubobjectClassifier( C, F ) ( operation )

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}().

 ‣ AddSubobjectOfClassifyingMorphism( C, F ) ( operation )

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).

 ‣ AddTruthMorphismOfAnd( C, F ) ( operation )

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}().

 ‣ AddTruthMorphismOfAndWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddTruthMorphismOfFalse( C, F ) ( operation )

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}().

 ‣ AddTruthMorphismOfFalseWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddTruthMorphismOfImplies( C, F ) ( operation )

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}().

 ‣ AddTruthMorphismOfImpliesWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddTruthMorphismOfNot( C, F ) ( operation )

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}().

 ‣ AddTruthMorphismOfNotWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddTruthMorphismOfOr( C, F ) ( operation )

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}().

 ‣ AddTruthMorphismOfOrWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddTruthMorphismOfTrue( C, F ) ( operation )

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}().

 ‣ AddTruthMorphismOfTrueWithGivenObjects( C, F ) ( operation )

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).

 ‣ AddUnionSubobject( C, F ) ( operation )

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).

 ‣ AddUpperSegmentOfRelation( C, F ) ( operation )

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).

 ‣ AddUpperSegmentOfRelationWithGivenRange( C, F ) ( operation )

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
 ‣ CoproductComplement( iota ) ( attribute )

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
 ‣ InjectionOfCoproductComplement( iota ) ( attribute )

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
 ‣ InjectionOfCoproductComplementWithGivenCoproductComplement( iota, C ) ( operation )

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
 ‣ DirectProductComplement( pi ) ( attribute )

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
 ‣ ProjectionInDirectProductComplement( pi ) ( attribute )

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
 ‣ ProjectionInDirectProductComplementWithGivenDirectProductComplement( pi, C ) ( operation )

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.

Goto Chapter: Top 1 2 3 Ind

generated by GAPDoc2HTML