Goto Chapter: Top 1 2 3 4 5 6 7 8 9 10 11 12 13 Ind

### 6 Universal Objects

#### 6.1 Kernel

For a given morphism $$\alpha: A \rightarrow B$$, a kernel of $$\alpha$$ consists of three parts:

• an object $$K$$,

• a morphism $$\iota: K \rightarrow A$$ such that $$\alpha \circ \iota \sim_{K,B} 0$$,

• a dependent function $$u$$ mapping each morphism $$\tau: T \rightarrow A$$ satisfying $$\alpha \circ \tau \sim_{T,B} 0$$ to a morphism $$u(\tau): T \rightarrow K$$ such that $$\iota \circ u( \tau ) \sim_{T,A} \tau$$.

The triple $$( K, \iota, u )$$ is called a kernel of $$\alpha$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$K$$ of such a triple by $$\mathrm{KernelObject}(\alpha)$$. We say that the morphism $$u(\tau)$$ is induced by the universal property of the kernel. $$\\$$ $$\mathrm{KernelObject}$$ is a functorial operation. This means: for $$\mu: A \rightarrow A'$$, $$\nu: B \rightarrow B'$$, $$\alpha: A \rightarrow B$$, $$\alpha': A' \rightarrow B'$$ such that $$\nu \circ \alpha \sim_{A,B'} \alpha' \circ \mu$$, we obtain a morphism $$\mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' )$$.

##### 6.1-1 KernelObject
 ‣ KernelObject( alpha ) ( attribute )

Returns: an object

The argument is a morphism $$\alpha$$. The output is the kernel $$K$$ of $$\alpha$$.

##### 6.1-2 KernelEmbedding
 ‣ KernelEmbedding( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{KernelObject}(\alpha),A)$$

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the kernel embedding $$\iota: \mathrm{KernelObject}(\alpha) \rightarrow A$$.

