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' )\).
‣ KernelObject( alpha ) | ( attribute ) |
Returns: an object
The argument is a morphism \(\alpha\). The output is the kernel \(K\) of \(\alpha\).
‣ 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\).
‣ 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\).
‣ 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.
‣ 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\).
‣ 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 functorality of the kernel.
‣ 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 functorality of the kernel.
‣ 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 functorality 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' ))\).
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' )\).
‣ CokernelObject( alpha ) | ( attribute ) |
Returns: an object
The argument is a morphism \(\alpha: A \rightarrow B\). The output is the cokernel \(K\) of \(\alpha\).
‣ 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 )\).
‣ 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 )\).
‣ 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.
‣ 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)\).
‣ 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 functorality of the cokernel.
‣ 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 functorality of the cokernel.
‣ 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 functorality 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' ))\).
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.
‣ ZeroObject( C ) | ( attribute ) |
Returns: an object
The argument is a category \(C\). The output is a zero object \(Z\) of \(C\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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}\).
‣ 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\).
‣ 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}\).
‣ 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}\).
‣ 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}\).
‣ 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})\).
‣ 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)\).
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\).
‣ TerminalObject( C ) | ( attribute ) |
Returns: an object
The argument is a category \(C\). The output is a terminal object \(T\) of \(C\).
‣ 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\).
‣ 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}\).
‣ 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)\).
‣ 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)\).
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\).
‣ InitialObject( C ) | ( attribute ) |
Returns: an object
The argument is a category \(C\). The output is an initial object \(I\) of \(C\).
‣ 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\).
‣ 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\).
‣ 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)\).
‣ 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 )\).
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 = \mathrm{id}_S\),
\(\pi_j \circ \iota_i = \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'\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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.
‣ 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.
‣ 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.
‣ 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.
‣ 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.
‣ 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.
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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.
‣ 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\).
‣ 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\).
‣ 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 functorality of the direct sum.
‣ 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 functorality 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')\).
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'\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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.
‣ 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.
‣ 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 )\).
‣ 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 functorality of the coproduct.
‣ 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 functorality 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')\).
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'\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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.
‣ 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.
‣ 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 )\)
‣ 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 functorality of the direct product.
‣ 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 functorality 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')\)
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' )\).
‣ 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\).
‣ 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\)
‣ 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\).
‣ 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)\)
‣ 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\).
‣ 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)\)
‣ 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\).
‣ 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\)
‣ 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)\).
‣ 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)\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ UniversalMorphismIntoFiberProduct( arg ) | ( function ) |
This is a convenience method. There are three 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.
‣ 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.
‣ 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)\)
‣ 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 functorality of the fiber product.
‣ 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 functorality 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} ) )\)
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' )\).
‣ 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\).
‣ 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)\)
‣ 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\).
‣ 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))\)
‣ 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\).
‣ 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)\)
‣ 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)\).
‣ 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))\)
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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 )\).
‣ 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 )\).
‣ 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 )\).
‣ UniversalMorphismFromPushout( arg ) | ( function ) |
This is a convenience method. There are three 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.
‣ 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.
‣ 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)\)
‣ 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 functorality of the pushout.
‣ 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 functorality 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 ) )\)
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.
‣ 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 ) ) )\)
‣ 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) )\)
‣ ImageObject( alpha ) | ( attribute ) |
Returns: an object
The argument is a morphism \(\alpha\). The output is the image \(\mathrm{im}( \alpha )\).
‣ 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\).
‣ 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\).
‣ 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 )\).
‣ 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\).
‣ 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.
‣ 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)\).
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.
‣ 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)\).
‣ 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 )\).
‣ 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)\).
‣ 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 )\).
‣ 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 ) ) )\).
‣ 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 ) )\).
‣ Coimage( alpha ) | ( attribute ) |
Returns: an object
The argument is a morphism \(\alpha\). The output is the coimage \(\mathrm{coim}( \alpha )\).
‣ 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\).
‣ 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 )\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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.
‣ 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)\)
generated by GAPDoc2HTML