##### 6.1-3 KernelEmbeddingWithGivenKernelObject
 ‣ KernelEmbeddingWithGivenKernelObject( alpha, K ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(K,A)$$

The arguments are a morphism $$\alpha: A \rightarrow B$$ and an object $$K = \mathrm{KernelObject}(\alpha)$$. The output is the kernel embedding $$\iota: K \rightarrow A$$.

##### 6.1-4 KernelLift
 ‣ KernelLift( alpha, tau ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(T,\mathrm{KernelObject}(\alpha))$$

The arguments are a morphism $$\alpha: A \rightarrow B$$ and a test morphism $$\tau: T \rightarrow A$$ satisfying $$\alpha \circ \tau \sim_{T,B} 0$$. The output is the morphism $$u(\tau): T \rightarrow \mathrm{KernelObject}(\alpha)$$ given by the universal property of the kernel.

##### 6.1-5 KernelLiftWithGivenKernelObject
 ‣ KernelLiftWithGivenKernelObject( alpha, tau, K ) ( operation )

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

The arguments are a morphism $$\alpha: A \rightarrow B$$, a test morphism $$\tau: T \rightarrow A$$ satisfying $$\alpha \circ \tau \sim_{T,B} 0$$, and an object $$K = \mathrm{KernelObject}(\alpha)$$. The output is the morphism $$u(\tau): T \rightarrow K$$ given by the universal property of the kernel.

 ‣ AddKernelObject( C, F ) ( operation )

Returns: nothing

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

 ‣ AddKernelEmbedding( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation KernelEmbedding. $$F: \alpha \mapsto \iota$$.

 ‣ AddKernelEmbeddingWithGivenKernelObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation KernelEmbeddingWithGivenKernelObject. $$F: (\alpha, K) \mapsto \iota$$.

 ‣ AddKernelLift( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation KernelLift. $$F: (\alpha, \tau) \mapsto u(\tau)$$.

 ‣ AddKernelLiftWithGivenKernelObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation KernelLiftWithGivenKernelObject. $$F: (\alpha, \tau, K) \mapsto u$$.

##### 6.1-11 KernelObjectFunctorial
 ‣ KernelObjectFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{KernelObject}( \alpha ), \mathrm{KernelObject}( \alpha' ) )$$

The argument is a list $$L = [ \alpha: A \rightarrow B, [ \mu: A \rightarrow A', \nu: B \rightarrow B' ], \alpha': A' \rightarrow B' ]$$ of morphisms. The output is the morphism $$\mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' )$$ given by the functoriality of the kernel.

##### 6.1-12 KernelObjectFunctorial
 ‣ KernelObjectFunctorial( alpha, mu, alpha_prime ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{KernelObject}( \alpha ), \mathrm{KernelObject}( \alpha' ) )$$

The arguments are three morphisms $$\alpha: A \rightarrow B$$, $$\mu: A \rightarrow A'$$, $$\alpha': A' \rightarrow B'$$. The output is the morphism $$\mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' )$$ given by the functoriality of the kernel.

##### 6.1-13 KernelObjectFunctorialWithGivenKernelObjects
 ‣ KernelObjectFunctorialWithGivenKernelObjects( s, alpha, mu, alpha_prime, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( s, r )$$

The arguments are an object $$s = \mathrm{KernelObject}( \alpha )$$, three morphisms $$\alpha: A \rightarrow B$$, $$\mu: A \rightarrow A'$$, $$\alpha': A' \rightarrow B'$$, and an object $$r = \mathrm{KernelObject}( \alpha' )$$. The output is the morphism $$\mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' )$$ given by the functoriality of the kernel.

##### 6.1-14 KernelObjectFunctorialWithGivenKernelObjects
 ‣ KernelObjectFunctorialWithGivenKernelObjects( s, alpha, mu, nu, alpha_prime, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( s, r )$$

The arguments are an object $$s = \mathrm{KernelObject}( \alpha )$$, four morphisms $$\alpha: A \rightarrow B$$, $$\mu: A \rightarrow A'$$, $$\nu: B \rightarrow B'$$, $$\alpha': A' \rightarrow B'$$, and an object $$r = \mathrm{KernelObject}( \alpha' )$$. The output is the morphism $$\mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' )$$ given by the functoriality of the kernel.

 ‣ AddKernelObjectFunctorialWithGivenKernelObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation KernelObjectFunctorialWithGivenKernelObjects. $$F: (\mathrm{KernelObject}( \alpha ), \alpha, \mu, \alpha', \mathrm{KernelObject}( \alpha' )) \mapsto (\mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' ))$$.

#### 6.2 Cokernel

For a given morphism $$\alpha: A \rightarrow B$$, a cokernel of $$\alpha$$ consists of three parts:

• an object $$K$$,

• a morphism $$\epsilon: B \rightarrow K$$ such that $$\epsilon \circ \alpha \sim_{A,K} 0$$,

• a dependent function $$u$$ mapping each $$\tau: B \rightarrow T$$ satisfying $$\tau \circ \alpha \sim_{A, T} 0$$ to a morphism $$u(\tau):K \rightarrow T$$ such that $$u(\tau) \circ \epsilon \sim_{B,T} \tau$$.

The triple $$( K, \epsilon, u )$$ is called a cokernel of $$\alpha$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$K$$ of such a triple by $$\mathrm{CokernelObject}(\alpha)$$. We say that the morphism $$u(\tau)$$ is induced by the universal property of the cokernel. $$\\$$ $$\mathrm{CokernelObject}$$ is a functorial operation. This means: for $$\mu: A \rightarrow A'$$, $$\nu: B \rightarrow B'$$, $$\alpha: A \rightarrow B$$, $$\alpha': A' \rightarrow B'$$ such that $$\nu \circ \alpha \sim_{A,B'} \alpha' \circ \mu$$, we obtain a morphism $$\mathrm{CokernelObject}( \alpha ) \rightarrow \mathrm{CokernelObject}( \alpha' )$$.

##### 6.2-1 CokernelObject
 ‣ CokernelObject( alpha ) ( attribute )

Returns: an object

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the cokernel $$K$$ of $$\alpha$$.

##### 6.2-2 CokernelProjection
 ‣ CokernelProjection( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(B, \mathrm{CokernelObject}( \alpha ))$$

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the cokernel projection $$\epsilon: B \rightarrow \mathrm{CokernelObject}( \alpha )$$.

##### 6.2-3 CokernelProjectionWithGivenCokernelObject
 ‣ CokernelProjectionWithGivenCokernelObject( alpha, K ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(B, K)$$

The arguments are a morphism $$\alpha: A \rightarrow B$$ and an object $$K = \mathrm{CokernelObject}(\alpha)$$. The output is the cokernel projection $$\epsilon: B \rightarrow \mathrm{CokernelObject}( \alpha )$$.

##### 6.2-4 CokernelColift
 ‣ CokernelColift( alpha, tau ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{CokernelObject}(\alpha),T)$$

The arguments are a morphism $$\alpha: A \rightarrow B$$ and a test morphism $$\tau: B \rightarrow T$$ satisfying $$\tau \circ \alpha \sim_{A, T} 0$$. The output is the morphism $$u(\tau): \mathrm{CokernelObject}(\alpha) \rightarrow T$$ given by the universal property of the cokernel.

##### 6.2-5 CokernelColiftWithGivenCokernelObject
 ‣ CokernelColiftWithGivenCokernelObject( alpha, tau, K ) ( operation )

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

The arguments are a morphism $$\alpha: A \rightarrow B$$, a test morphism $$\tau: B \rightarrow T$$ satisfying $$\tau \circ \alpha \sim_{A, T} 0$$, and an object $$K = \mathrm{CokernelObject}(\alpha)$$. The output is the morphism $$u(\tau): K \rightarrow T$$ given by the universal property of the cokernel.

 ‣ AddCokernelObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CokernelObject. $$F: \alpha \mapsto K$$.

 ‣ AddCokernelProjection( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CokernelProjection. $$F: \alpha \mapsto \epsilon$$.

 ‣ AddCokernelProjectionWithGivenCokernelObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CokernelProjection. $$F: (\alpha, K) \mapsto \epsilon$$.

 ‣ AddCokernelColift( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CokernelProjection. $$F: (\alpha, \tau) \mapsto u(\tau)$$.

 ‣ AddCokernelColiftWithGivenCokernelObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CokernelProjection. $$F: (\alpha, \tau, K) \mapsto u(\tau)$$.

##### 6.2-11 CokernelObjectFunctorial
 ‣ CokernelObjectFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{CokernelObject}( \alpha ), \mathrm{CokernelObject}( \alpha' ))$$

The argument is a list $$L = [ \alpha: A \rightarrow B, [ \mu:A \rightarrow A', \nu: B \rightarrow B' ], \alpha': A' \rightarrow B' ]$$. The output is the morphism $$\mathrm{CokernelObject}( \alpha ) \rightarrow \mathrm{CokernelObject}( \alpha' )$$ given by the functoriality of the cokernel.

##### 6.2-12 CokernelObjectFunctorial
 ‣ CokernelObjectFunctorial( alpha, nu, alpha_prime ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{CokernelObject}( \alpha ), \mathrm{CokernelObject}( \alpha' ))$$

The arguments are three morphisms $$\alpha: A \rightarrow B, \nu: B \rightarrow B', \alpha': A' \rightarrow B'$$. The output is the morphism $$\mathrm{CokernelObject}( \alpha ) \rightarrow \mathrm{CokernelObject}( \alpha' )$$ given by the functoriality of the cokernel.

##### 6.2-13 CokernelObjectFunctorialWithGivenCokernelObjects
 ‣ CokernelObjectFunctorialWithGivenCokernelObjects( s, alpha, nu, alpha_prime, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(s, r)$$

The arguments are an object $$s = \mathrm{CokernelObject}( \alpha )$$, three morphisms $$\alpha: A \rightarrow B, \nu: B \rightarrow B', \alpha': A' \rightarrow B'$$, and an object $$r = \mathrm{CokernelObject}( \alpha' )$$. The output is the morphism $$\mathrm{CokernelObject}( \alpha ) \rightarrow \mathrm{CokernelObject}( \alpha' )$$ given by the functoriality of the cokernel.

##### 6.2-14 CokernelObjectFunctorialWithGivenCokernelObjects
 ‣ CokernelObjectFunctorialWithGivenCokernelObjects( s, alpha, mu, nu, alpha_prime, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(s, r)$$

The arguments are an object $$s = \mathrm{CokernelObject}( \alpha )$$, four morphisms $$\alpha: A \rightarrow B, \mu: A \rightarrow A', \nu: B \rightarrow B', \alpha': A' \rightarrow B'$$, and an object $$r = \mathrm{CokernelObject}( \alpha' )$$. The output is the morphism $$\mathrm{CokernelObject}( \alpha ) \rightarrow \mathrm{CokernelObject}( \alpha' )$$ given by the functoriality of the cokernel.

 ‣ AddCokernelObjectFunctorialWithGivenCokernelObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CokernelObjectFunctorialWithGivenCokernelObjects. $$F: (\mathrm{CokernelObject}( \alpha ), \alpha, \nu, \alpha', \mathrm{CokernelObject}( \alpha' )) \mapsto (\mathrm{CokernelObject}( \alpha ) \rightarrow \mathrm{CokernelObject}( \alpha' ))$$.

#### 6.3 Zero Object

A zero object consists of three parts:

• an object $$Z$$,

• a function $$u_{\mathrm{in}}$$ mapping each object $$A$$ to a morphism $$u_{\mathrm{in}}(A): A \rightarrow Z$$,

• a function $$u_{\mathrm{out}}$$ mapping each object $$A$$ to a morphism $$u_{\mathrm{out}}(A): Z \rightarrow A$$.

The triple $$(Z, u_{\mathrm{in}}, u_{\mathrm{out}})$$ is called a zero object if the morphisms $$u_{\mathrm{in}}(A)$$, $$u_{\mathrm{out}}(A)$$ are uniquely determined up to congruence of morphisms. We denote the object $$Z$$ of such a triple by $$\mathrm{ZeroObject}$$. We say that the morphisms $$u_{\mathrm{in}}(A)$$ and $$u_{\mathrm{out}}(A)$$ are induced by the universal property of the zero object.

##### 6.3-1 ZeroObject
 ‣ ZeroObject( C ) ( attribute )

Returns: an object

The argument is a category $$C$$. The output is a zero object $$Z$$ of $$C$$.

##### 6.3-2 ZeroObject
 ‣ ZeroObject( c ) ( attribute )

Returns: an object

This is a convenience method. The argument is a cell $$c$$. The output is a zero object $$Z$$ of the category $$C$$ for which $$c \in C$$.

##### 6.3-3 MorphismFromZeroObject
 ‣ MorphismFromZeroObject( A ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{ZeroObject}, A)$$

This is a convenience method. The argument is an object $$A$$. It calls $$\mathrm{UniversalMorphismFromZeroObject}$$ on $$A$$.

##### 6.3-4 MorphismIntoZeroObject
 ‣ MorphismIntoZeroObject( A ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(A, \mathrm{ZeroObject})$$

This is a convenience method. The argument is an object $$A$$. It calls $$\mathrm{UniversalMorphismIntoZeroObject}$$ on $$A$$.

##### 6.3-5 UniversalMorphismFromZeroObject
 ‣ UniversalMorphismFromZeroObject( A ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{ZeroObject}, A)$$

The argument is an object $$A$$. The output is the universal morphism $$u_{\mathrm{out}}: \mathrm{ZeroObject} \rightarrow A$$.

##### 6.3-6 UniversalMorphismFromZeroObjectWithGivenZeroObject
 ‣ UniversalMorphismFromZeroObjectWithGivenZeroObject( A, Z ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(Z, A)$$

The arguments are an object $$A$$, and a zero object $$Z = \mathrm{ZeroObject}$$. The output is the universal morphism $$u_{\mathrm{out}}: Z \rightarrow A$$.

##### 6.3-7 UniversalMorphismIntoZeroObject
 ‣ UniversalMorphismIntoZeroObject( A ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(A, \mathrm{ZeroObject})$$

The argument is an object $$A$$. The output is the universal morphism $$u_{\mathrm{in}}: A \rightarrow \mathrm{ZeroObject}$$.

##### 6.3-8 UniversalMorphismIntoZeroObjectWithGivenZeroObject
 ‣ UniversalMorphismIntoZeroObjectWithGivenZeroObject( A, Z ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(A, Z)$$

The arguments are an object $$A$$, and a zero object $$Z = \mathrm{ZeroObject}$$. The output is the universal morphism $$u_{\mathrm{in}}: A \rightarrow Z$$.

##### 6.3-9 IsomorphismFromZeroObjectToInitialObject
 ‣ IsomorphismFromZeroObjectToInitialObject( C ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{ZeroObject}, \mathrm{InitialObject})$$

The argument is a category $$C$$. The output is the unique isomorphism $$\mathrm{ZeroObject} \rightarrow \mathrm{InitialObject}$$.

##### 6.3-10 IsomorphismFromInitialObjectToZeroObject
 ‣ IsomorphismFromInitialObjectToZeroObject( C ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{InitialObject}, \mathrm{ZeroObject})$$

The argument is a category $$C$$. The output is the unique isomorphism $$\mathrm{InitialObject} \rightarrow \mathrm{ZeroObject}$$.

##### 6.3-11 IsomorphismFromZeroObjectToTerminalObject
 ‣ IsomorphismFromZeroObjectToTerminalObject( C ) ( attribute )

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

The argument is a category $$C$$. The output is the unique isomorphism $$\mathrm{ZeroObject} \rightarrow \mathrm{TerminalObject}$$.

##### 6.3-12 IsomorphismFromTerminalObjectToZeroObject
 ‣ IsomorphismFromTerminalObjectToZeroObject( C ) ( attribute )

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

The argument is a category $$C$$. The output is the unique isomorphism $$\mathrm{TerminalObject} \rightarrow \mathrm{ZeroObject}$$.

 ‣ AddZeroObject( C, F ) ( operation )

Returns: nothing

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

 ‣ AddUniversalMorphismIntoZeroObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoZeroObject. $$F: A \mapsto u_{\mathrm{in}}(A)$$.

 ‣ AddUniversalMorphismIntoZeroObjectWithGivenZeroObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoZeroObjectWithGivenZeroObject. $$F: (A, Z) \mapsto u_{\mathrm{in}}(A)$$.

 ‣ AddUniversalMorphismFromZeroObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromZeroObject. $$F: A \mapsto u_{\mathrm{out}}(A)$$.

 ‣ AddUniversalMorphismFromZeroObjectWithGivenZeroObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromZeroObjectWithGivenZeroObject. $$F: (A,Z) \mapsto u_{\mathrm{out}}(A)$$.

 ‣ AddIsomorphismFromZeroObjectToInitialObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromZeroObjectToInitialObject. $$F: () \mapsto (\mathrm{ZeroObject} \rightarrow \mathrm{InitialObject})$$.

 ‣ AddIsomorphismFromInitialObjectToZeroObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromInitialObjectToZeroObject. $$F: () \mapsto ( \mathrm{InitialObject} \rightarrow \mathrm{ZeroObject})$$.

 ‣ AddIsomorphismFromZeroObjectToTerminalObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromZeroObjectToTerminalObject. $$F: () \mapsto (\mathrm{ZeroObject} \rightarrow \mathrm{TerminalObject})$$.

 ‣ AddIsomorphismFromTerminalObjectToZeroObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromTerminalObjectToZeroObject. $$F: () \mapsto ( \mathrm{TerminalObject} \rightarrow \mathrm{ZeroObject})$$.

##### 6.3-22 ZeroObjectFunctorial
 ‣ ZeroObjectFunctorial( C ) ( attribute )

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

The argument is a category $$C$$. The output is the unique morphism $$\mathrm{ZeroObject} \rightarrow \mathrm{ZeroObject}$$.

 ‣ AddZeroObjectFunctorial( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ZeroObjectFunctorial. $$F: () \mapsto (T \rightarrow T)$$.

#### 6.4 Terminal Object

A terminal object consists of two parts:

• an object $$T$$,

• a function $$u$$ mapping each object $$A$$ to a morphism $$u( A ): A \rightarrow T$$.

The pair $$( T, u )$$ is called a terminal object if the morphisms $$u( A )$$ are uniquely determined up to congruence of morphisms. We denote the object $$T$$ of such a pair by $$\mathrm{TerminalObject}$$. We say that the morphism $$u( A )$$ is induced by the universal property of the terminal object. $$\\$$ $$\mathrm{TerminalObject}$$ is a functorial operation. This just means: There exists a unique morphism $$T \rightarrow T$$.

##### 6.4-1 TerminalObject
 ‣ TerminalObject( C ) ( attribute )

Returns: an object

The argument is a category $$C$$. The output is a terminal object $$T$$ of $$C$$.

##### 6.4-2 TerminalObject
 ‣ TerminalObject( c ) ( attribute )

Returns: an object

This is a convenience method. The argument is a cell $$c$$. The output is a terminal object $$T$$ of the category $$C$$ for which $$c \in C$$.

##### 6.4-3 UniversalMorphismIntoTerminalObject
 ‣ UniversalMorphismIntoTerminalObject( A ) ( attribute )

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

The argument is an object $$A$$. The output is the universal morphism $$u(A): A \rightarrow \mathrm{TerminalObject}$$.

##### 6.4-4 UniversalMorphismIntoTerminalObjectWithGivenTerminalObject
 ‣ UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( A, T ) ( operation )

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

The argument are an object $$A$$, and an object $$T = \mathrm{TerminalObject}$$. The output is the universal morphism $$u(A): A \rightarrow T$$.

 ‣ AddTerminalObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TerminalObject. $$F: () \mapsto T$$.

 ‣ AddUniversalMorphismIntoTerminalObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoTerminalObject. $$F: A \mapsto u(A)$$.

 ‣ AddUniversalMorphismIntoTerminalObjectWithGivenTerminalObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoTerminalObjectWithGivenTerminalObject. $$F: (A,T) \mapsto u(A)$$.

##### 6.4-8 TerminalObjectFunctorial
 ‣ TerminalObjectFunctorial( C ) ( attribute )

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

The argument is a category $$C$$. The output is the unique morphism $$\mathrm{TerminalObject} \rightarrow \mathrm{TerminalObject}$$.

 ‣ AddTerminalObjectFunctorial( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TerminalObjectFunctorial. $$F: () \mapsto (T \rightarrow T)$$.

#### 6.5 Initial Object

An initial object consists of two parts:

• an object $$I$$,

• a function $$u$$ mapping each object $$A$$ to a morphism $$u( A ): I \rightarrow A$$.

The pair $$(I,u)$$ is called a initial object if the morphisms $$u(A)$$ are uniquely determined up to congruence of morphisms. We denote the object $$I$$ of such a triple by $$\mathrm{InitialObject}$$. We say that the morphism $$u( A )$$ is induced by the universal property of the initial object. $$\\$$ $$\mathrm{InitialObject}$$ is a functorial operation. This just means: There exists a unique morphisms $$I \rightarrow I$$.

##### 6.5-1 InitialObject
 ‣ InitialObject( C ) ( attribute )

Returns: an object

The argument is a category $$C$$. The output is an initial object $$I$$ of $$C$$.

##### 6.5-2 InitialObject
 ‣ InitialObject( c ) ( attribute )

Returns: an object

This is a convenience method. The argument is a cell $$c$$. The output is an initial object $$I$$ of the category $$C$$ for which $$c \in C$$.

##### 6.5-3 UniversalMorphismFromInitialObject
 ‣ UniversalMorphismFromInitialObject( A ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{InitialObject} \rightarrow A)$$.

The argument is an object $$A$$. The output is the universal morphism $$u(A): \mathrm{InitialObject} \rightarrow A$$.

##### 6.5-4 UniversalMorphismFromInitialObjectWithGivenInitialObject
 ‣ UniversalMorphismFromInitialObjectWithGivenInitialObject( A, I ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{InitialObject} \rightarrow A)$$.

The arguments are an object $$A$$, and an object $$I = \mathrm{InitialObject}$$. The output is the universal morphism $$u(A): \mathrm{InitialObject} \rightarrow A$$.

 ‣ AddInitialObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InitialObject. $$F: () \mapsto I$$.

 ‣ AddUniversalMorphismFromInitialObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromInitialObject. $$F: A \mapsto u(A)$$.

 ‣ AddUniversalMorphismFromInitialObjectWithGivenInitialObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromInitialObjectWithGivenInitialObject. $$F: (A,I) \mapsto u(A)$$.

##### 6.5-8 InitialObjectFunctorial
 ‣ InitialObjectFunctorial( C ) ( attribute )

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

The argument is a category $$C$$. The output is the unique morphism $$\mathrm{InitialObject} \rightarrow \mathrm{InitialObject}$$.

 ‣ AddInitialObjectFunctorial( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InitialObjectFunctorial. $$F: () \rightarrow ( I \rightarrow I )$$.

#### 6.6 Direct Sum

For a given list $$D = (S_1, \dots, S_n)$$ in an Ab-category, a direct sum consists of five parts:

• an object $$S$$,

• a list of morphisms $$\pi = (\pi_i: S \rightarrow S_i)_{i = 1 \dots n}$$,

• a list of morphisms $$\iota = (\iota_i: S_i \rightarrow S)_{i = 1 \dots n}$$,

• a dependent function $$u_{\mathrm{in}}$$ mapping every list $$\tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}$$ to a morphism $$u_{\mathrm{in}}(\tau): T \rightarrow S$$ such that $$\pi_i \circ u_{\mathrm{in}}(\tau) \sim_{T,S_i} \tau_i$$ for all $$i = 1, \dots, n$$.

• a dependent function $$u_{\mathrm{out}}$$ mapping every list $$\tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}$$ to a morphism $$u_{\mathrm{out}}(\tau): S \rightarrow T$$ such that $$u_{\mathrm{out}}(\tau) \circ \iota_i \sim_{S_i, T} \tau_i$$ for all $$i = 1, \dots, n$$,

such that

• $$\sum_{i=1}^{n} \iota_i \circ \pi_i \sim_{S,S} \mathrm{id}_S$$,

• $$\pi_j \circ \iota_i \sim_{S_i, S_j} \delta_{i,j}$$,

where $$\delta_{i,j} \in \mathrm{Hom}( S_i, S_j )$$ is the identity if $$i=j$$, and $$0$$ otherwise. The $$5$$-tuple $$(S, \pi, \iota, u_{\mathrm{in}}, u_{\mathrm{out}})$$ is called a direct sum of $$D$$. We denote the object $$S$$ of such a $$5$$-tuple by $$\bigoplus_{i=1}^n S_i$$. We say that the morphisms $$u_{\mathrm{in}}(\tau), u_{\mathrm{out}}(\tau)$$ are induced by the universal property of the direct sum. $$\\$$ $$\mathrm{DirectSum}$$ is a functorial operation. This means: For $$(\mu_i: S_i \rightarrow S'_i)_{i=1\dots n}$$, we obtain a morphism $$\bigoplus_{i=1}^n S_i \rightarrow \bigoplus_{i=1}^n S_i'$$.

##### 6.6-1 DirectSumOp
 ‣ DirectSumOp( D, method_selection_object ) ( operation )

Returns: an object

The argument is a list of objects $$D = (S_1, \dots, S_n)$$ and an object for method selection. The output is the direct sum $$\bigoplus_{i=1}^n S_i$$.

##### 6.6-2 ProjectionInFactorOfDirectSum
 ‣ ProjectionInFactorOfDirectSum( D, k ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n S_i, S_k )$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$ and an integer $$k$$. The output is the $$k$$-th projection $$\pi_k: \bigoplus_{i=1}^n S_i \rightarrow S_k$$.

##### 6.6-3 ProjectionInFactorOfDirectSumOp
 ‣ ProjectionInFactorOfDirectSumOp( D, k, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n S_i, S_k )$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$, an integer $$k$$, and an object for method selection. The output is the $$k$$-th projection $$\pi_k: \bigoplus_{i=1}^n S_i \rightarrow S_k$$.

##### 6.6-4 ProjectionInFactorOfDirectSumWithGivenDirectSum
 ‣ ProjectionInFactorOfDirectSumWithGivenDirectSum( D, k, S ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( S, S_k )$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$, an integer $$k$$, and an object $$S = \bigoplus_{i=1}^n S_i$$. The output is the $$k$$-th projection $$\pi_k: S \rightarrow S_k$$.

##### 6.6-5 InjectionOfCofactorOfDirectSum
 ‣ InjectionOfCofactorOfDirectSum( D, k ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( S_k, \bigoplus_{i=1}^n S_i )$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$ and an integer $$k$$. The output is the $$k$$-th injection $$\iota_k: S_k \rightarrow \bigoplus_{i=1}^n S_i$$.

##### 6.6-6 InjectionOfCofactorOfDirectSumOp
 ‣ InjectionOfCofactorOfDirectSumOp( D, k, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( S_k, \bigoplus_{i=1}^n S_i )$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$, an integer $$k$$, and an object for method selection. The output is the $$k$$-th injection $$\iota_k: S_k \rightarrow \bigoplus_{i=1}^n S_i$$.

##### 6.6-7 InjectionOfCofactorOfDirectSumWithGivenDirectSum
 ‣ InjectionOfCofactorOfDirectSumWithGivenDirectSum( D, k, S ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( S_k, S )$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$, an integer $$k$$, and an object $$S = \bigoplus_{i=1}^n S_i$$. The output is the $$k$$-th injection $$\iota_k: S_k \rightarrow S$$.

##### 6.6-8 UniversalMorphismIntoDirectSum
 ‣ UniversalMorphismIntoDirectSum( arg ) ( function )

Returns: a morphism in $$\mathrm{Hom}(T, \bigoplus_{i=1}^n S_i)$$

This is a convenience method. There are three different ways to use this method:

• The arguments are a list of objects $$D = (S_1, \dots, S_n)$$ and a list of morphisms $$\tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}$$.

• The argument is a list of morphisms $$\tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}$$.

• The arguments are morphisms $$\tau_1: T \rightarrow S_1, \dots, \tau_n: T \rightarrow S_n$$.

The output is the morphism $$u_{\mathrm{in}}(\tau): T \rightarrow \bigoplus_{i=1}^n S_i$$ given by the universal property of the direct sum.

##### 6.6-9 UniversalMorphismIntoDirectSumOp
 ‣ UniversalMorphismIntoDirectSumOp( D, tau, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(T, \bigoplus_{i=1}^n S_i)$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$, a list of morphisms $$\tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}$$, and an object for method selection. The output is the morphism $$u_{\mathrm{in}}(\tau): T \rightarrow \bigoplus_{i=1}^n S_i$$ given by the universal property of the direct sum.

##### 6.6-10 UniversalMorphismIntoDirectSumWithGivenDirectSum
 ‣ UniversalMorphismIntoDirectSumWithGivenDirectSum( D, tau, S ) ( operation )

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

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$, a list of morphisms $$\tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}$$, and an object $$S = \bigoplus_{i=1}^n S_i$$. The output is the morphism $$u_{\mathrm{in}}(\tau): T \rightarrow S$$ given by the universal property of the direct sum.

##### 6.6-11 UniversalMorphismFromDirectSum
 ‣ UniversalMorphismFromDirectSum( arg ) ( function )

Returns: a morphism in $$\mathrm{Hom}(\bigoplus_{i=1}^n S_i, T)$$

This is a convenience method. There are three different ways to use this method:

• The arguments are a list of objects $$D = (S_1, \dots, S_n)$$ and a list of morphisms $$\tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}$$.

• The argument is a list of morphisms $$\tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}$$.

• The arguments are morphisms $$S_1 \rightarrow T, \dots, S_n \rightarrow T$$.

The output is the morphism $$u_{\mathrm{out}}(\tau): \bigoplus_{i=1}^n S_i \rightarrow T$$ given by the universal property of the direct sum.

##### 6.6-12 UniversalMorphismFromDirectSumOp
 ‣ UniversalMorphismFromDirectSumOp( D, tau, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\bigoplus_{i=1}^n S_i, T)$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$, a list of morphisms $$\tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}$$, and an object for method selection. The output is the morphism $$u_{\mathrm{out}}(\tau): \bigoplus_{i=1}^n S_i \rightarrow T$$ given by the universal property of the direct sum.

##### 6.6-13 UniversalMorphismFromDirectSumWithGivenDirectSum
 ‣ UniversalMorphismFromDirectSumWithGivenDirectSum( D, tau, S ) ( operation )

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

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$, a list of morphisms $$\tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}$$, and an object $$S = \bigoplus_{i=1}^n S_i$$. The output is the morphism $$u_{\mathrm{out}}(\tau): S \rightarrow T$$ given by the universal property of the direct sum.

##### 6.6-14 IsomorphismFromDirectSumToDirectProduct
 ‣ IsomorphismFromDirectSumToDirectProduct( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n S_i, \prod_{i=1}^{n}S_i )$$

The argument is a list of objects $$D = (S_1, \dots, S_n)$$. The output is the canonical isomorphism $$\bigoplus_{i=1}^n S_i \rightarrow \prod_{i=1}^{n}S_i$$.

##### 6.6-15 IsomorphismFromDirectSumToDirectProductOp
 ‣ IsomorphismFromDirectSumToDirectProductOp( D, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n S_i, \prod_{i=1}^{n}S_i )$$

The arguments are a list of objects $$D = (S_1, \dots, S_n)$$ and an object for method selection. The output is the canonical isomorphism $$\bigoplus_{i=1}^n S_i \rightarrow \prod_{i=1}^{n}S_i$$.

##### 6.6-16 IsomorphismFromDirectProductToDirectSum
 ‣ IsomorphismFromDirectProductToDirectSum( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \prod_{i=1}^{n}S_i, \bigoplus_{i=1}^n S_i )$$

The argument is a list of objects $$D = (S_1, \dots, S_n)$$. The output is the canonical isomorphism $$\prod_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i$$.

##### 6.6-17 IsomorphismFromDirectProductToDirectSumOp
 ‣ IsomorphismFromDirectProductToDirectSumOp( D, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \prod_{i=1}^{n}S_i, \bigoplus_{i=1}^n S_i )$$

The argument is a list of objects $$D = (S_1, \dots, S_n)$$ and an object for method selection. The output is the canonical isomorphism $$\prod_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i$$.

##### 6.6-18 IsomorphismFromDirectSumToCoproduct
 ‣ IsomorphismFromDirectSumToCoproduct( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n S_i, \bigsqcup_{i=1}^{n}S_i )$$

The argument is a list of objects $$D = (S_1, \dots, S_n)$$. The output is the canonical isomorphism $$\bigoplus_{i=1}^n S_i \rightarrow \bigsqcup_{i=1}^{n}S_i$$.

##### 6.6-19 IsomorphismFromDirectSumToCoproductOp
 ‣ IsomorphismFromDirectSumToCoproductOp( D, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n S_i, \bigsqcup_{i=1}^{n}S_i )$$

The argument is a list of objects $$D = (S_1, \dots, S_n)$$ and an object for method selection. The output is the canonical isomorphism $$\bigoplus_{i=1}^n S_i \rightarrow \bigsqcup_{i=1}^{n}S_i$$.

##### 6.6-20 IsomorphismFromCoproductToDirectSum
 ‣ IsomorphismFromCoproductToDirectSum( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigsqcup_{i=1}^{n}S_i, \bigoplus_{i=1}^n S_i )$$

The argument is a list of objects $$D = (S_1, \dots, S_n)$$. The output is the canonical isomorphism $$\bigsqcup_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i$$.

##### 6.6-21 IsomorphismFromCoproductToDirectSumOp
 ‣ IsomorphismFromCoproductToDirectSumOp( D, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigsqcup_{i=1}^{n}S_i, \bigoplus_{i=1}^n S_i )$$

The argument is a list of objects $$D = (S_1, \dots, S_n)$$ and an object for method selection. The output is the canonical isomorphism $$\bigsqcup_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i$$.

##### 6.6-22 MorphismBetweenDirectSums
 ‣ MorphismBetweenDirectSums( M ) ( operation )
 ‣ MorphismBetweenDirectSums( S, M, T ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\bigoplus_{i=1}^{m}A_i, \bigoplus_{j=1}^n B_j)$$

The argument $$M = ( ( \phi_{i,j}: A_i \rightarrow B_j )_{j = 1 \dots n} )_{i = 1 \dots m}$$ is a list of lists of morphisms. The output is the morphism $$\bigoplus_{i=1}^{m}A_i \rightarrow \bigoplus_{j=1}^n B_j$$ defined by the matrix $$M$$. The extra arguments $$S = \bigoplus_{i=1}^{m}A_i$$ and $$T = \bigoplus_{j=1}^n B_j$$ are source and target of the output, respectively. They must be provided in case $$M$$ is an empty list or a list of empty lists.

 ‣ AddMorphismBetweenDirectSums( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MorphismBetweenDirectSums. $$F: (\bigoplus_{i=1}^{m}A_i, M, \bigoplus_{j=1}^n B_j) \mapsto (\bigoplus_{i=1}^{m}A_i \rightarrow \bigoplus_{j=1}^n B_j)$$.

##### 6.6-24 MorphismBetweenDirectSumsOp
 ‣ MorphismBetweenDirectSumsOp( M, m, n, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\bigoplus_{i=1}^{m}A_i, \bigoplus_{j=1}^n B_j)$$

The arguments are a list $$M = ( \phi_{1,1}, \phi_{1,2}, \dots, \phi_{1,n}, \phi_{2,1}, \dots, \phi_{m,n} )$$ of morphisms $$\phi_{i,j}: A_i \rightarrow B_j$$, an integer $$m$$, an integer $$n$$, and a method selection morphism. The output is the morphism $$\bigoplus_{i=1}^{m}A_i \rightarrow \bigoplus_{j=1}^n B_j$$ defined by the list $$M$$ regarded as a matrix of dimension $$m \times n$$.

##### 6.6-25 ComponentOfMorphismIntoDirectSum
 ‣ ComponentOfMorphismIntoDirectSum( alpha, D, k ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(A, S_k)$$

The arguments are a morphism $$\alpha: A \rightarrow S$$, a list $$D = (S_1, \dots, S_n)$$ of objects with $$S = \bigoplus_{j=1}^n S_j$$, and an integer $$k$$. The output is the component morphism $$A \rightarrow S_k$$.

##### 6.6-26 ComponentOfMorphismFromDirectSum
 ‣ ComponentOfMorphismFromDirectSum( alpha, D, k ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(S_k, A)$$

The arguments are a morphism $$\alpha: S \rightarrow A$$, a list $$D = (S_1, \dots, S_n)$$ of objects with $$S = \bigoplus_{j=1}^n S_j$$, and an integer $$k$$. The output is the component morphism $$S_k \rightarrow A$$.

 ‣ AddComponentOfMorphismIntoDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ComponentOfMorphismIntoDirectSum. $$F: (\alpha: A \rightarrow S,D,k) \mapsto (A \rightarrow S_k)$$.

 ‣ AddComponentOfMorphismFromDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ComponentOfMorphismFromDirectSum. $$F: (\alpha: S \rightarrow A,D,k) \mapsto (S_k \rightarrow A)$$.

 ‣ AddProjectionInFactorOfDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ProjectionInFactorOfDirectSum. $$F: (D,k) \mapsto \pi_{k}$$.

 ‣ AddProjectionInFactorOfDirectSumWithGivenDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ProjectionInFactorOfDirectSumWithGivenDirectSum. $$F: (D,k,S) \mapsto \pi_{k}$$.

 ‣ AddInjectionOfCofactorOfDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InjectionOfCofactorOfDirectSum. $$F: (D,k) \mapsto \iota_{k}$$.

 ‣ AddInjectionOfCofactorOfDirectSumWithGivenDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InjectionOfCofactorOfDirectSumWithGivenDirectSum. $$F: (D,k,S) \mapsto \iota_{k}$$.

 ‣ AddUniversalMorphismIntoDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoDirectSum. $$F: (D,\tau) \mapsto u_{\mathrm{in}}(\tau)$$.

 ‣ AddUniversalMorphismIntoDirectSumWithGivenDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoDirectSumWithGivenDirectSum. $$F: (D,\tau,S) \mapsto u_{\mathrm{in}}(\tau)$$.

 ‣ AddUniversalMorphismFromDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromDirectSum. $$F: (D,\tau) \mapsto u_{\mathrm{out}}(\tau)$$.

 ‣ AddUniversalMorphismFromDirectSumWithGivenDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromDirectSumWithGivenDirectSum. $$F: (D,\tau,S) \mapsto u_{\mathrm{out}}(\tau)$$.

 ‣ AddIsomorphismFromDirectSumToDirectProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromDirectSumToDirectProduct. $$F: D \mapsto (\bigoplus_{i=1}^n S_i \rightarrow \prod_{i=1}^{n}S_i)$$.

 ‣ AddIsomorphismFromDirectProductToDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromDirectProductToDirectSum. $$F: D \mapsto ( \prod_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i )$$.

 ‣ AddIsomorphismFromDirectSumToCoproduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromDirectSumToCoproduct. $$F: D \mapsto ( \bigoplus_{i=1}^n S_i \rightarrow \bigsqcup_{i=1}^{n}S_i )$$.

 ‣ AddIsomorphismFromCoproductToDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromCoproductToDirectSum. $$F: D \mapsto ( \bigsqcup_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i )$$.

 ‣ AddDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DirectSum. $$F: D \mapsto \bigoplus_{i=1}^n S_i$$.

##### 6.6-42 DirectSumFunctorial
 ‣ DirectSumFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n S_i, \bigoplus_{i=1}^n S_i' )$$

The argument is a list of morphisms $$L = ( \mu_1: S_1 \rightarrow S_1', \dots, \mu_n: S_n \rightarrow S_n' )$$. The output is a morphism $$\bigoplus_{i=1}^n S_i \rightarrow \bigoplus_{i=1}^n S_i'$$ given by the functoriality of the direct sum.

##### 6.6-43 DirectSumFunctorialWithGivenDirectSums
 ‣ DirectSumFunctorialWithGivenDirectSums( d_1, L, d_2 ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( d_1, d_2 )$$

The arguments are an object $$d_1 = \bigoplus_{i=1}^n S_i$$, a list of morphisms $$L = ( \mu_1: S_1 \rightarrow S_1', \dots, \mu_n: S_n \rightarrow S_n' )$$, and an object $$d_2 = \bigoplus_{i=1}^n S_i'$$. The output is a morphism $$d_1 \rightarrow d_2$$ given by the functoriality of the direct sum.

 ‣ AddDirectSumFunctorialWithGivenDirectSums( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DirectSumFunctorialWithGivenDirectSums. $$F: (\bigoplus_{i=1}^n S_i, ( \mu_1, \dots, \mu_n ), \bigoplus_{i=1}^n S_i') \mapsto (\bigoplus_{i=1}^n S_i \rightarrow \bigoplus_{i=1}^n S_i')$$.

#### 6.7 Coproduct

For a given list of objects $$D = ( I_1, \dots, I_n )$$, a coproduct of $$D$$ consists of three parts:

• an object $$I$$,

• a list of morphisms $$\iota = ( \iota_i: I_i \rightarrow I )_{i = 1 \dots n}$$

• a dependent function $$u$$ mapping each list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )$$ to a morphism $$u( \tau ): I \rightarrow T$$ such that $$u( \tau ) \circ \iota_i \sim_{I_i, T} \tau_i$$ for all $$i = 1, \dots, n$$.

The triple $$( I, \iota, u )$$ is called a coproduct of $$D$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$I$$ of such a triple by $$\bigsqcup_{i=1}^n I_i$$. We say that the morphism $$u( \tau )$$ is induced by the universal property of the coproduct. $$\\$$ $$\mathrm{Coproduct}$$ is a functorial operation. This means: For $$(\mu_i: I_i \rightarrow I'_i)_{i=1\dots n}$$, we obtain a morphism $$\bigsqcup_{i=1}^n I_i \rightarrow \bigsqcup_{i=1}^n I_i'$$.

##### 6.7-1 Coproduct
 ‣ Coproduct( D ) ( attribute )

Returns: an object

The argument is a list of objects $$D = ( I_1, \dots, I_n )$$. The output is the coproduct $$\bigsqcup_{i=1}^n I_i$$.

##### 6.7-2 Coproduct
 ‣ Coproduct( I1, I2 ) ( operation )

Returns: an object

This is a convenience method. The arguments are two objects $$I_1, I_2$$. The output is the coproduct $$I_1 \bigsqcup I_2$$.

##### 6.7-3 Coproduct
 ‣ Coproduct( I1, I2 ) ( operation )

Returns: an object

This is a convenience method. The arguments are three objects $$I_1, I_2, I_3$$. The output is the coproduct $$I_1 \bigsqcup I_2 \bigsqcup I_3$$.

##### 6.7-4 CoproductOp
 ‣ CoproductOp( D, method_selection_object ) ( operation )

Returns: an object

The arguments are a list of objects $$D = ( I_1, \dots, I_n )$$ and a method selection object. The output is the coproduct $$\bigsqcup_{i=1}^n I_i$$.

##### 6.7-5 InjectionOfCofactorOfCoproduct
 ‣ InjectionOfCofactorOfCoproduct( D, k ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(I_k, \bigsqcup_{i=1}^n I_i)$$

The arguments are a list of objects $$D = ( I_1, \dots, I_n )$$ and an integer $$k$$. The output is the $$k$$-th injection $$\iota_k: I_k \rightarrow \bigsqcup_{i=1}^n I_i$$.

##### 6.7-6 InjectionOfCofactorOfCoproductOp
 ‣ InjectionOfCofactorOfCoproductOp( D, k, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(I_k, \bigsqcup_{i=1}^n I_i)$$

The arguments are a list of objects $$D = ( I_1, \dots, I_n )$$, an integer $$k$$, and a method selection object. The output is the $$k$$-th injection $$\iota_k: I_k \rightarrow \bigsqcup_{i=1}^n I_i$$.

##### 6.7-7 InjectionOfCofactorOfCoproductWithGivenCoproduct
 ‣ InjectionOfCofactorOfCoproductWithGivenCoproduct( D, k, I ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(I_k, I)$$

The arguments are a list of objects $$D = ( I_1, \dots, I_n )$$, an integer $$k$$, and an object $$I = \bigsqcup_{i=1}^n I_i$$. The output is the $$k$$-th injection $$\iota_k: I_k \rightarrow I$$.

##### 6.7-8 UniversalMorphismFromCoproduct
 ‣ UniversalMorphismFromCoproduct( arg ) ( function )

Returns: a morphism in $$\mathrm{Hom}(\bigsqcup_{i=1}^n I_i, T)$$

This is a convenience method. There are three different ways to use this method.

• The arguments are a list of objects $$D = ( I_1, \dots, I_n )$$, a list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )$$.

• The argument is a list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )$$.

• The arguments are morphisms $$\tau_1: I_1 \rightarrow T, \dots, \tau_n: I_n \rightarrow T$$

The output is the morphism $$u( \tau ): \bigsqcup_{i=1}^n I_i \rightarrow T$$ given by the universal property of the coproduct.

##### 6.7-9 UniversalMorphismFromCoproductOp
 ‣ UniversalMorphismFromCoproductOp( D, tau, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\bigsqcup_{i=1}^n I_i, T)$$

The arguments are a list of objects $$D = ( I_1, \dots, I_n )$$, a list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )$$, and a method selection object. The output is the morphism $$u( \tau ): \bigsqcup_{i=1}^n I_i \rightarrow T$$ given by the universal property of the coproduct.

##### 6.7-10 UniversalMorphismFromCoproductWithGivenCoproduct
 ‣ UniversalMorphismFromCoproductWithGivenCoproduct( D, tau, I ) ( operation )

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

The arguments are a list of objects $$D = ( I_1, \dots, I_n )$$, a list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )$$, and an object $$I = \bigsqcup_{i=1}^n I_i$$. The output is the morphism $$u( \tau ): I \rightarrow T$$ given by the universal property of the coproduct.

 ‣ AddCoproduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation Coproduct. $$F: ( (I_1, \dots, I_n) ) \mapsto I$$.

 ‣ AddInjectionOfCofactorOfCoproduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InjectionOfCofactorOfCoproduct. $$F: ( (I_1, \dots, I_n), i ) \mapsto \iota_i$$.

 ‣ AddInjectionOfCofactorOfCoproductWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InjectionOfCofactorOfCoproductWithGivenCoproduct. $$F: ( (I_1, \dots, I_n), i, I ) \mapsto \iota_i$$.

 ‣ AddUniversalMorphismFromCoproduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromCoproduct. $$F: ( (I_1, \dots, I_n), \tau ) \mapsto u( \tau )$$.

 ‣ AddUniversalMorphismFromCoproductWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromCoproductWithGivenCoproduct. $$F: ( (I_1, \dots, I_n), \tau, I ) \mapsto u( \tau )$$.

##### 6.7-16 CoproductFunctorial
 ‣ CoproductFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\bigsqcup_{i=1}^n I_i, \bigsqcup_{i=1}^n I_i')$$

The argument is a list $$L = ( \mu_1: I_1 \rightarrow I_1', \dots, \mu_n: I_n \rightarrow I_n' )$$. The output is a morphism $$\bigsqcup_{i=1}^n I_i \rightarrow \bigsqcup_{i=1}^n I_i'$$ given by the functoriality of the coproduct.

##### 6.7-17 CoproductFunctorialWithGivenCoproducts
 ‣ CoproductFunctorialWithGivenCoproducts( s, L, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(s, r)$$

The arguments are an object $$s = \bigsqcup_{i=1}^n I_i$$, a list $$L = ( \mu_1: I_1 \rightarrow I_1', \dots, \mu_n: I_n \rightarrow I_n' )$$, and an object $$r = \bigsqcup_{i=1}^n I_i'$$. The output is a morphism $$\bigsqcup_{i=1}^n I_i \rightarrow \bigsqcup_{i=1}^n I_i'$$ given by the functoriality of the coproduct.

 ‣ AddCoproductFunctorialWithGivenCoproducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CoproductFunctorialWithGivenCoproducts. $$F: (\bigsqcup_{i=1}^n I_i, (\mu_1, \dots, \mu_n), \bigsqcup_{i=1}^n I_i') \rightarrow (\bigsqcup_{i=1}^n I_i \rightarrow \bigsqcup_{i=1}^n I_i')$$.

#### 6.8 Direct Product

For a given list of objects $$D = ( P_1, \dots, P_n )$$, a direct product of $$D$$ consists of three parts:

• an object $$P$$,

• a list of morphisms $$\pi = ( \pi_i: P \rightarrow P_i )_{i = 1 \dots n}$$

• a dependent function $$u$$ mapping each list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}$$ to a morphism $$u(\tau): T \rightarrow P$$ such that $$\pi_i \circ u( \tau ) \sim_{T,P_i} \tau_i$$ for all $$i = 1, \dots, n$$.

The triple $$( P, \pi, u )$$ is called a direct product of $$D$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$P$$ of such a triple by $$\prod_{i=1}^n P_i$$. We say that the morphism $$u( \tau )$$ is induced by the universal property of the direct product. $$\\$$ $$\mathrm{DirectProduct}$$ is a functorial operation. This means: For $$(\mu_i: P_i \rightarrow P'_i)_{i=1\dots n}$$, we obtain a morphism $$\prod_{i=1}^n P_i \rightarrow \prod_{i=1}^n P_i'$$.

##### 6.8-1 DirectProductOp
 ‣ DirectProductOp( D ) ( operation )

Returns: an object

The arguments are a list of objects $$D = ( P_1, \dots, P_n )$$ and an object for method selection. The output is the direct product $$\prod_{i=1}^n P_i$$.

##### 6.8-2 ProjectionInFactorOfDirectProduct
 ‣ ProjectionInFactorOfDirectProduct( D, k ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\prod_{i=1}^n P_i, P_k)$$

The arguments are a list of objects $$D = ( P_1, \dots, P_n )$$ and an integer $$k$$. The output is the $$k$$-th projection $$\pi_k: \prod_{i=1}^n P_i \rightarrow P_k$$.

##### 6.8-3 ProjectionInFactorOfDirectProductOp
 ‣ ProjectionInFactorOfDirectProductOp( D, k, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\prod_{i=1}^n P_i, P_k)$$

The arguments are a list of objects $$D = ( P_1, \dots, P_n )$$, an integer $$k$$, and an object for method selection. The output is the $$k$$-th projection $$\pi_k: \prod_{i=1}^n P_i \rightarrow P_k$$.

##### 6.8-4 ProjectionInFactorOfDirectProductWithGivenDirectProduct
 ‣ ProjectionInFactorOfDirectProductWithGivenDirectProduct( D, k, P ) ( operation )

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

The arguments are a list of objects $$D = ( P_1, \dots, P_n )$$, an integer $$k$$, and an object $$P = \prod_{i=1}^n P_i$$. The output is the $$k$$-th projection $$\pi_k: P \rightarrow P_k$$.

##### 6.8-5 UniversalMorphismIntoDirectProduct
 ‣ UniversalMorphismIntoDirectProduct( arg ) ( function )

Returns: a morphism in $$\mathrm{Hom}(T, \prod_{i=1}^n P_i)$$

This is a convenience method. There are three different ways to use this method.

• The arguments are a list of objects $$D = ( P_1, \dots, P_n )$$ and a list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}$$.

• The argument is a list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}$$.

• The arguments are morphisms $$\tau_1: T \rightarrow P_1, \dots, \tau_n: T \rightarrow P_n$$.

The output is the morphism $$u(\tau): T \rightarrow \prod_{i=1}^n P_i$$ given by the universal property of the direct product.

##### 6.8-6 UniversalMorphismIntoDirectProductOp
 ‣ UniversalMorphismIntoDirectProductOp( D, tau, method_selection_object ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(T, \prod_{i=1}^n P_i)$$

The arguments are a list of objects $$D = ( P_1, \dots, P_n )$$, a list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}$$, and an object for method selection. The output is the morphism $$u(\tau): T \rightarrow \prod_{i=1}^n P_i$$ given by the universal property of the direct product.

##### 6.8-7 UniversalMorphismIntoDirectProductWithGivenDirectProduct
 ‣ UniversalMorphismIntoDirectProductWithGivenDirectProduct( D, tau, P ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(T, \prod_{i=1}^n P_i)$$

The arguments are a list of objects $$D = ( P_1, \dots, P_n )$$, a list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}$$, and an object $$P = \prod_{i=1}^n P_i$$. The output is the morphism $$u(\tau): T \rightarrow \prod_{i=1}^n P_i$$ given by the universal property of the direct product.

 ‣ AddDirectProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DirectProduct. $$F: ( (P_1, \dots, P_n) ) \mapsto P$$

 ‣ AddProjectionInFactorOfDirectProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ProjectionInFactorOfDirectProduct. $$F: ( (P_1, \dots, P_n),k ) \mapsto \pi_k$$

 ‣ AddProjectionInFactorOfDirectProductWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ProjectionInFactorOfDirectProductWithGivenDirectProduct. $$F: ( (P_1, \dots, P_n),k,P ) \mapsto \pi_k$$

 ‣ AddUniversalMorphismIntoDirectProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoDirectProduct. $$F: ( (P_1, \dots, P_n), \tau ) \mapsto u( \tau )$$

 ‣ AddUniversalMorphismIntoDirectProductWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoDirectProductWithGivenDirectProduct. $$F: ( (P_1, \dots, P_n), \tau, P ) \mapsto u( \tau )$$

##### 6.8-13 DirectProductFunctorial
 ‣ DirectProductFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \prod_{i=1}^n P_i, \prod_{i=1}^n P_i' )$$

The argument is a list of morphisms $$L = (\mu_i: P_i \rightarrow P'_i)_{i=1\dots n}$$. The output is a morphism $$\prod_{i=1}^n P_i \rightarrow \prod_{i=1}^n P_i'$$ given by the functoriality of the direct product.

##### 6.8-14 DirectProductFunctorialWithGivenDirectProducts
 ‣ DirectProductFunctorialWithGivenDirectProducts( s, L, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( s, r )$$

The arguments are an object $$s = \prod_{i=1}^n P_i$$, a list of morphisms $$L = (\mu_i: P_i \rightarrow P'_i)_{i=1\dots n}$$, and an object $$r = \prod_{i=1}^n P_i'$$. The output is a morphism $$\prod_{i=1}^n P_i \rightarrow \prod_{i=1}^n P_i'$$ given by the functoriality of the direct product.

 ‣ AddDirectProductFunctorialWithGivenDirectProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DirectProductFunctorialWithGivenDirectProducts. $$F: ( \prod_{i=1}^n P_i, (\mu_i: P_i \rightarrow P'_i)_{i=1\dots n}, \prod_{i=1}^n P_i' ) \mapsto (\prod_{i=1}^n P_i \rightarrow \prod_{i=1}^n P_i')$$

##### 6.8-16 AssociatorRightToLeftOfDirectProductsWithGivenDirectProducts
 ‣ AssociatorRightToLeftOfDirectProductsWithGivenDirectProducts( s, a, b, c, r ) ( operation )

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

The arguments are an object $$s = a \times (b \times c)$$, three objects $$a,b,c$$, and an object $$r = (a \times b) \times c$$. The output is the associator $$\alpha_{a,(b,c)}: a \times (b \times c) \rightarrow (a \times b) \times c$$.

 ‣ AddAssociatorRightToLeftOfDirectProductsWithGivenDirectProducts( C, F ) ( operation )

Returns: nothing

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

##### 6.8-18 AssociatorLeftToRightOfDirectProductsWithGivenDirectProducts
 ‣ AssociatorLeftToRightOfDirectProductsWithGivenDirectProducts( s, a, b, c, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( (a \times b) \times c \rightarrow a \times (b \times c) )$$.

The arguments are an object $$s = (a \times b) \times c$$, three objects $$a,b,c$$, and an object $$r = a \times (b \times c)$$. The output is the associator $$\alpha_{(a,b),c}: (a \times b) \times c \rightarrow a \times (b \times c)$$.

 ‣ AddAssociatorLeftToRightOfDirectProductsWithGivenDirectProducts( C, F ) ( operation )

Returns: nothing

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

#### 6.9 Equalizer

For a given list of morphisms $$D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$$, an equalizer of $$D$$ consists of three parts:

• an object $$E$$,

• a morphism $$\iota: E \rightarrow A$$ such that $$\beta_i \circ \iota \sim_{E, B} \beta_j \circ \iota$$ for all pairs $$i,j$$.

• a dependent function $$u$$ mapping each morphism $$\tau = ( \tau: T \rightarrow A )$$ such that $$\beta_i \circ \tau \sim_{T, B} \beta_j \circ \tau$$ for all pairs $$i,j$$ to a morphism $$u( \tau ): T \rightarrow E$$ such that $$\iota \circ u( \tau ) \sim_{T, A} \tau$$.

The triple $$( E, \iota, u )$$ is called an equalizer of $$D$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$E$$ of such a triple by $$\mathrm{Equalizer}(D)$$. We say that the morphism $$u( \tau )$$ is induced by the universal property of the equalizer. $$\\$$ $$\mathrm{Equalizer}$$ is a functorial operation. This means: For a second diagram $$D' = (\beta_i': A' \rightarrow B')_{i = 1 \dots n}$$ and a natural morphism between equalizer diagrams (i.e., a collection of morphisms $$\mu: A \rightarrow A'$$ and $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \mu \sim_{A,B'} \beta \circ \beta_i$$ for $$i = 1, \dots, n$$) we obtain a morphism $$\mathrm{Equalizer}( D ) \rightarrow \mathrm{Equalizer}( D' )$$.

##### 6.9-1 Equalizer
 ‣ Equalizer( arg ) ( function )

Returns: an object

This is a convenience method. There are two different ways to use this method:

• The argument is a list of morphisms $$D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$$.

• The arguments are morphisms $$\beta_1: A \rightarrow B, \dots, \beta_n: A \rightarrow B$$.

The output is the equalizer $$\mathrm{Equalizer}(D)$$.

##### 6.9-2 EqualizerOp
 ‣ EqualizerOp( D, method_selection_morphism ) ( operation )

Returns: an object

The arguments are a list of morphisms $$D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$$ and a morphism for method selection. The output is the equalizer $$\mathrm{Equalizer}(D)$$.

##### 6.9-3 EmbeddingOfEqualizer
 ‣ EmbeddingOfEqualizer( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{Equalizer}(D), A )$$

The arguments are a list of morphisms $$D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$$. The output is the equalizer embedding $$\iota: \mathrm{Equalizer}(D) \rightarrow A$$.

##### 6.9-4 EmbeddingOfEqualizerOp
 ‣ EmbeddingOfEqualizerOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{Equalizer}(D), A )$$

The arguments are a list of morphisms $$D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$$. and a morphism for method selection. The output is the equalizer embedding $$\iota: \mathrm{Equalizer}(D) \rightarrow A$$.

##### 6.9-5 EmbeddingOfEqualizerWithGivenEqualizer
 ‣ EmbeddingOfEqualizerWithGivenEqualizer( D, E ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( E, A )$$

The arguments are a list of morphisms $$D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$$, and an object $$E = \mathrm{Equalizer}(D)$$. The output is the equalizer embedding $$\iota: E \rightarrow A$$.

##### 6.9-6 UniversalMorphismIntoEqualizer
 ‣ UniversalMorphismIntoEqualizer( D, tau ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( T, \mathrm{Equalizer}(D) )$$

The arguments are a list of morphisms $$D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$$ and a morphism $$\tau: T \rightarrow A$$ such that $$\beta_i \circ \tau \sim_{T, B} \beta_j \circ \tau$$ for all pairs $$i,j$$. The output is the morphism $$u( \tau ): T \rightarrow \mathrm{Equalizer}(D)$$ given by the universal property of the equalizer.

##### 6.9-7 UniversalMorphismIntoEqualizerWithGivenEqualizer
 ‣ UniversalMorphismIntoEqualizerWithGivenEqualizer( D, tau, E ) ( operation )

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

The arguments are a list of morphisms $$D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}$$, a morphism $$\tau: T \rightarrow A )$$ such that $$\beta_i \circ \tau \sim_{T, B} \beta_j \circ \tau$$ for all pairs $$i,j$$, and an object $$E = \mathrm{Equalizer}(D)$$. The output is the morphism $$u( \tau ): T \rightarrow E$$ given by the universal property of the equalizer.

 ‣ AddEqualizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation Equalizer. $$F: ( (\beta_i: A \rightarrow B)_{i = 1 \dots n} ) \mapsto E$$

 ‣ AddEmbeddingOfEqualizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation EmbeddingOfEqualizer. $$F: ( (\beta_i: A \rightarrow B)_{i = 1 \dots n}, k ) \mapsto \iota$$

 ‣ AddEmbeddingOfEqualizerWithGivenEqualizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation EmbeddingOfEqualizerWithGivenEqualizer. $$F: ( (\beta_i: A \rightarrow B)_{i = 1 \dots n},E ) \mapsto \iota$$

 ‣ AddUniversalMorphismIntoEqualizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoEqualizer. $$F: ( (\beta_i: A \rightarrow B)_{i = 1 \dots n}, \tau ) \mapsto u(\tau)$$

 ‣ AddUniversalMorphismIntoEqualizerWithGivenEqualizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoEqualizerWithGivenEqualizer. $$F: ( (\beta_i: A \rightarrow B)_{i = 1 \dots n}, \tau, E ) \mapsto u(\tau)$$

##### 6.9-13 EqualizerFunctorial
 ‣ EqualizerFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{Equalizer}( ( \beta_i )_{i=1 \dots n} ), \mathrm{Equalizer}( ( \beta_i' )_{i=1 \dots n} ))$$

The argument is a triple $$L = ( (\beta_i: A \rightarrow B)_{i = 1 \dots n}, \mu: A \rightarrow A', (\beta_i': A' \rightarrow B')_{i = 1 \dots n} )$$ with morphisms $$\beta_i$$, $$\mu$$ and $$\beta_i'$$ such that there exists a morphism $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \mu \sim_{A,B'} \beta \circ \beta_i$$ for $$i = 1, \dots, n$$. The output is the morphism $$\mathrm{Equalizer}( ( \beta_i )_{i=1 \dots n} ) \rightarrow \mathrm{Equalizer}( ( \beta_i' )_{i=1 \dots n} )$$ given by the functorality of the equalizer.

##### 6.9-14 EqualizerFunctorialWithGivenEqualizers
 ‣ EqualizerFunctorialWithGivenEqualizers( s, L, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(s, r)$$

The arguments are an object $$s = \mathrm{Equalizer}( ( \beta_i )_{i=1 \dots n} )$$, a triple $$L = ( (\beta_i: A \rightarrow B)_{i = 1 \dots n}, \mu: A \rightarrow A', (\beta_i': A' \rightarrow B')_{i = 1 \dots n} )$$ with morphisms $$\beta_i$$, $$\mu$$ and $$\beta_i'$$ such that there exists a morphism $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \mu \sim_{A,B'} \beta \circ \beta_i$$ for $$i = 1, \dots, n$$, and an object $$r = \mathrm{Equalizer}( ( \beta_i' )_{i=1 \dots n} )$$. The output is the morphism $$s \rightarrow r$$ given by the functorality of the equalizer.

 ‣ AddEqualizerFunctorialWithGivenEqualizers( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation EqualizerFunctorialWithGivenEqualizers. $$F: ( \mathrm{Equalizer}( ( \beta_i )_{i=1 \dots n} ), ( ( \beta_i: A \rightarrow B )_{i = 1 \dots n}, \mu: A \rightarrow A', ( \beta_i': A' \rightarrow B' )_{i = 1 \dots n} ), \mathrm{Equalizer}( ( \beta_i' )_{i=1 \dots n} ) ) \mapsto (\mathrm{Equalizer}( ( \beta_i )_{i=1 \dots n} ) \rightarrow \mathrm {Equalizer}( ( \beta_i' )_{i=1 \dots n} ) )$$

#### 6.10 Coequalizer

For a given list of morphisms $$D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$$, a coequalizer of $$D$$ consists of three parts:

• an object $$C$$,

• a morphism $$\pi: A \rightarrow C$$ such that $$\pi \circ \beta_i \sim_{B,C} \pi \circ \beta_j$$ for all pairs $$i,j$$,

• a dependent function $$u$$ mapping the morphism $$\tau: A \rightarrow T$$ such that $$\tau \circ \beta_i \sim_{B,T} \tau \circ \beta_j$$ to a morphism $$u( \tau ): C \rightarrow T$$ such that $$u( \tau ) \circ \pi \sim_{A, T} \tau$$.

The triple $$( C, \pi, u )$$ is called a coequalizer of $$D$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$C$$ of such a triple by $$\mathrm{Coequalizer}(D)$$. We say that the morphism $$u( \tau )$$ is induced by the universal property of the coequalizer. $$\\$$ $$\mathrm{Coequalizer}$$ is a functorial operation. This means: For a second diagram $$D' = (\beta_i': B' \rightarrow A')_{i = 1 \dots n}$$ and a natural morphism between coequalizer diagrams (i.e., a collection of morphisms $$\mu: A \rightarrow A'$$ and $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \beta \sim_{B, A'} \mu \circ \beta_i$$ for $$i = 1, \dots n$$) we obtain a morphism $$\mathrm{Coequalizer}( D ) \rightarrow \mathrm{Coequalizer}( D' )$$.

##### 6.10-1 Coequalizer
 ‣ Coequalizer( arg ) ( function )

Returns: an object

This is a convenience method. There are two different ways to use this method:

• The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$$.

• The arguments are morphisms $$\beta_1: B \rightarrow A, \dots, \beta_n: B \rightarrow A$$.

The output is the coequalizer $$\mathrm{Coequalizer}(D)$$.

##### 6.10-2 CoequalizerOp
 ‣ CoequalizerOp( D, method_selection_morphism ) ( operation )

Returns: an object

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$$ and a morphism for method selection. The output is the coequalizer $$\mathrm{Coequalizer}(D)$$.

##### 6.10-3 ProjectionOntoCoequalizer
 ‣ ProjectionOntoCoequalizer( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( A, \mathrm{Coequalizer}( D ) )$$.

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$$. The output is the projection $$\pi: A \rightarrow \mathrm{Coequalizer}( D )$$.

##### 6.10-4 ProjectionOntoCoequalizerOp
 ‣ ProjectionOntoCoequalizerOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( A, \mathrm{Coequalizer}( D ) )$$.

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$$, and a morphism for method selection. The output is the projection $$\pi: A \rightarrow \mathrm{Coequalizer}( D )$$.

##### 6.10-5 ProjectionOntoCoequalizerWithGivenCoequalizer
 ‣ ProjectionOntoCoequalizerWithGivenCoequalizer( D, C ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( A, C )$$.

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$$, and an object $$C = \mathrm{Coequalizer}(D)$$. The output is the projection $$\pi: A \rightarrow C$$.

##### 6.10-6 UniversalMorphismFromCoequalizer
 ‣ UniversalMorphismFromCoequalizer( D, tau ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{Coequalizer}(D), T )$$

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$$ and a morphism $$\tau: A \rightarrow T$$ such that $$\tau \circ \beta_i \sim_{B,T} \tau \circ \beta_j$$ for all pairs $$i,j$$. The output is the morphism $$u( \tau ): \mathrm{Coequalizer}(D) \rightarrow T$$ given by the universal property of the coequalizer.

##### 6.10-7 UniversalMorphismFromCoequalizerWithGivenCoequalizer
 ‣ UniversalMorphismFromCoequalizerWithGivenCoequalizer( D, tau, C ) ( operation )

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

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}$$, a morphism $$\tau: A \rightarrow T$$ such that $$\tau \circ \beta_i \sim_{B,T} \tau \circ \beta_j$$, and an object $$C = \mathrm{Coequalizer}(D)$$. The output is the morphism $$u( \tau ): C \rightarrow T$$ given by the universal property of the coequalizer.

 ‣ AddCoequalizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation Coequalizer. $$F: ( (\beta_i: B \rightarrow A)_{i = 1 \dots n} ) \mapsto C$$

 ‣ AddProjectionOntoCoequalizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ProjectionOntoCoequalizer. $$F: ( (\beta_i: B \rightarrow A)_{i = 1 \dots n}, k ) \mapsto \pi$$

 ‣ AddProjectionOntoCoequalizerWithGivenCoequalizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ProjectionOntoCoequalizerWithGivenCoequalizer. $$F: ( (\beta_i: B \rightarrow A)_{i = 1 \dots n}, C) \mapsto \pi$$

 ‣ AddUniversalMorphismFromCoequalizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromCoequalizer. $$F: ( (\beta_i: B \rightarrow A)_{i = 1 \dots n}, \tau ) \mapsto u(\tau)$$

 ‣ AddUniversalMorphismFromCoequalizerWithGivenCoequalizer( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromCoequalizerWithGivenCoequalizer. $$F: ( (\beta_i: B \rightarrow A)_{i = 1 \dots n}, \tau, C ) \mapsto u(\tau)$$

##### 6.10-13 CoequalizerFunctorial
 ‣ CoequalizerFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{Coequalizer}( ( \beta_i )_{i=1 \dots n} ), \mathrm{Coequalizer}( ( \beta_i' )_{i=1 \dots n} ))$$

The argument is a triple $$L = ( ( \beta_i: B \rightarrow A)_{i = 1 \dots n}, \mu: A \rightarrow A', ( \beta_i': B' \rightarrow A' )_{i = 1 \dots n} )$$ with morphisms $$\beta_i$$, $$\mu$$ and $$\beta_i'$$ such that there exists a morphism $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \beta \sim_{B, A'} \mu \circ \beta_i$$ for $$i = 1, \dots n$$. The output is the morphism $$\mathrm{Coequalizer}( ( \beta_i )_{i=1}^n ) \rightarrow \mathrm{Coequalizer}( ( \beta_i' )_{i=1}^n )$$ given by the functorality of the coequalizer.

##### 6.10-14 CoequalizerFunctorialWithGivenCoequalizers
 ‣ CoequalizerFunctorialWithGivenCoequalizers( s, L, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(s, r)$$

The arguments are an object $$s = \mathrm{Coequalizer}( ( \beta_i )_{i=1}^n )$$, a triple $$L = ( ( \beta_i: B \rightarrow A )_{i = 1 \dots n}, \mu: A \rightarrow A', ( \beta_i': B' \rightarrow A' )_{i = 1 \dots n} )$$ with morphisms $$\beta_i$$, $$\mu$$ and $$\beta_i'$$ such that there exists a morphism $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \beta \sim_{B, A'} \mu \circ \beta_i$$ for $$i = 1, \dots n$$, and an object $$r = \mathrm{Coequalizer}( ( \beta_i' )_{i=1}^n )$$. The output is the morphism $$s \rightarrow r$$ given by the functorality of the coequalizer.

 ‣ AddCoequalizerFunctorialWithGivenCoequalizers( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CoequalizerFunctorialWithGivenCoequalizers. $$F: ( \mathrm{Coequalizer}( ( \beta_i )_{i=1}^n ), ( ( \beta_i: B \rightarrow A )_{i = 1 \dots n}, \mu: A \rightarrow A', ( \beta_i': B' \rightarrow A' )_{i = 1 \dots n} ), \mathrm{Coequalizer}( ( \beta_i' )_{i=1}^n ) ) \mapsto (\mathrm{Coequalizer}( ( \beta_i )_{i=1}^n ) \rightarrow \mathrm{Coequalizer}( ( \beta_i' )_{i=1}^n ) )$$

#### 6.11 Fiber Product

For a given list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$, a fiber product of $$D$$ consists of three parts:

• an object $$P$$,

• a list of morphisms $$\pi = ( \pi_i: P \rightarrow P_i )_{i = 1 \dots n}$$ such that $$\beta_i \circ \pi_i \sim_{P, B} \beta_j \circ \pi_j$$ for all pairs $$i,j$$.

• a dependent function $$u$$ mapping each list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )$$ such that $$\beta_i \circ \tau_i \sim_{T, B} \beta_j \circ \tau_j$$ for all pairs $$i,j$$ to a morphism $$u( \tau ): T \rightarrow P$$ such that $$\pi_i \circ u( \tau ) \sim_{T, P_i} \tau_i$$ for all $$i = 1, \dots, n$$.

The triple $$( P, \pi, u )$$ is called a fiber product of $$D$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$P$$ of such a triple by $$\mathrm{FiberProduct}(D)$$. We say that the morphism $$u( \tau )$$ is induced by the universal property of the fiber product. $$\\$$ $$\mathrm{FiberProduct}$$ is a functorial operation. This means: For a second diagram $$D' = (\beta_i': P_i' \rightarrow B')_{i = 1 \dots n}$$ and a natural morphism between pullback diagrams (i.e., a collection of morphisms $$(\mu_i: P_i \rightarrow P'_i)_{i=1\dots n}$$ and $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \mu_i \sim_{P_i,B'} \beta \circ \beta_i$$ for $$i = 1, \dots, n$$) we obtain a morphism $$\mathrm{FiberProduct}( D ) \rightarrow \mathrm{FiberProduct}( D' )$$.

##### 6.11-1 IsomorphismFromFiberProductToKernelOfDiagonalDifference
 ‣ IsomorphismFromFiberProductToKernelOfDiagonalDifference( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{FiberProduct}(D), \Delta)$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$. The output is a morphism $$\mathrm{FiberProduct}(D) \rightarrow \Delta$$, where $$\Delta$$ denotes the kernel object equalizing the morphisms $$\beta_i$$.

##### 6.11-2 IsomorphismFromFiberProductToKernelOfDiagonalDifferenceOp
 ‣ IsomorphismFromFiberProductToKernelOfDiagonalDifferenceOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{FiberProduct}(D), \Delta)$$

The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\mathrm{FiberProduct}(D) \rightarrow \Delta$$, where $$\Delta$$ denotes the kernel object equalizing the morphisms $$\beta_i$$.

 ‣ AddIsomorphismFromFiberProductToKernelOfDiagonalDifference( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromFiberProductToKernelOfDiagonalDifference. $$F: ( ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n} ) \mapsto \mathrm{FiberProduct}(D) \rightarrow \Delta$$

##### 6.11-4 IsomorphismFromKernelOfDiagonalDifferenceToFiberProduct
 ‣ IsomorphismFromKernelOfDiagonalDifferenceToFiberProduct( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\Delta, \mathrm{FiberProduct}(D))$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$. The output is a morphism $$\Delta \rightarrow \mathrm{FiberProduct}(D)$$, where $$\Delta$$ denotes the kernel object equalizing the morphisms $$\beta_i$$.

##### 6.11-5 IsomorphismFromKernelOfDiagonalDifferenceToFiberProductOp
 ‣ IsomorphismFromKernelOfDiagonalDifferenceToFiberProductOp( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\Delta, \mathrm{FiberProduct}(D))$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\Delta \rightarrow \mathrm{FiberProduct}(D)$$, where $$\Delta$$ denotes the kernel object equalizing the morphisms $$\beta_i$$.

 ‣ AddIsomorphismFromKernelOfDiagonalDifferenceToFiberProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromKernelOfDiagonalDifferenceToFiberProduct. $$F: ( ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n} ) \mapsto \Delta \rightarrow \mathrm{FiberProduct}(D)$$

##### 6.11-7 IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram
 ‣ IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{FiberProduct}(D), \Delta)$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$. The output is a morphism $$\mathrm{FiberProduct}(D) \rightarrow \Delta$$, where $$\Delta$$ denotes the equalizer of the product diagram of the morphisms $$\beta_i$$.

##### 6.11-8 IsomorphismFromFiberProductToEqualizerOfDirectProductDiagramOp
 ‣ IsomorphismFromFiberProductToEqualizerOfDirectProductDiagramOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{FiberProduct}(D), \Delta)$$

The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\mathrm{FiberProduct}(D) \rightarrow \Delta$$, where $$\Delta$$ denotes the equalizer of the product diagram of the morphisms $$\beta_i$$.

 ‣ AddIsomorphismFromFiberProductToEqualizerOfDirectProductDiagram( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram. $$F: ( ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n} ) \mapsto \mathrm{FiberProduct}(D) \rightarrow \Delta$$

##### 6.11-10 IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct
 ‣ IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\Delta, \mathrm{FiberProduct}(D))$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$. The output is a morphism $$\Delta \rightarrow \mathrm{FiberProduct}(D)$$, where $$\Delta$$ denotes the equalizer of the product diagram of the morphisms $$\beta_i$$.

##### 6.11-11 IsomorphismFromEqualizerOfDirectProductDiagramToFiberProductOp
 ‣ IsomorphismFromEqualizerOfDirectProductDiagramToFiberProductOp( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\Delta, \mathrm{FiberProduct}(D))$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\Delta \rightarrow \mathrm{FiberProduct}(D)$$, where $$\Delta$$ denotes the equalizer of the product diagram of the morphisms $$\beta_i$$.

 ‣ AddIsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct. $$F: ( ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n} ) \mapsto \Delta \rightarrow \mathrm{FiberProduct}(D)$$

##### 6.11-13 DirectSumDiagonalDifference
 ‣ DirectSumDiagonalDifference( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n P_i, B )$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$. The output is a morphism $$\bigoplus_{i=1}^n P_i \rightarrow B$$ such that its kernel equalizes the $$\beta_i$$.

##### 6.11-14 DirectSumDiagonalDifferenceOp
 ‣ DirectSumDiagonalDifferenceOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n P_i, B )$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\bigoplus_{i=1}^n P_i \rightarrow B$$ such that its kernel equalizes the $$\beta_i$$.

 ‣ AddDirectSumDiagonalDifference( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DirectSumDiagonalDifference. $$F: ( D ) \mapsto \mathrm{DirectSumDiagonalDifference}(D)$$

##### 6.11-16 FiberProductEmbeddingInDirectSum
 ‣ FiberProductEmbeddingInDirectSum( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{FiberProduct}(D), \bigoplus_{i=1}^n P_i )$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$. The output is the natural embedding $$\mathrm{FiberProduct}(D) \rightarrow \bigoplus_{i=1}^n P_i$$.

##### 6.11-17 FiberProductEmbeddingInDirectSumOp
 ‣ FiberProductEmbeddingInDirectSumOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{FiberProduct}(D), \bigoplus_{i=1}^n P_i )$$

The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and a morphism for method selection. The output is the natural embedding $$\mathrm{FiberProduct}(D) \rightarrow \bigoplus_{i=1}^n P_i$$.

 ‣ AddFiberProductEmbeddingInDirectSum( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation FiberProductEmbeddingInDirectSum. $$F: ( ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n} ) \mapsto \mathrm{FiberProduct}(D) \rightarrow \bigoplus_{i=1}^n P_i$$

##### 6.11-19 FiberProduct
 ‣ FiberProduct( arg ) ( function )

Returns: an object

This is a convenience method. There are two different ways to use this method:

• The argument is a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$.

• The arguments are morphisms $$\beta_1: P_1 \rightarrow B, \dots, \beta_n: P_n \rightarrow B$$.

The output is the fiber product $$\mathrm{FiberProduct}(D)$$.

##### 6.11-20 FiberProductOp
 ‣ FiberProductOp( D, method_selection_morphism ) ( operation )

Returns: an object

The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and a morphism for method selection. The output is the fiber product $$\mathrm{FiberProduct}(D)$$.

##### 6.11-21 ProjectionInFactorOfFiberProduct
 ‣ ProjectionInFactorOfFiberProduct( D, k ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{FiberProduct}(D), P_k )$$

The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and an integer $$k$$. The output is the $$k$$-th projection $$\pi_{k}: \mathrm{FiberProduct}(D) \rightarrow P_k$$.

##### 6.11-22 ProjectionInFactorOfFiberProductOp
 ‣ ProjectionInFactorOfFiberProductOp( D, k, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{FiberProduct}(D), P_k )$$

The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$, an integer $$k$$, and a morphism for method selection. The output is the $$k$$-th projection $$\pi_{k}: \mathrm{FiberProduct}(D) \rightarrow P_k$$.

##### 6.11-23 ProjectionInFactorOfFiberProductWithGivenFiberProduct
 ‣ ProjectionInFactorOfFiberProductWithGivenFiberProduct( D, k, P ) ( operation )

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

The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$, an integer $$k$$, and an object $$P = \mathrm{FiberProduct}(D)$$. The output is the $$k$$-th projection $$\pi_{k}: P \rightarrow P_k$$.

##### 6.11-24 UniversalMorphismIntoFiberProduct
 ‣ UniversalMorphismIntoFiberProduct( arg ) ( function )

This is a convenience method. There are two different ways to use this method:

• The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and a list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )$$ such that $$\beta_i \circ \tau_i \sim_{T, B} \beta_j \circ \tau_j$$ for all pairs $$i,j$$. The output is the morphism $$u( \tau ): T \rightarrow \mathrm{FiberProduct}(D)$$ given by the universal property of the fiber product.

• The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$ and morphisms $$\tau_1: T \rightarrow P_1, \dots, \tau_n: T \rightarrow P_n$$ such that $$\beta_i \circ \tau_i \sim_{T, B} \beta_j \circ \tau_j$$ for all pairs $$i,j$$. The output is the morphism $$u( \tau ): T \rightarrow \mathrm{FiberProduct}(D)$$ given by the universal property of the fiber product.

##### 6.11-25 UniversalMorphismIntoFiberProductOp
 ‣ UniversalMorphismIntoFiberProductOp( D, tau, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( T, \mathrm{FiberProduct}(D) )$$

The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$, a list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )$$ such that $$\beta_i \circ \tau_i \sim_{T, B} \beta_j \circ \tau_j$$ for all pairs $$i,j$$, and a morphism for method selection. The output is the morphism $$u( \tau ): T \rightarrow \mathrm{FiberProduct}(D)$$ given by the universal property of the fiber product.

##### 6.11-26 UniversalMorphismIntoFiberProductWithGivenFiberProduct
 ‣ UniversalMorphismIntoFiberProductWithGivenFiberProduct( D, tau, P ) ( operation )

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

The arguments are a list of morphisms $$D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}$$, a list of morphisms $$\tau = ( \tau_i: T \rightarrow P_i )$$ such that $$\beta_i \circ \tau_i \sim_{T, B} \beta_j \circ \tau_j$$ for all pairs $$i,j$$, and an object $$P = \mathrm{FiberProduct}(D)$$. The output is the morphism $$u( \tau ): T \rightarrow P$$ given by the universal property of the fiber product.

 ‣ AddFiberProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation FiberProduct. $$F: ( (\beta_i: P_i \rightarrow B)_{i = 1 \dots n} ) \mapsto P$$

 ‣ AddProjectionInFactorOfFiberProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ProjectionInFactorOfFiberProduct. $$F: ( (\beta_i: P_i \rightarrow B)_{i = 1 \dots n}, k ) \mapsto \pi_k$$

 ‣ AddProjectionInFactorOfFiberProductWithGivenFiberProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ProjectionInFactorOfFiberProductWithGivenFiberProduct. $$F: ( (\beta_i: P_i \rightarrow B)_{i = 1 \dots n}, k,P ) \mapsto \pi_k$$

 ‣ AddUniversalMorphismIntoFiberProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoFiberProduct. $$F: ( (\beta_i: P_i \rightarrow B)_{i = 1 \dots n}, \tau ) \mapsto u(\tau)$$

 ‣ AddUniversalMorphismIntoFiberProductWithGivenFiberProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoFiberProductWithGivenFiberProduct. $$F: ( (\beta_i: P_i \rightarrow B)_{i = 1 \dots n}, \tau, P ) \mapsto u(\tau)$$

##### 6.11-32 FiberProductFunctorial
 ‣ FiberProductFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{FiberProduct}( ( \beta_i )_{i=1 \dots n} ), \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} ))$$

The argument is a list of triples of morphisms $$L = ( (\beta_i: P_i \rightarrow B, \mu_i: P_i \rightarrow P_i', \beta_i': P_i' \rightarrow B')_{i = 1 \dots n} )$$ such that there exists a morphism $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \mu_i \sim_{P_i,B'} \beta \circ \beta_i$$ for $$i = 1, \dots, n$$. The output is the morphism $$\mathrm{FiberProduct}( ( \beta_i )_{i=1 \dots n} ) \rightarrow \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} )$$ given by the functoriality of the fiber product.

##### 6.11-33 FiberProductFunctorialWithGivenFiberProducts
 ‣ FiberProductFunctorialWithGivenFiberProducts( s, L, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(s, r)$$

The arguments are an object $$s = \mathrm{FiberProduct}( ( \beta_i )_{i=1 \dots n} )$$, a list of triples of morphisms $$L = ( (\beta_i: P_i \rightarrow B, \mu_i: P_i \rightarrow P_i', \beta_i': P_i' \rightarrow B')_{i = 1 \dots n} )$$ such that there exists a morphism $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \mu_i \sim_{P_i,B'} \beta \circ \beta_i$$ for $$i = 1, \dots, n$$, and an object $$r = \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} )$$. The output is the morphism $$s \rightarrow r$$ given by the functoriality of the fiber product.

 ‣ AddFiberProductFunctorialWithGivenFiberProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation FiberProductFunctorialWithGivenFiberProducts. $$F: ( \mathrm{FiberProduct}( ( \beta_i )_{i=1 \dots n} ), (\beta_i: P_i \rightarrow B, \mu_i: P_i \rightarrow P_i', \beta_i': P_i' \rightarrow B')_{i = 1 \dots n}, \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} ) ) \mapsto (\mathrm{FiberProduct}( ( \beta_i )_{i=1 \dots n} ) \rightarrow \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} ) )$$

#### 6.12 Pushout

For a given list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$, a pushout of $$D$$ consists of three parts:

• an object $$I$$,

• a list of morphisms $$\iota = ( \iota_i: I_i \rightarrow I )_{i = 1 \dots n}$$ such that $$\iota_i \circ \beta_i \sim_{B,I} \iota_j \circ \beta_j$$ for all pairs $$i,j$$,

• a dependent function $$u$$ mapping each list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )_{i = 1 \dots n}$$ such that $$\tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j$$ to a morphism $$u( \tau ): I \rightarrow T$$ such that $$u( \tau ) \circ \iota_i \sim_{I_i, T} \tau_i$$ for all $$i = 1, \dots, n$$.

The triple $$( I, \iota, u )$$ is called a pushout of $$D$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$I$$ of such a triple by $$\mathrm{Pushout}(D)$$. We say that the morphism $$u( \tau )$$ is induced by the universal property of the pushout. $$\\$$ $$\mathrm{Pushout}$$ is a functorial operation. This means: For a second diagram $$D' = (\beta_i': B' \rightarrow I_i')_{i = 1 \dots n}$$ and a natural morphism between pushout diagrams (i.e., a collection of morphisms $$(\mu_i: I_i \rightarrow I'_i)_{i=1\dots n}$$ and $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \beta \sim_{B, I_i'} \mu_i \circ \beta_i$$ for $$i = 1, \dots n$$) we obtain a morphism $$\mathrm{Pushout}( D ) \rightarrow \mathrm{Pushout}( D' )$$.

##### 6.12-1 IsomorphismFromPushoutToCokernelOfDiagonalDifference
 ‣ IsomorphismFromPushoutToCokernelOfDiagonalDifference( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{Pushout}(D), \Delta)$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$. The output is a morphism $$\mathrm{Pushout}(D) \rightarrow \Delta$$, where $$\Delta$$ denotes the cokernel object coequalizing the morphisms $$\beta_i$$.

##### 6.12-2 IsomorphismFromPushoutToCokernelOfDiagonalDifferenceOp
 ‣ IsomorphismFromPushoutToCokernelOfDiagonalDifferenceOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{Pushout}(D), \Delta)$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\mathrm{Pushout}(D) \rightarrow \Delta$$, where $$\Delta$$ denotes the cokernel object coequalizing the morphisms $$\beta_i$$.

 ‣ AddIsomorphismFromPushoutToCokernelOfDiagonalDifference( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromPushoutToCokernelOfDiagonalDifference. $$F: ( ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n} ) \mapsto (\mathrm{Pushout}(D) \rightarrow \Delta)$$

##### 6.12-4 IsomorphismFromCokernelOfDiagonalDifferenceToPushout
 ‣ IsomorphismFromCokernelOfDiagonalDifferenceToPushout( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \Delta, \mathrm{Pushout}(D))$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$. The output is a morphism $$\Delta \rightarrow \mathrm{Pushout}(D)$$, where $$\Delta$$ denotes the cokernel object coequalizing the morphisms $$\beta_i$$.

##### 6.12-5 IsomorphismFromCokernelOfDiagonalDifferenceToPushoutOp
 ‣ IsomorphismFromCokernelOfDiagonalDifferenceToPushoutOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \Delta, \mathrm{Pushout}(D))$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\Delta \rightarrow \mathrm{Pushout}(D)$$, where $$\Delta$$ denotes the cokernel object coequalizing the morphisms $$\beta_i$$.

 ‣ AddIsomorphismFromCokernelOfDiagonalDifferenceToPushout( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromCokernelOfDiagonalDifferenceToPushout. $$F: ( ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n} ) \mapsto (\Delta \rightarrow \mathrm{Pushout}(D))$$

##### 6.12-7 IsomorphismFromPushoutToCoequalizerOfCoproductDiagram
 ‣ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{Pushout}(D), \Delta)$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$. The output is a morphism $$\mathrm{Pushout}(D) \rightarrow \Delta$$, where $$\Delta$$ denotes the coequalizer of the coproduct diagram of the morphisms $$\beta_i$$.

##### 6.12-8 IsomorphismFromPushoutToCoequalizerOfCoproductDiagramOp
 ‣ IsomorphismFromPushoutToCoequalizerOfCoproductDiagramOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{Pushout}(D), \Delta)$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\mathrm{Pushout}(D) \rightarrow \Delta$$, where $$\Delta$$ denotes the coequalizer of the coproduct diagram of the morphisms $$\beta_i$$.

 ‣ AddIsomorphismFromPushoutToCoequalizerOfCoproductDiagram( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromPushoutToCoequalizerOfCoproductDiagram. $$F: ( ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n} ) \mapsto (\mathrm{Pushout}(D) \rightarrow \Delta)$$

##### 6.12-10 IsomorphismFromCoequalizerOfCoproductDiagramToPushout
 ‣ IsomorphismFromCoequalizerOfCoproductDiagramToPushout( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \Delta, \mathrm{Pushout}(D))$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$. The output is a morphism $$\Delta \rightarrow \mathrm{Pushout}(D)$$, where $$\Delta$$ denotes the coequalizer of the coproduct diagram of the morphisms $$\beta_i$$.

##### 6.12-11 IsomorphismFromCoequalizerOfCoproductDiagramToPushoutOp
 ‣ IsomorphismFromCoequalizerOfCoproductDiagramToPushoutOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \Delta, \mathrm{Pushout}(D))$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$\Delta \rightarrow \mathrm{Pushout}(D)$$, where $$\Delta$$ denotes the coequalizer of the coproduct diagram of the morphisms $$\beta_i$$.

 ‣ AddIsomorphismFromCoequalizerOfCoproductDiagramToPushout( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromCoequalizerOfCoproductDiagramToPushout. $$F: ( ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n} ) \mapsto (\Delta \rightarrow \mathrm{Pushout}(D))$$

##### 6.12-13 DirectSumCodiagonalDifference
 ‣ DirectSumCodiagonalDifference( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(B, \bigoplus_{i=1}^n I_i)$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$. The output is a morphism $$B \rightarrow \bigoplus_{i=1}^n I_i$$ such that its cokernel coequalizes the $$\beta_i$$.

##### 6.12-14 DirectSumCodiagonalDifferenceOp
 ‣ DirectSumCodiagonalDifferenceOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(B, \bigoplus_{i=1}^n I_i)$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and a morphism for method selection. The output is a morphism $$B \rightarrow \bigoplus_{i=1}^n I_i$$ such that its cokernel coequalizes the $$\beta_i$$.

 ‣ AddDirectSumCodiagonalDifference( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DirectSumCodiagonalDifference. $$F: ( D ) \mapsto \mathrm{DirectSumCodiagonalDifference}(D)$$

##### 6.12-16 DirectSumProjectionInPushout
 ‣ DirectSumProjectionInPushout( D ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n I_i, \mathrm{Pushout}(D) )$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$. The output is the natural projection $$\bigoplus_{i=1}^n I_i \rightarrow \mathrm{Pushout}(D)$$.

##### 6.12-17 DirectSumProjectionInPushoutOp
 ‣ DirectSumProjectionInPushoutOp( D, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \bigoplus_{i=1}^n I_i, \mathrm{Pushout}(D) )$$

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and a morphism for method selection. The output is the natural projection $$\bigoplus_{i=1}^n I_i \rightarrow \mathrm{Pushout}(D)$$.

 ‣ AddDirectSumProjectionInPushout( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DirectSumProjectionInPushout. $$F: ( ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n} ) \mapsto (\bigoplus_{i=1}^n I_i \rightarrow \mathrm{Pushout}(D))$$

##### 6.12-19 Pushout
 ‣ Pushout( D ) ( operation )

Returns: an object

The argument is a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ The output is the pushout $$\mathrm{Pushout}(D)$$.

##### 6.12-20 Pushout
 ‣ Pushout( D ) ( operation )

Returns: an object

This is a convenience method. The arguments are a morphism $$\alpha$$ and a morphism $$\beta$$. The output is the pushout $$\mathrm{Pushout}(\alpha, \beta)$$.

##### 6.12-21 PushoutOp
 ‣ PushoutOp( D ) ( operation )

Returns: an object

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and a morphism for method selection. The output is the pushout $$\mathrm{Pushout}(D)$$.

##### 6.12-22 InjectionOfCofactorOfPushout
 ‣ InjectionOfCofactorOfPushout( D, k ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( I_k, \mathrm{Pushout}( D ) )$$.

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and an integer $$k$$. The output is the $$k$$-th injection $$\iota_k: I_k \rightarrow \mathrm{Pushout}( D )$$.

##### 6.12-23 InjectionOfCofactorOfPushoutOp
 ‣ InjectionOfCofactorOfPushoutOp( D, k, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( I_k, \mathrm{Pushout}( D ) )$$.

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$, an integer $$k$$, and a morphism for method selection. The output is the $$k$$-th injection $$\iota_k: I_k \rightarrow \mathrm{Pushout}( D )$$.

##### 6.12-24 InjectionOfCofactorOfPushoutWithGivenPushout
 ‣ InjectionOfCofactorOfPushoutWithGivenPushout( D, k, I ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( I_k, \mathrm{Pushout}( D ) )$$.

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$, an integer $$k$$, and an object $$I = \mathrm{Pushout}(D)$$. The output is the $$k$$-th injection $$\iota_k: I_k \rightarrow \mathrm{Pushout}( D )$$.

##### 6.12-25 UniversalMorphismFromPushout
 ‣ UniversalMorphismFromPushout( arg ) ( function )

This is a convenience method. There are two different ways to use this method:

• The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and a list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )_{i = 1 \dots n}$$ such that $$\tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j$$. The output is the morphism $$u( \tau ): \mathrm{Pushout}(D) \rightarrow T$$ given by the universal property of the pushout.

• The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$ and morphisms $$\tau_1: I_1 \rightarrow T, \dots, \tau_n: I_n \rightarrow T$$ such that $$\tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j$$. The output is the morphism $$u( \tau ): \mathrm{Pushout}(D) \rightarrow T$$ given by the universal property of the pushout.

##### 6.12-26 UniversalMorphismFromPushoutOp
 ‣ UniversalMorphismFromPushoutOp( D, tau, method_selection_morphism ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{Pushout}(D), T )$$

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$, a list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )_{i = 1 \dots n}$$ such that $$\tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j$$, and a morphism for method selection. The output is the morphism $$u( \tau ): \mathrm{Pushout}(D) \rightarrow T$$ given by the universal property of the pushout.

##### 6.12-27 UniversalMorphismFromPushoutWithGivenPushout
 ‣ UniversalMorphismFromPushoutWithGivenPushout( D, tau, I ) ( operation )

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

The arguments are a list of morphisms $$D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}$$, a list of morphisms $$\tau = ( \tau_i: I_i \rightarrow T )_{i = 1 \dots n}$$ such that $$\tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j$$, and an object $$I = \mathrm{Pushout}(D)$$. The output is the morphism $$u( \tau ): I \rightarrow T$$ given by the universal property of the pushout.

 ‣ AddPushout( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation Pushout. $$F: ( (\beta_i: B \rightarrow I_i)_{i = 1 \dots n} ) \mapsto I$$

 ‣ AddInjectionOfCofactorOfPushout( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InjectionOfCofactorOfPushout. $$F: ( (\beta_i: B \rightarrow I_i)_{i = 1 \dots n}, k ) \mapsto \iota_k$$

 ‣ AddInjectionOfCofactorOfPushoutWithGivenPushout( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InjectionOfCofactorOfPushoutWithGivenPushout. $$F: ( (\beta_i: B \rightarrow I_i)_{i = 1 \dots n}, k, I ) \mapsto \iota_k$$

 ‣ AddUniversalMorphismFromPushout( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromPushout. $$F: ( (\beta_i: B \rightarrow I_i)_{i = 1 \dots n}, \tau ) \mapsto u(\tau)$$

 ‣ AddUniversalMorphismFromPushoutWithGivenPushout( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromPushout. $$F: ( (\beta_i: B \rightarrow I_i)_{i = 1 \dots n}, \tau, I ) \mapsto u(\tau)$$

##### 6.12-33 PushoutFunctorial
 ‣ PushoutFunctorial( L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{Pushout}( ( \beta_i )_{i=1}^n ), \mathrm{Pushout}( ( \beta_i' )_{i=1}^n ))$$

The argument is a list $$L = ( ( \beta_i: B \rightarrow I_i, \mu_i: I_i \rightarrow I_i', \beta_i': B' \rightarrow I_i' )_{i = 1 \dots n} )$$ such that there exists a morphism $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \beta \sim_{B, I_i'} \mu_i \circ \beta_i$$ for $$i = 1, \dots n$$. The output is the morphism $$\mathrm{Pushout}( ( \beta_i )_{i=1}^n ) \rightarrow \mathrm{Pushout}( ( \beta_i' )_{i=1}^n )$$ given by the functoriality of the pushout.

##### 6.12-34 PushoutFunctorialWithGivenPushouts
 ‣ PushoutFunctorialWithGivenPushouts( s, L, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(s, r)$$

The arguments are an object $$s = \mathrm{Pushout}( ( \beta_i )_{i=1}^n )$$, a list $$L = ( ( \beta_i: B \rightarrow I_i, \mu_i: I_i \rightarrow I_i', \beta_i': B' \rightarrow I_i' )_{i = 1 \dots n} )$$ such that there exists a morphism $$\beta: B \rightarrow B'$$ such that $$\beta_i' \circ \beta \sim_{B, I_i'} \mu_i \circ \beta_i$$ for $$i = 1, \dots n$$, and an object $$r = \mathrm{Pushout}( ( \beta_i' )_{i=1}^n )$$. The output is the morphism $$s \rightarrow r$$ given by the functoriality of the pushout.

 ‣ AddPushoutFunctorialWithGivenPushouts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation PushoutFunctorial. $$F: ( \mathrm{Pushout}( ( \beta_i )_{i=1}^n ), ( \beta_i: B \rightarrow I_i, \mu_i: I_i \rightarrow I_i', \beta_i': B' \rightarrow I_i' )_{i = 1 \dots n}, \mathrm{Pushout}( ( \beta_i' )_{i=1}^n ) ) \mapsto (\mathrm{Pushout}( ( \beta_i )_{i=1}^n ) \rightarrow \mathrm{Pushout}( ( \beta_i' )_{i=1}^n ) )$$

#### 6.13 Image

For a given morphism $$\alpha: A \rightarrow B$$, an image of $$\alpha$$ consists of four parts:

• an object $$I$$,

• a morphism $$c: A \rightarrow I$$,

• a monomorphism $$\iota: I \hookrightarrow B$$ such that $$\iota \circ c \sim_{A,B} \alpha$$,

• a dependent function $$u$$ mapping each pair of morphisms $$\tau = ( \tau_1: A \rightarrow T, \tau_2: T \hookrightarrow B )$$ where $$\tau_2$$ is a monomorphism such that $$\tau_2 \circ \tau_1 \sim_{A,B} \alpha$$ to a morphism $$u(\tau): I \rightarrow T$$ such that $$\tau_2 \circ u(\tau) \sim_{I,B} \iota$$ and $$u(\tau) \circ c \sim_{A,T} \tau_1$$.

The $$4$$-tuple $$( I, c, \iota, u )$$ is called an image of $$\alpha$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$I$$ of such a $$4$$-tuple by $$\mathrm{im}(\alpha)$$. We say that the morphism $$u( \tau )$$ is induced by the universal property of the image.

##### 6.13-1 IsomorphismFromImageObjectToKernelOfCokernel
 ‣ IsomorphismFromImageObjectToKernelOfCokernel( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{im}(\alpha), \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ) )$$

The argument is a morphism $$\alpha$$. The output is the canonical morphism $$\mathrm{im}(\alpha) \rightarrow \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) )$$.

 ‣ AddIsomorphismFromImageObjectToKernelOfCokernel( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromImageObjectToKernelOfCokernel. $$F: \alpha \mapsto ( \mathrm{im}(\alpha) \rightarrow \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ) )$$

##### 6.13-3 IsomorphismFromKernelOfCokernelToImageObject
 ‣ IsomorphismFromKernelOfCokernelToImageObject( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ), \mathrm{im}(\alpha) )$$

The argument is a morphism $$\alpha$$. The output is the canonical morphism $$\mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ) \rightarrow \mathrm{im}(\alpha)$$.

 ‣ AddIsomorphismFromKernelOfCokernelToImageObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromKernelOfCokernelToImageObject. $$F: \alpha \mapsto ( \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ) \rightarrow \mathrm{im}(\alpha) )$$

##### 6.13-5 ImageObject
 ‣ ImageObject( alpha ) ( attribute )

Returns: an object

The argument is a morphism $$\alpha$$. The output is the image $$\mathrm{im}( \alpha )$$.

##### 6.13-6 ImageEmbedding
 ‣ ImageEmbedding( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{im}(\alpha), B)$$

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the image embedding $$\iota: \mathrm{im}(\alpha) \hookrightarrow B$$.

##### 6.13-7 ImageEmbeddingWithGivenImageObject
 ‣ ImageEmbeddingWithGivenImageObject( alpha, I ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(I, B)$$

The argument is a morphism $$\alpha: A \rightarrow B$$ and an object $$I = \mathrm{im}( \alpha )$$. The output is the image embedding $$\iota: I \hookrightarrow B$$.

##### 6.13-8 CoastrictionToImage
 ‣ CoastrictionToImage( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(A, \mathrm{im}( \alpha ))$$

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the coastriction to image $$c: A \rightarrow \mathrm{im}( \alpha )$$.

##### 6.13-9 CoastrictionToImageWithGivenImageObject
 ‣ CoastrictionToImageWithGivenImageObject( alpha, I ) ( operation )

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

The argument is a morphism $$\alpha: A \rightarrow B$$ and an object $$I = \mathrm{im}( \alpha )$$. The output is the coastriction to image $$c: A \rightarrow I$$.

##### 6.13-10 UniversalMorphismFromImage
 ‣ UniversalMorphismFromImage( alpha, tau ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{im}(\alpha), T)$$

The arguments are a morphism $$\alpha: A \rightarrow B$$ and a pair of morphisms $$\tau = ( \tau_1: A \rightarrow T, \tau_2: T \hookrightarrow B )$$ where $$\tau_2$$ is a monomorphism such that $$\tau_2 \circ \tau_1 \sim_{A,B} \alpha$$. The output is the morphism $$u(\tau): \mathrm{im}(\alpha) \rightarrow T$$ given by the universal property of the image.

##### 6.13-11 UniversalMorphismFromImageWithGivenImageObject
 ‣ UniversalMorphismFromImageWithGivenImageObject( alpha, tau, I ) ( operation )

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

The arguments are a morphism $$\alpha: A \rightarrow B$$, a pair of morphisms $$\tau = ( \tau_1: A \rightarrow T, \tau_2: T \hookrightarrow B )$$ where $$\tau_2$$ is a monomorphism such that $$\tau_2 \circ \tau_1 \sim_{A,B} \alpha$$, and an object $$I = \mathrm{im}( \alpha )$$. The output is the morphism $$u(\tau): \mathrm{im}(\alpha) \rightarrow T$$ given by the universal property of the image.

 ‣ AddImageObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ImageObject. $$F: \alpha \mapsto I$$.

 ‣ AddImageEmbedding( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ImageEmbedding. $$F: \alpha \mapsto \iota$$.

 ‣ AddImageEmbeddingWithGivenImageObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation ImageEmbeddingWithGivenImageObject. $$F: (\alpha,I) \mapsto \iota$$.

 ‣ AddCoastrictionToImage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CoastrictionToImage. $$F: \alpha \mapsto c$$.

 ‣ AddCoastrictionToImageWithGivenImageObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CoastrictionToImageWithGivenImageObject. $$F: (\alpha,I) \mapsto c$$.

 ‣ AddUniversalMorphismFromImage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromImage. $$F: (\alpha, \tau) \mapsto u(\tau)$$.

 ‣ AddUniversalMorphismFromImageWithGivenImageObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismFromImageWithGivenImageObject. $$F: (\alpha, \tau, I) \mapsto u(\tau)$$.

#### 6.14 Coimage

For a given morphism $$\alpha: A \rightarrow B$$, a coimage of $$\alpha$$ consists of four parts:

• an object $$C$$,

• an epimorphism $$\pi: A \twoheadrightarrow C$$,

• a morphism $$a: C \rightarrow B$$ such that $$a \circ \pi \sim_{A,B} \alpha$$,

• a dependent function $$u$$ mapping each pair of morphisms $$\tau = ( \tau_1: A \twoheadrightarrow T, \tau_2: T \rightarrow B )$$ where $$\tau_1$$ is an epimorphism such that $$\tau_2 \circ \tau_1 \sim_{A,B} \alpha$$ to a morphism $$u(\tau): T \rightarrow C$$ such that $$u( \tau ) \circ \tau_1 \sim_{A,C} \pi$$ and $$a \circ u( \tau ) \sim_{T,B} \tau_2$$.

The $$4$$-tuple $$( C, \pi, a, u )$$ is called a coimage of $$\alpha$$ if the morphisms $$u( \tau )$$ are uniquely determined up to congruence of morphisms. We denote the object $$C$$ of such a $$4$$-tuple by $$\mathrm{coim}(\alpha)$$. We say that the morphism $$u( \tau )$$ is induced by the universal property of the coimage.

##### 6.14-1 MorphismFromCoimageToImage
 ‣ MorphismFromCoimageToImage( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{coim}(\alpha), \mathrm{im}(\alpha))$$

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the canonical morphism (in a preabelian category) $$\mathrm{coim}(\alpha) \rightarrow \mathrm{im}(\alpha)$$.

##### 6.14-2 MorphismFromCoimageToImageWithGivenObjects
 ‣ MorphismFromCoimageToImageWithGivenObjects( alpha ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(C,I)$$

The argument is an object $$C = \mathrm{coim}(\alpha)$$, a morphism $$\alpha: A \rightarrow B$$, and an object $$I = \mathrm{im}(\alpha)$$. The output is the canonical morphism (in a preabelian category) $$C \rightarrow I$$.

 ‣ AddMorphismFromCoimageToImageWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MorphismFromCoimageToImageWithGivenObjects. $$F: (C, \alpha, I) \mapsto ( C \rightarrow I )$$.

##### 6.14-4 InverseMorphismFromCoimageToImage
 ‣ InverseMorphismFromCoimageToImage( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{im}(\alpha), \mathrm{coim}(\alpha))$$

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the inverse of the canonical morphism (in an abelian category) $$\mathrm{im}(\alpha) \rightarrow \mathrm{coim}(\alpha)$$.

##### 6.14-5 InverseMorphismFromCoimageToImageWithGivenObjects
 ‣ InverseMorphismFromCoimageToImageWithGivenObjects( alpha ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(I,C)$$

The argument is an object $$C = \mathrm{coim}(\alpha)$$, a morphism $$\alpha: A \rightarrow B$$, and an object $$I = \mathrm{im}(\alpha)$$. The output is the inverse of the canonical morphism (in an abelian category) $$I \rightarrow C$$.

 ‣ AddInverseMorphismFromCoimageToImageWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MorphismFromCoimageToImageWithGivenObjects. $$F: (C, \alpha, I) \mapsto ( I \rightarrow C )$$.

##### 6.14-7 IsomorphismFromCoimageToCokernelOfKernel
 ‣ IsomorphismFromCoimageToCokernelOfKernel( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{coim}( \alpha ), \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ) )$$.

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the canonical morphism $$\mathrm{coim}( \alpha ) \rightarrow \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) )$$.

 ‣ AddIsomorphismFromCoimageToCokernelOfKernel( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromCoimageToCokernelOfKernel. $$F: \alpha \mapsto ( \mathrm{coim}( \alpha ) \rightarrow \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ) )$$.

##### 6.14-9 IsomorphismFromCokernelOfKernelToCoimage
 ‣ IsomorphismFromCokernelOfKernelToCoimage( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ), \mathrm{coim}( \alpha ) )$$.

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the canonical morphism $$\mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ) \rightarrow \mathrm{coim}( \alpha )$$.

 ‣ AddIsomorphismFromCokernelOfKernelToCoimage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromCokernelOfKernelToCoimage. $$F: \alpha \mapsto ( \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ) \rightarrow \mathrm{coim}( \alpha ) )$$.

##### 6.14-11 Coimage
 ‣ Coimage( alpha ) ( attribute )

Returns: an object

The argument is a morphism $$\alpha$$. The output is the coimage $$\mathrm{coim}( \alpha )$$.

##### 6.14-12 CoimageProjection
 ‣ CoimageProjection( C ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(A, C)$$

This is a convenience method. The argument is an object $$C$$ which was created as a coimage of a morphism $$\alpha: A \rightarrow B$$. The output is the coimage projection $$\pi: A \twoheadrightarrow C$$.

##### 6.14-13 CoimageProjection
 ‣ CoimageProjection( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(A, \mathrm{coim}( \alpha ))$$

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the coimage projection $$\pi: A \twoheadrightarrow \mathrm{coim}( \alpha )$$.

##### 6.14-14 CoimageProjectionWithGivenCoimage
 ‣ CoimageProjectionWithGivenCoimage( alpha, C ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(A, C)$$

The arguments are a morphism $$\alpha: A \rightarrow B$$ and an object $$C = \mathrm{coim}(\alpha)$$. The output is the coimage projection $$\pi: A \twoheadrightarrow C$$.

##### 6.14-15 AstrictionToCoimage
 ‣ AstrictionToCoimage( C ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(C,B)$$

This is a convenience method. The argument is an object $$C$$ which was created as a coimage of a morphism $$\alpha: A \rightarrow B$$. The output is the astriction to coimage $$a: C \rightarrow B$$.

##### 6.14-16 AstrictionToCoimage
 ‣ AstrictionToCoimage( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{coim}( \alpha ),B)$$

The argument is a morphism $$\alpha: A \rightarrow B$$. The output is the astriction to coimage $$a: \mathrm{coim}( \alpha ) \rightarrow B$$.

##### 6.14-17 AstrictionToCoimageWithGivenCoimage
 ‣ AstrictionToCoimageWithGivenCoimage( alpha, C ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(C,B)$$

The argument are a morphism $$\alpha: A \rightarrow B$$ and an object $$C = \mathrm{coim}( \alpha )$$. The output is the astriction to coimage $$a: C \rightarrow B$$.

##### 6.14-18 UniversalMorphismIntoCoimage
 ‣ UniversalMorphismIntoCoimage( alpha, tau ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(T, \mathrm{coim}( \alpha ))$$

The arguments are a morphism $$\alpha: A \rightarrow B$$ and a pair of morphisms $$\tau = ( \tau_1: A \twoheadrightarrow T, \tau_2: T \rightarrow B )$$ where $$\tau_1$$ is an epimorphism such that $$\tau_2 \circ \tau_1 \sim_{A,B} \alpha$$. The output is the morphism $$u(\tau): T \rightarrow \mathrm{coim}( \alpha )$$ given by the universal property of the coimage.

##### 6.14-19 UniversalMorphismIntoCoimageWithGivenCoimage
 ‣ UniversalMorphismIntoCoimageWithGivenCoimage( alpha, tau, C ) ( operation )

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

The arguments are a morphism $$\alpha: A \rightarrow B$$, a pair of morphisms $$\tau = ( \tau_1: A \twoheadrightarrow T, \tau_2: T \rightarrow B )$$ where $$\tau_1$$ is an epimorphism such that $$\tau_2 \circ \tau_1 \sim_{A,B} \alpha$$, and an object $$C = \mathrm{coim}( \alpha )$$. The output is the morphism $$u(\tau): T \rightarrow C$$ given by the universal property of the coimage.

 ‣ AddCoimage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation Coimage. $$F: \alpha \mapsto C$$

 ‣ AddCoimageProjection( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CoimageProjection. $$F: \alpha \mapsto \pi$$

 ‣ AddCoimageProjectionWithGivenCoimage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CoimageProjectionWithGivenCoimage. $$F: (\alpha,C) \mapsto \pi$$

 ‣ AddAstrictionToCoimage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation AstrictionToCoimage. $$F: \alpha \mapsto a$$

 ‣ AddAstrictionToCoimageWithGivenCoimage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation AstrictionToCoimageWithGivenCoimage. $$F: (\alpha,C) \mapsto a$$

 ‣ AddUniversalMorphismIntoCoimage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoCoimage. $$F: (\alpha, \tau) \mapsto u(\tau)$$

 ‣ AddUniversalMorphismIntoCoimageWithGivenCoimage( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalMorphismIntoCoimageWithGivenCoimage. $$F: (\alpha, \tau,C) \mapsto u(\tau)$$

#### 6.15 Subobject Classifier

A subobject classifier object 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.

##### 6.15-1 SubobjectClassifier
 ‣ SubobjectClassifier( C ) ( attribute )

Returns: an object

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

##### 6.15-2 SubobjectClassifier
 ‣ SubobjectClassifier( c ) ( attribute )

Returns: an object

This is a convenience method. The argument is a cell $$c$$. The output is a subobject classifier $$\Omega$$ of the category $$C$$ for which $$c \in C$$.

##### 6.15-3 TruthMorphismIntoSubobjectClassifierWithGivenObjects
 ‣ TruthMorphismIntoSubobjectClassifierWithGivenObjects( T, W ) ( operation )

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

The arguments are a terminal object of the category and a subobject classifier. The output is the truth morphism to the subobject classifier $$\mathrm{true}: \mathrm{TerminalObject} \rightarrow \mathrm{SubobjectClassifier}$$.

##### 6.15-4 TruthMorphismIntoSubobjectClassifier
 ‣ TruthMorphismIntoSubobjectClassifier( C ) ( operation )

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

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

##### 6.15-5 TruthMorphismIntoSubobjectClassifier
 ‣ TruthMorphismIntoSubobjectClassifier( c ) ( operation )

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

This is a convenience method. The argument is a cell $$c$$. The output is the truth morphism to the subobject classifier $$\mathrm{true}: \mathrm{TerminalObject} \rightarrow \mathrm{SubobjectClassifier}$$ of the category $$C$$ for which $$c \in C$$.

##### 6.15-6 ClassifyingMorphismOfSubobject
 ‣ ClassifyingMorphismOfSubobject( m ) ( operation )

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

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

##### 6.15-7 ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier
 ‣ ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier( m, omega ) ( operation )

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

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

##### 6.15-8 SubobjectOfClassifyingMorphism
 ‣ SubobjectOfClassifyingMorphism( chi ) ( operation )

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

 ‣ AddSubobjectClassifier( C, F ) ( operation )

Returns: nothing

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

 ‣ 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 : m \mapsto \mathrm{ClassifyingMorphism}(m)$$.

 ‣ 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 : (m, \Omega) \mapsto \mathrm{ClassifyingMorphism}(m)$$.

 ‣ AddTruthMorphismIntoSubobjectClassifierWithGivenObjects( 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 TruthMorphismIntoSubobjectClassifierWithGivenObjects. $$F : (1, \Omega) \mapsto \mathrm{true}$$.

 ‣ AddSubobjectOfClassifyingMorphism( C, F ) ( operation )
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 : m \mapsto \mathrm{SubobjectOfClassifyingMorphism}(m)$$.