Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/GAP/pkg/cap/doc/   (Algebra von RWTH Aachen Version 4.15.1©)  Datei vom 22.8.2025 mit Größe 212 kB image not shown  

SSL chap6.html

  Interaktion und
PortierbarkeitHTML 		 

 products/Sources/formale Sprachen/GAP/pkg/cap/doc/chap6.html


<?xml version="1.0" encoding="UTF-8"?>

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
         "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">

<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en">
<head>
<title>GAP (CAP) - Chapter 6: Universal Objects</title>
<meta http-equiv="content-type" content="text/html; charset=UTF-8" />
<meta name="generator" content="GAPDoc2HTML" />
<link rel="stylesheet" type="text/css" href="manual.css" />
<script src="manual.js" type="text/javascript"></script>
<script type="text/javascript">overwriteStyle();</script>
</head>
<body class="chap6"  onload="jscontent()">


<div class="chlinktop"><span class="chlink1">Goto Chapter: </span><a href="chap0.html">Top</a>  <a href="chap1.html">1</a>  <a href="chap2.html">2</a>  <a href="chap3.html">3</a>  <a href="chap4.html">4</a>  <a href="chap5.html">5</a>  <a href="chap6.html">6</a>  <a href="chap7.html">7</a>  <a href="chap8.html">8</a>  <a href="chap9.html">9</a>  <a href="chap10.html">10</a>  <a href="chap11.html">11</a>  <a href="chap12.html">12</a>  <a href="chap13.html">13</a>  <a href="chap14.html">14</a>  <a href="chap15.html">15</a>  <a href="chap16.html">16</a>  <a href="chap17.html">17</a>  <a href="chap18.html">18</a>  <a href="chapInd.html">Ind</a>  </div>

<div class="chlinkprevnexttop"> <a href="chap0.html">[Top of Book]</a>   <a href="chap0.html#contents">[Contents]</a>    <a href="chap5.html">[Previous Chapter]</a>    <a href="chap7.html">[Next Chapter]</a>   </div>

<p id="mathjaxlink" class="pcenter"><a href="chap6_mj.html">[MathJax on]</a></p>
<p><a id="X7994CC1487D7617C" name="X7994CC1487D7617C"></a></p>
<div class="ChapSects"><a href="chap6.html#X7994CC1487D7617C">6 <span class="Heading">Universal Objects</span></a>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X7DCD99628504B810">6.1 <span class="Heading">Kernel</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82EAD3357C9FE4C8">6.1-1 KernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8430666980D732FB">6.1-2 KernelEmbedding</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7CBE1D0C84F5A47E">6.1-3 KernelEmbeddingWithGivenKernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78140AF884DE0736">6.1-4 MorphismFromKernelObjectToSink</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7BF5A3A57E23C795">6.1-5 MorphismFromKernelObjectToSinkWithGivenKernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X87920AC67A5802BC">6.1-6 KernelLift</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X83D439A07AD29D05">6.1-7 KernelLiftWithGivenKernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78D5B94A7EF4D4F0">6.1-8 KernelObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X787AE8F07F7A062C">6.1-9 KernelObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7F61FE0B82AF4CDB">6.1-10 KernelObjectFunctorialWithGivenKernelObjects</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7A17922D869CCEB5">6.1-11 KernelObjectFunctorialWithGivenKernelObjects</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X875F177A82BF9B8B">6.2 <span class="Heading">Cokernel</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82803DBC80F40EFC">6.2-1 CokernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78948D7A7B52AB31">6.2-2 CokernelProjection</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X845DC9377A05BE7B">6.2-3 CokernelProjectionWithGivenCokernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X872E26C57F195D50">6.2-4 MorphismFromSourceToCokernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X876648527E75AA04">6.2-5 MorphismFromSourceToCokernelObjectWithGivenCokernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8735262382CE2560">6.2-6 CokernelColift</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X86DB5CD27C0EB7D2">6.2-7 CokernelColiftWithGivenCokernelObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78E421227FB90A70">6.2-8 CokernelObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X837889ED7BD6CBED">6.2-9 CokernelObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7BA172F07A431626">6.2-10 CokernelObjectFunctorialWithGivenCokernelObjects</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7F59A455873709D3">6.2-11 CokernelObjectFunctorialWithGivenCokernelObjects</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X797A74DE8267C974">6.3 <span class="Heading">Zero Object</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X790C4FA87CADB93E">6.3-1 ZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X87D87A177FE0542F">6.3-2 ZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7A0BF1118777C8A3">6.3-3 UniversalMorphismFromZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X80327B2387F38FE8">6.3-4 UniversalMorphismFromZeroObjectWithGivenZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X86003308844F8341">6.3-5 UniversalMorphismIntoZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X866104CA84CBC40A">6.3-6 UniversalMorphismIntoZeroObjectWithGivenZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7F701A11812C74C5">6.3-7 MorphismFromZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X837BD808791003FF">6.3-8 MorphismIntoZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8711ABE9811C7CCF">6.3-9 IsomorphismFromZeroObjectToInitialObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X86FF82B284B8E2EB">6.3-10 IsomorphismFromInitialObjectToZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78C501A179BB6CBB">6.3-11 IsomorphismFromZeroObjectToTerminalObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X83E84FC187EE2445">6.3-12 IsomorphismFromTerminalObjectToZeroObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X79CEAF827DDED44B">6.3-13 ZeroObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82D7BF1F85268B0A">6.3-14 ZeroObjectFunctorialWithGivenZeroObjects</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X827CD17C7EBFD58F">6.4 <span class="Heading">Terminal Object</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7DC837217946D22D">6.4-1 TerminalObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7D86D2EA7845AEEB">6.4-2 TerminalObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7BEA5AF67D63F4A5">6.4-3 UniversalMorphismIntoTerminalObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8707AD1784DCBBFF">6.4-4 UniversalMorphismIntoTerminalObjectWithGivenTerminalObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7C616CD287760D2F">6.4-5 TerminalObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8511229882130F93">6.4-6 TerminalObjectFunctorialWithGivenTerminalObjects</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X78B0ED8B80BF5254">6.5 <span class="Heading">Initial Object</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7A70384E7F182B00">6.5-1 InitialObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E17CDF481C348B9">6.5-2 InitialObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X873FC2B087004DC3">6.5-3 UniversalMorphismFromInitialObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7F7177F585576F6B">6.5-4 UniversalMorphismFromInitialObjectWithGivenInitialObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X87B1C71179F798C8">6.5-5 InitialObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7CE9BBC27F70F3BD">6.5-6 InitialObjectFunctorialWithGivenInitialObjects</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X81FDB99378D1307A">6.6 <span class="Heading">Direct Sum</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82AD6F187B550060">6.6-1 DirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7BC1F4728357D708">6.6-2 DirectSumOp</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78E4506F7BBA7A9A">6.6-3 ProjectionInFactorOfDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X832F2E577B7B70BB">6.6-4 ProjectionInFactorOfDirectSumWithGivenDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X842743E97E2F28CD">6.6-5 InjectionOfCofactorOfDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X876493497F824480">6.6-6 InjectionOfCofactorOfDirectSumWithGivenDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X84FCF65E798EBF7B">6.6-7 UniversalMorphismIntoDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X79EFDADB8276B639">6.6-8 UniversalMorphismIntoDirectSumWithGivenDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X812D12CF7AB6F499">6.6-9 UniversalMorphismFromDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7B64A051814EFDDB">6.6-10 UniversalMorphismFromDirectSumWithGivenDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7AB9D34882B5EDDF">6.6-11 IsomorphismFromDirectSumToDirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E87C9257A1BFFEE">6.6-12 IsomorphismFromDirectProductToDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X85599FEC812FD591">6.6-13 IsomorphismFromDirectSumToCoproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7CACFBCA7B9A4E19">6.6-14 IsomorphismFromCoproductToDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X847C8B7E8646DF61">6.6-15 MorphismBetweenDirectSums</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7FDE63F78410A822">6.6-16 MorphismBetweenDirectSums</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E020D2783A62178">6.6-17 MorphismBetweenDirectSumsWithGivenDirectSums</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7A3400D485D0C438">6.6-18 ComponentOfMorphismIntoDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7B71C4F4799263E6">6.6-19 ComponentOfMorphismFromDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X784D53A47F683192">6.6-20 DirectSumFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78B24593868483EE">6.6-21 DirectSumFunctorialWithGivenDirectSums</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X7E8036DF7AC65994">6.7 <span class="Heading">Coproduct</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X872D3F297979C7B8">6.7-1 Coproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E3C6A0482E8CAB5">6.7-2 Coproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82FCE4657D132584">6.7-3 Coproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82D87B52862BB55C">6.7-4 InjectionOfCofactorOfCoproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X83687CD9789CAB9C">6.7-5 InjectionOfCofactorOfCoproductWithGivenCoproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7D002C7B82B26908">6.7-6 UniversalMorphismFromCoproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X85F392E5865012C7">6.7-7 UniversalMorphismFromCoproductWithGivenCoproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7FDE92577EFB6866">6.7-8 CoproductFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X85FFAD9E7FAFF9D4">6.7-9 CoproductFunctorialWithGivenCoproducts</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82F0CBC179945B84">6.7-10 ComponentOfMorphismFromCoproduct</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X844C65417FBEA3C7">6.8 <span class="Heading">Direct Product</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X861BA02C7902A4F4">6.8-1 DirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7AEF0CD1812F7EC8">6.8-2 DirectProductOp</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7FFBE9EC7BEE7673">6.8-3 ProjectionInFactorOfDirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8288ABA984EF9DED">6.8-4 ProjectionInFactorOfDirectProductWithGivenDirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X872189E4848F6863">6.8-5 UniversalMorphismIntoDirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X81A27DC180D751B8">6.8-6 UniversalMorphismIntoDirectProductWithGivenDirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X79EB76507C8AB4A4">6.8-7 DirectProductFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7DD930FE78492D58">6.8-8 DirectProductFunctorialWithGivenDirectProducts</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7C5769577CEAF2C4">6.8-9 ComponentOfMorphismIntoDirectProduct</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X824FD8F786D2350D">6.9 <span class="Heading">Equalizer</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X824FD8F786D2350D">6.9-1 Equalizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7B1937088320E680">6.9-2 EqualizerOp</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X803E62B382D76E4F">6.9-3 EmbeddingOfEqualizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X828423F283DF97BA">6.9-4 EmbeddingOfEqualizerWithGivenEqualizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78A6E6AA87FADB13">6.9-5 MorphismFromEqualizerToSink</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7CF04F98844789DE">6.9-6 MorphismFromEqualizerToSinkWithGivenEqualizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X872F9E2E853EB91D">6.9-7 UniversalMorphismIntoEqualizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7F7191B57D8AA456">6.9-8 UniversalMorphismIntoEqualizerWithGivenEqualizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82400CA57F0E5585">6.9-9 EqualizerFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7804D05C7EFDC5CE">6.9-10 EqualizerFunctorialWithGivenEqualizers</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7DD2167B7836DF62">6.9-11 JointPairwiseDifferencesOfMorphismsIntoDirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E8843F17F0F3D14">6.9-12 IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7A96B57382715059">6.9-13 IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X7BA8F7BD793CC288">6.10 <span class="Heading">Coequalizer</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7BA8F7BD793CC288">6.10-1 Coequalizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X80FCD6BE84781FE6">6.10-2 CoequalizerOp</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E0468077DE9EC3B">6.10-3 ProjectionOntoCoequalizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78B7474384BAA57A">6.10-4 ProjectionOntoCoequalizerWithGivenCoequalizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7D3F328F82CD8A49">6.10-5 MorphismFromSourceToCoequalizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82EB657782E82115">6.10-6 MorphismFromSourceToCoequalizerWithGivenCoequalizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X86EFF737796C2630">6.10-7 UniversalMorphismFromCoequalizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X816990198092E8B6">6.10-8 UniversalMorphismFromCoequalizerWithGivenCoequalizer</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X818C5AD2794A2C7B">6.10-9 CoequalizerFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7CB3323C7B44B75F">6.10-10 CoequalizerFunctorialWithGivenCoequalizers</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7AE156547D6F06CE">6.10-11 JointPairwiseDifferencesOfMorphismsFromCoproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X80AFEE3579EB987A">6.10-12 IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78A3F1087B86E650">6.10-13 IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X8038824E84B571F8">6.11 <span class="Heading">Fiber Product (= Pullback)</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7DAB395584678429">6.11-1 IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8190FBB47DB6307D">6.11-2 IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82157EF887CC99D1">6.11-3 FiberProductEmbeddingInDirectProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7919AF7486FA42C5">6.11-4 FiberProductEmbeddingInDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7DE20941803BFBD9">6.11-5 FiberProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8000EEB77D6E8B7C">6.11-6 FiberProductOp</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8104B3717D3B646F">6.11-7 ProjectionInFactorOfFiberProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8085606A7B09071F">6.11-8 ProjectionInFactorOfFiberProductWithGivenFiberProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7C6EF50085D13D12">6.11-9 MorphismFromFiberProductToSink</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X866ED61786F4C76C">6.11-10 MorphismFromFiberProductToSinkWithGivenFiberProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8441CF7F8140E8C2">6.11-11 UniversalMorphismIntoFiberProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7A6A890D85F01977">6.11-12 UniversalMorphismIntoFiberProductWithGivenFiberProduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X791F33AB7EAF6A2A">6.11-13 FiberProductFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X83A9F01A82894F65">6.11-14 FiberProductFunctorialWithGivenFiberProducts</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X81A2D49D85923894">6.12 <span class="Heading">Pushout</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X87C495A782BE3433">6.12-1 IsomorphismFromPushoutToCoequalizerOfCoproductDiagram</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7EAFDD727D94E932">6.12-2 IsomorphismFromCoequalizerOfCoproductDiagramToPushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E718F228767638A">6.12-3 PushoutProjectionFromCoproduct</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X837467847F63FE1B">6.12-4 PushoutProjectionFromDirectSum</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78E10D9E849FE214">6.12-5 Pushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78D93A2883C83CAC">6.12-6 Pushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7CF12E527805752F">6.12-7 InjectionOfCofactorOfPushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E54DB957B5F9157">6.12-8 InjectionOfCofactorOfPushoutWithGivenPushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X84B182F882D1F039">6.12-9 MorphismFromSourceToPushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7D3DAF80816918A4">6.12-10 MorphismFromSourceToPushoutWithGivenPushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X84F299F47BFB39F8">6.12-11 UniversalMorphismFromPushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7E3C69767F1C3B30">6.12-12 UniversalMorphismFromPushoutWithGivenPushout</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X80494AF087F5DE4B">6.12-13 PushoutFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7DAF60808113D76B">6.12-14 PushoutFunctorialWithGivenPushouts</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X87F4D35A826599C6">6.13 <span class="Heading">Image</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X80490BD785CA695A">6.13-1 IsomorphismFromImageObjectToKernelOfCokernel</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7CAA3342865B456B">6.13-2 IsomorphismFromKernelOfCokernelToImageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X83B457FF79AC5AC6">6.13-3 ImageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X86CEE2D1876EC2B9">6.13-4 ImageEmbedding</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82991FA17B460744">6.13-5 ImageEmbeddingWithGivenImageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8144201987A27661">6.13-6 CoastrictionToImage</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78BE36EA83BEF493">6.13-7 CoastrictionToImageWithGivenImageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7989B1FB811D2033">6.13-8 UniversalMorphismFromImage</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X86E557097CFB4430">6.13-9 UniversalMorphismFromImageWithGivenImageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7A46647F7AA9C398">6.13-10 ImageObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X85F174A07A09B04C">6.13-11 ImageObjectFunctorialWithGivenImageObjects</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X7EB02EC487B586E5">6.14 <span class="Heading">Coimage</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7C594E227D8DB0ED">6.14-1 IsomorphismFromCoimageToCokernelOfKernel</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7CF7E7E47A460E56">6.14-2 IsomorphismFromCokernelOfKernelToCoimage</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X82318F9B876ACB1A">6.14-3 CoimageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X788E717C7CCC6645">6.14-4 CoimageProjection</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X836301DF80A22C5C">6.14-5 CoimageProjectionWithGivenCoimageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X805108BF8047357E">6.14-6 AstrictionToCoimage</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X78AC1C7384A60A5E">6.14-7 AstrictionToCoimageWithGivenCoimageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7D051DDF7A68BFFB">6.14-8 UniversalMorphismIntoCoimage</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X87AACC0083B6D49F">6.14-9 UniversalMorphismIntoCoimageWithGivenCoimageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X852EFBA87E7F6831">6.14-10 CoimageObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7FB58F087D65DB38">6.14-11 CoimageObjectFunctorialWithGivenCoimageObjects</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X8047F7C57B874495">6.15 <span class="Heading">Morphism between Coimage and Image</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7F7BD6A18581671E">6.15-1 MorphismFromCoimageToImage</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8025749B78E12A2B">6.15-2 MorphismFromCoimageToImageWithGivenObjects</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X86692249870B0EC6">6.15-3 InverseOfMorphismFromCoimageToImage</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7B32041F7C9427E4">6.15-4 InverseOfMorphismFromCoimageToImageWithGivenObjects</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X87F38F8284D3137C">6.16 <span class="Heading">Homology objects</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8713652D7B7E1418">6.16-1 HomologyObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8647C62283C9B921">6.16-2 HomologyObjectFunctorial</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X81012CC0845DE717">6.16-3 HomologyObjectFunctorialWithGivenHomologyObjects</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X8799E88E79EFE007">6.16-4 IsomorphismFromHomologyObjectToItsConstructionAsAnImageObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X828E94BA7CF6FB71">6.16-5 IsomorphismFromItsConstructionAsAnImageObjectToHomologyObject</a></span>
</div></div>
<div class="ContSect"><span class="tocline"><span class="nocss"> </span><a href="chap6.html#X81E4AE0B7876230B">6.17 <span class="Heading">Projective covers and injective envelopes</span></a>
</span>
<div class="ContSSBlock">
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X790C931979343CFF">6.17-1 ProjectiveCoverObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X851836CC829092D9">6.17-2 EpimorphismFromProjectiveCoverObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X7C9F2CC480C7DA1D">6.17-3 EpimorphismFromProjectiveCoverObjectWithGivenProjectiveCoverObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X791CA23A8401BF2F">6.17-4 InjectiveEnvelopeObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X879A01DD7DC8AB13">6.17-5 MonomorphismIntoInjectiveEnvelopeObject</a></span>
<span class="ContSS"><br /><span class="nocss">  </span><a href="chap6.html#X781E3ED78574B379">6.17-6 MonomorphismIntoInjectiveEnvelopeObjectWithGivenInjectiveEnvelopeObject</a></span>
</div></div>
</div>

<h3>6 <span class="Heading">Universal Objects</span></h3>

<p><a id="X7DCD99628504B810" name="X7DCD99628504B810"></a></p>

<h4>6.1 <span class="Heading">Kernel</span></h4>

<p>For a given morphism <span class="Math">\alpha: A \rightarrow B</span>, a kernel of <span class="Math">\alpha</span> consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">K</span>,</p>

</li>
<li><p>a morphism <span class="Math">\iota: K \rightarrow A</span> such that <span class="Math">\alpha \circ \iota \sim_{K,B} 0</span>,</p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each morphism <span class="Math">\tau: T \rightarrow A</span> satisfying <span class="Math">\alpha \circ \tau \sim_{T,B} 0</span> to a morphism <span class="Math">u(\tau): T \rightarrow K</span> such that <span class="Math">\iota \circ u( \tau ) \sim_{T,A} \tau</span>.</p>

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

<p><a id="X82EAD3357C9FE4C8" name="X82EAD3357C9FE4C8"></a></p>

<h5>6.1-1 KernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelObject</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a morphism <span class="Math">\alpha</span>. The output is the kernel <span class="Math">K</span> of <span class="Math">\alpha</span>.</p>

<p><a id="X8430666980D732FB" name="X8430666980D732FB"></a></p>

<h5>6.1-2 KernelEmbedding</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelEmbedding</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{KernelObject}(\alpha),A)</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the kernel embedding <span class="Math">\iota: \mathrm{KernelObject}(\alpha) \rightarrow A</span>.</p>

<p><a id="X7CBE1D0C84F5A47E" name="X7CBE1D0C84F5A47E"></a></p>

<h5>6.1-3 KernelEmbeddingWithGivenKernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelEmbeddingWithGivenKernelObject</code>( <var class="Arg">alpha</var>, <var class="Arg">K</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(K,A)</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow B</span> and an object <span class="Math">K = \mathrm{KernelObject}(\alpha)</span>. The output is the kernel embedding <span class="Math">\iota: K \rightarrow A</span>.</p>

<p><a id="X78140AF884DE0736" name="X78140AF884DE0736"></a></p>

<h5>6.1-4 MorphismFromKernelObjectToSink</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromKernelObjectToSink</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: the zero morphism in <span class="Math">\mathrm{Hom}( \mathrm{KernelObject}(\alpha), B )</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the zero morphism <span class="Math">0: \mathrm{KernelObject}(\alpha) \rightarrow B</span>.</p>

<p><a id="X7BF5A3A57E23C795" name="X7BF5A3A57E23C795"></a></p>

<h5>6.1-5 MorphismFromKernelObjectToSinkWithGivenKernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromKernelObjectToSinkWithGivenKernelObject</code>( <var class="Arg">alpha</var>, <var class="Arg">K</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: the zero morphism in <span class="Math">\mathrm{Hom}( K, B )</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow B</span> and an object <span class="Math">K = \mathrm{KernelObject}(\alpha)</span>. The output is the zero morphism <span class="Math">0: K \rightarrow B</span>.</p>

<p><a id="X87920AC67A5802BC" name="X87920AC67A5802BC"></a></p>

<h5>6.1-6 KernelLift</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelLift</code>( <var class="Arg">alpha</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(T,\mathrm{KernelObject}(\alpha))</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow B</span>, a test object <span class="Math">T</span>, and a test morphism <span class="Math">\tau: T \rightarrow A</span> satisfying <span class="Math">\alpha \circ \tau \sim_{T,B} 0</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u(\tau): T \rightarrow \mathrm{KernelObject}(\alpha)</span> given by the universal property of the kernel.</p>

<p><a id="X83D439A07AD29D05" name="X83D439A07AD29D05"></a></p>

<h5>6.1-7 KernelLiftWithGivenKernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelLiftWithGivenKernelObject</code>( <var class="Arg">alpha</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">K</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(T,K)</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow B</span>, a test object <span class="Math">T</span>, a test morphism <span class="Math">\tau: T \rightarrow A</span> satisfying <span class="Math">\alpha \circ \tau \sim_{T,B} 0</span>, and an object <span class="Math">K = \mathrm{KernelObject}(\alpha)</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u(\tau): T \rightarrow K</span> given by the universal property of the kernel.</p>

<p><a id="X78D5B94A7EF4D4F0" name="X78D5B94A7EF4D4F0"></a></p>

<h5>6.1-8 KernelObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelObjectFunctorial</code>( <var class="Arg">L</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{KernelObject}( \alpha ), \mathrm{KernelObject}( \alpha' ) )</span></p>

<p>The argument is a list <span class="Math">L = [ \alpha: A \rightarrow B, [ \mu: A \rightarrow A', \nu: B \rightarrow B' ], \alpha': A' \rightarrow B' ]</span> of morphisms. The output is the morphism <span class="Math">\mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' )</span> given by the functoriality of the kernel.</p>

<p><a id="X787AE8F07F7A062C" name="X787AE8F07F7A062C"></a></p>

<h5>6.1-9 KernelObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelObjectFunctorial</code>( <var class="Arg">alpha</var>, <var class="Arg">mu</var>, <var class="Arg">alpha_prime</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{KernelObject}( \alpha ), \mathrm{KernelObject}( \alpha' ) )</span></p>

<p>The arguments are three morphisms <span class="Math">\alpha: A \rightarrow B</span>, <span class="Math">\mu: A \rightarrow A'</span>, <span class="Math">\alpha': A' \rightarrow B'</span>. The output is the morphism <span class="Math">\mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' )</span> given by the functoriality of the kernel.</p>

<p><a id="X7F61FE0B82AF4CDB" name="X7F61FE0B82AF4CDB"></a></p>

<h5>6.1-10 KernelObjectFunctorialWithGivenKernelObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelObjectFunctorialWithGivenKernelObjects</code>( <var class="Arg">s</var>, <var class="Arg">alpha</var>, <var class="Arg">mu</var>, <var class="Arg">alpha_prime</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( s, r )</span></p>

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

<p><a id="X7A17922D869CCEB5" name="X7A17922D869CCEB5"></a></p>

<h5>6.1-11 KernelObjectFunctorialWithGivenKernelObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ KernelObjectFunctorialWithGivenKernelObjects</code>( <var class="Arg">s</var>, <var class="Arg">alpha</var>, <var class="Arg">mu</var>, <var class="Arg">nu</var>, <var class="Arg">alpha_prime</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( s, r )</span></p>

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

<p><a id="X875F177A82BF9B8B" name="X875F177A82BF9B8B"></a></p>

<h4>6.2 <span class="Heading">Cokernel</span></h4>

<p>For a given morphism <span class="Math">\alpha: A \rightarrow B</span>, a cokernel of <span class="Math">\alpha</span> consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">K</span>,</p>

</li>
<li><p>a morphism <span class="Math">\epsilon: B \rightarrow K</span> such that <span class="Math">\epsilon \circ \alpha \sim_{A,K} 0</span>,</p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each <span class="Math">\tau: B \rightarrow T</span> satisfying <span class="Math">\tau \circ \alpha \sim_{A, T} 0</span> to a morphism <span class="Math">u(\tau):K \rightarrow T</span> such that <span class="Math">u(\tau) \circ \epsilon \sim_{B,T} \tau</span>.</p>

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

<p><a id="X82803DBC80F40EFC" name="X82803DBC80F40EFC"></a></p>

<h5>6.2-1 CokernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelObject</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the cokernel <span class="Math">K</span> of <span class="Math">\alpha</span>.</p>

<p><a id="X78948D7A7B52AB31" name="X78948D7A7B52AB31"></a></p>

<h5>6.2-2 CokernelProjection</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelProjection</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(B, \mathrm{CokernelObject}( \alpha ))</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the cokernel projection <span class="Math">\epsilon: B \rightarrow \mathrm{CokernelObject}( \alpha )</span>.</p>

<p><a id="X845DC9377A05BE7B" name="X845DC9377A05BE7B"></a></p>

<h5>6.2-3 CokernelProjectionWithGivenCokernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelProjectionWithGivenCokernelObject</code>( <var class="Arg">alpha</var>, <var class="Arg">K</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(B, K)</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow B</span> and an object <span class="Math">K = \mathrm{CokernelObject}(\alpha)</span>. The output is the cokernel projection <span class="Math">\epsilon: B \rightarrow \mathrm{CokernelObject}( \alpha )</span>.</p>

<p><a id="X872E26C57F195D50" name="X872E26C57F195D50"></a></p>

<h5>6.2-4 MorphismFromSourceToCokernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromSourceToCokernelObject</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: the zero morphism in <span class="Math">\mathrm{Hom}( A, \mathrm{CokernelObject}( \alpha ) )</span>.</p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the zero morphism <span class="Math">0: A \rightarrow \mathrm{CokernelObject}(\alpha)</span>.</p>

<p><a id="X876648527E75AA04" name="X876648527E75AA04"></a></p>

<h5>6.2-5 MorphismFromSourceToCokernelObjectWithGivenCokernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromSourceToCokernelObjectWithGivenCokernelObject</code>( <var class="Arg">alpha</var>, <var class="Arg">K</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: the zero morphism in <span class="Math">\mathrm{Hom}( A, K )</span>.</p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span> and an object <span class="Math">K = \mathrm{CokernelObject}(\alpha)</span>. The output is the zero morphism <span class="Math">0: A \rightarrow K</span>.</p>

<p><a id="X8735262382CE2560" name="X8735262382CE2560"></a></p>

<h5>6.2-6 CokernelColift</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelColift</code>( <var class="Arg">alpha</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{CokernelObject}(\alpha),T)</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow B</span>, a test object <span class="Math">T</span>, and a test morphism <span class="Math">\tau: B \rightarrow T</span> satisfying <span class="Math">\tau \circ \alpha \sim_{A, T} 0</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u(\tau): \mathrm{CokernelObject}(\alpha) \rightarrow T</span> given by the universal property of the cokernel.</p>

<p><a id="X86DB5CD27C0EB7D2" name="X86DB5CD27C0EB7D2"></a></p>

<h5>6.2-7 CokernelColiftWithGivenCokernelObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelColiftWithGivenCokernelObject</code>( <var class="Arg">alpha</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">K</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(K,T)</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow B</span>, a test object <span class="Math">T</span>, a test morphism <span class="Math">\tau: B \rightarrow T</span> satisfying <span class="Math">\tau \circ \alpha \sim_{A, T} 0</span>, and an object <span class="Math">K = \mathrm{CokernelObject}(\alpha)</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u(\tau): K \rightarrow T</span> given by the universal property of the cokernel.</p>

<p><a id="X78E421227FB90A70" name="X78E421227FB90A70"></a></p>

<h5>6.2-8 CokernelObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelObjectFunctorial</code>( <var class="Arg">L</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{CokernelObject}( \alpha ), \mathrm{CokernelObject}( \alpha' ))</span></p>

<p>The argument is a list <span class="Math">L = [ \alpha: A \rightarrow B, [ \mu:A \rightarrow A', \nu: B \rightarrow B' ], \alpha': A' \rightarrow B' ]</span>. The output is the morphism <span class="Math">\mathrm{CokernelObject}( \alpha ) \rightarrow \mathrm{CokernelObject}( \alpha' )</span> given by the functoriality of the cokernel.</p>

<p><a id="X837889ED7BD6CBED" name="X837889ED7BD6CBED"></a></p>

<h5>6.2-9 CokernelObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelObjectFunctorial</code>( <var class="Arg">alpha</var>, <var class="Arg">nu</var>, <var class="Arg">alpha_prime</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{CokernelObject}( \alpha ), \mathrm{CokernelObject}( \alpha' ))</span></p>

<p>The arguments are three morphisms <span class="Math">\alpha: A \rightarrow B, \nu: B \rightarrow B', \alpha': A' \rightarrow B'</span>. The output is the morphism <span class="Math">\mathrm{CokernelObject}( \alpha ) \rightarrow \mathrm{CokernelObject}( \alpha' )</span> given by the functoriality of the cokernel.</p>

<p><a id="X7BA172F07A431626" name="X7BA172F07A431626"></a></p>

<h5>6.2-10 CokernelObjectFunctorialWithGivenCokernelObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelObjectFunctorialWithGivenCokernelObjects</code>( <var class="Arg">s</var>, <var class="Arg">alpha</var>, <var class="Arg">nu</var>, <var class="Arg">alpha_prime</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(s, r)</span></p>

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

<p><a id="X7F59A455873709D3" name="X7F59A455873709D3"></a></p>

<h5>6.2-11 CokernelObjectFunctorialWithGivenCokernelObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CokernelObjectFunctorialWithGivenCokernelObjects</code>( <var class="Arg">s</var>, <var class="Arg">alpha</var>, <var class="Arg">mu</var>, <var class="Arg">nu</var>, <var class="Arg">alpha_prime</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(s, r)</span></p>

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

<p><a id="X797A74DE8267C974" name="X797A74DE8267C974"></a></p>

<h4>6.3 <span class="Heading">Zero Object</span></h4>

<p>A zero object consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">Z</span>,</p>

</li>
<li><p>a function <span class="Math">u_{\mathrm{in}}</span> mapping each object <span class="Math">A</span> to a morphism <span class="Math">u_{\mathrm{in}}(A): A \rightarrow Z</span>,</p>

</li>
<li><p>a function <span class="Math">u_{\mathrm{out}}</span> mapping each object <span class="Math">A</span> to a morphism <span class="Math">u_{\mathrm{out}}(A): Z \rightarrow A</span>.</p>

</li>
</ul>
<p>The triple <span class="Math">(Z, u_{\mathrm{in}}, u_{\mathrm{out}})</span> is called a <em>zero object</em> if the morphisms <span class="Math">u_{\mathrm{in}}(A)</span>, <span class="Math">u_{\mathrm{out}}(A)</span> are uniquely determined up to congruence of morphisms. We denote the object <span class="Math">Z</span> of such a triple by <span class="Math">\mathrm{ZeroObject}</span>. We say that the morphisms <span class="Math">u_{\mathrm{in}}(A)</span> and <span class="Math">u_{\mathrm{out}}(A)</span> are induced by the <em>universal property of the zero object</em>.</p>

<p><a id="X790C4FA87CADB93E" name="X790C4FA87CADB93E"></a></p>

<h5>6.3-1 ZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ZeroObject</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a category <span class="Math">C</span>. The output is a zero object <span class="Math">Z</span> of <span class="Math">C</span>.</p>

<p><a id="X87D87A177FE0542F" name="X87D87A177FE0542F"></a></p>

<h5>6.3-2 ZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ZeroObject</code>( <var class="Arg">c</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. The argument is a cell <span class="Math">c</span>. The output is a zero object <span class="Math">Z</span> of the category <span class="Math">C</span> for which <span class="Math">c \in C</span>.</p>

<p><a id="X7A0BF1118777C8A3" name="X7A0BF1118777C8A3"></a></p>

<h5>6.3-3 UniversalMorphismFromZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromZeroObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{ZeroObject}, A)</span></p>

<p>The argument is an object <span class="Math">A</span>. The output is the universal morphism <span class="Math">u_{\mathrm{out}}: \mathrm{ZeroObject} \rightarrow A</span>.</p>

<p><a id="X80327B2387F38FE8" name="X80327B2387F38FE8"></a></p>

<h5>6.3-4 UniversalMorphismFromZeroObjectWithGivenZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromZeroObjectWithGivenZeroObject</code>( <var class="Arg">A</var>, <var class="Arg">Z</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(Z, A)</span></p>

<p>The arguments are an object <span class="Math">A</span>, and a zero object <span class="Math">Z = \mathrm{ZeroObject}</span>. The output is the universal morphism <span class="Math">u_{\mathrm{out}}: Z \rightarrow A</span>.</p>

<p><a id="X86003308844F8341" name="X86003308844F8341"></a></p>

<h5>6.3-5 UniversalMorphismIntoZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoZeroObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, \mathrm{ZeroObject})</span></p>

<p>The argument is an object <span class="Math">A</span>. The output is the universal morphism <span class="Math">u_{\mathrm{in}}: A \rightarrow \mathrm{ZeroObject}</span>.</p>

<p><a id="X866104CA84CBC40A" name="X866104CA84CBC40A"></a></p>

<h5>6.3-6 UniversalMorphismIntoZeroObjectWithGivenZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoZeroObjectWithGivenZeroObject</code>( <var class="Arg">A</var>, <var class="Arg">Z</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, Z)</span></p>

<p>The arguments are an object <span class="Math">A</span>, and a zero object <span class="Math">Z = \mathrm{ZeroObject}</span>. The output is the universal morphism <span class="Math">u_{\mathrm{in}}: A \rightarrow Z</span>.</p>

<p><a id="X7F701A11812C74C5" name="X7F701A11812C74C5"></a></p>

<h5>6.3-7 MorphismFromZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromZeroObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{ZeroObject}, A)</span></p>

<p>This is a synonym for <code class="code">UniversalMorphismFromZeroObject</code>.</p>

<p><a id="X837BD808791003FF" name="X837BD808791003FF"></a></p>

<h5>6.3-8 MorphismIntoZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismIntoZeroObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, \mathrm{ZeroObject})</span></p>

<p>This is a synonym for <code class="code">UniversalMorphismIntoZeroObject</code>.</p>

<p><a id="X8711ABE9811C7CCF" name="X8711ABE9811C7CCF"></a></p>

<h5>6.3-9 IsomorphismFromZeroObjectToInitialObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromZeroObjectToInitialObject</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{ZeroObject}, \mathrm{InitialObject})</span></p>

<p>The argument is a category <span class="Math">C</span>. The output is the unique isomorphism <span class="Math">\mathrm{ZeroObject} \rightarrow \mathrm{InitialObject}</span>.</p>

<p><a id="X86FF82B284B8E2EB" name="X86FF82B284B8E2EB"></a></p>

<h5>6.3-10 IsomorphismFromInitialObjectToZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromInitialObjectToZeroObject</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{InitialObject}, \mathrm{ZeroObject})</span></p>

<p>The argument is a category <span class="Math">C</span>. The output is the unique isomorphism <span class="Math">\mathrm{InitialObject} \rightarrow \mathrm{ZeroObject}</span>.</p>

<p><a id="X78C501A179BB6CBB" name="X78C501A179BB6CBB"></a></p>

<h5>6.3-11 IsomorphismFromZeroObjectToTerminalObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromZeroObjectToTerminalObject</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{ZeroObject}, \mathrm{TerminalObject})</span></p>

<p>The argument is a category <span class="Math">C</span>. The output is the unique isomorphism <span class="Math">\mathrm{ZeroObject} \rightarrow \mathrm{TerminalObject}</span>.</p>

<p><a id="X83E84FC187EE2445" name="X83E84FC187EE2445"></a></p>

<h5>6.3-12 IsomorphismFromTerminalObjectToZeroObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromTerminalObjectToZeroObject</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{TerminalObject}, \mathrm{ZeroObject})</span></p>

<p>The argument is a category <span class="Math">C</span>. The output is the unique isomorphism <span class="Math">\mathrm{TerminalObject} \rightarrow \mathrm{ZeroObject}</span>.</p>

<p><a id="X79CEAF827DDED44B" name="X79CEAF827DDED44B"></a></p>

<h5>6.3-13 ZeroObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ZeroObjectFunctorial</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{ZeroObject}, \mathrm{ZeroObject} )</span></p>

<p>The argument is a category <span class="Math">C</span>. The output is the unique morphism <span class="Math">\mathrm{ZeroObject} \rightarrow \mathrm{ZeroObject}</span>.</p>

<p><a id="X82D7BF1F85268B0A" name="X82D7BF1F85268B0A"></a></p>

<h5>6.3-14 ZeroObjectFunctorialWithGivenZeroObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ZeroObjectFunctorialWithGivenZeroObjects</code>( <var class="Arg">C</var>, <var class="Arg">zero_object1</var>, <var class="Arg">zero_object2</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(zero_object1, zero_object2)</span></p>

<p>The argument is a category <span class="Math">C</span> and a zero object <span class="Math">\mathrm{ZeroObject}(C)</span> twice (for compatibility with other functorials). The output is the unique morphism <span class="Math">zero_object1 \rightarrow zero_object2</span>.</p>

<p><a id="X827CD17C7EBFD58F" name="X827CD17C7EBFD58F"></a></p>

<h4>6.4 <span class="Heading">Terminal Object</span></h4>

<p>A terminal object consists of two parts:</p>


<ul>
<li><p>an object <span class="Math">T</span>,</p>

</li>
<li><p>a function <span class="Math">u</span> mapping each object <span class="Math">A</span> to a morphism <span class="Math">u( A ): A \rightarrow T</span>.</p>

</li>
</ul>
<p>The pair <span class="Math">( T, u )</span> is called a <em>terminal object</em> if the morphisms <span class="Math">u( A )</span> are uniquely determined up to congruence of morphisms. We denote the object <span class="Math">T</span> of such a pair by <span class="Math">\mathrm{TerminalObject}</span>. We say that the morphism <span class="Math">u( A )</span> is induced by the <em>universal property of the terminal object</em>. <span class="Math">\\ </span> <span class="Math">\mathrm{TerminalObject}</span> is a functorial operation. This just means: There exists a unique morphism <span class="Math">T \rightarrow T</span>.</p>

<p><a id="X7DC837217946D22D" name="X7DC837217946D22D"></a></p>

<h5>6.4-1 TerminalObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ TerminalObject</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a category <span class="Math">C</span>. The output is a terminal object <span class="Math">T</span> of <span class="Math">C</span>.</p>

<p><a id="X7D86D2EA7845AEEB" name="X7D86D2EA7845AEEB"></a></p>

<h5>6.4-2 TerminalObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ TerminalObject</code>( <var class="Arg">c</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. The argument is a cell <span class="Math">c</span>. The output is a terminal object <span class="Math">T</span> of the category <span class="Math">C</span> for which <span class="Math">c \in C</span>.</p>

<p><a id="X7BEA5AF67D63F4A5" name="X7BEA5AF67D63F4A5"></a></p>

<h5>6.4-3 UniversalMorphismIntoTerminalObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoTerminalObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( A, \mathrm{TerminalObject} )</span></p>

<p>The argument is an object <span class="Math">A</span>. The output is the universal morphism <span class="Math">u(A): A \rightarrow \mathrm{TerminalObject}</span>.</p>

<p><a id="X8707AD1784DCBBFF" name="X8707AD1784DCBBFF"></a></p>

<h5>6.4-4 UniversalMorphismIntoTerminalObjectWithGivenTerminalObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoTerminalObjectWithGivenTerminalObject</code>( <var class="Arg">A</var>, <var class="Arg">T</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( A, T )</span></p>

<p>The argument are an object <span class="Math">A</span>, and an object <span class="Math">T = \mathrm{TerminalObject}</span>. The output is the universal morphism <span class="Math">u(A): A \rightarrow T</span>.</p>

<p><a id="X7C616CD287760D2F" name="X7C616CD287760D2F"></a></p>

<h5>6.4-5 TerminalObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ TerminalObjectFunctorial</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{TerminalObject}, \mathrm{TerminalObject} )</span></p>

<p>The argument is a category <span class="Math">C</span>. The output is the unique morphism <span class="Math">\mathrm{TerminalObject} \rightarrow \mathrm{TerminalObject}</span>.</p>

<p><a id="X8511229882130F93" name="X8511229882130F93"></a></p>

<h5>6.4-6 TerminalObjectFunctorialWithGivenTerminalObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ TerminalObjectFunctorialWithGivenTerminalObjects</code>( <var class="Arg">C</var>, <var class="Arg">terminal_object1</var>, <var class="Arg">terminal_object2</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(terminal_object1, terminal_object2)</span></p>

<p>The argument is a category <span class="Math">C</span> and a terminal object <span class="Math">\mathrm{TerminalObject}(C)</span> twice (for compatibility with other functorials). The output is the unique morphism <span class="Math">terminal_object1 \rightarrow terminal_object2</span>.</p>

<p><a id="X78B0ED8B80BF5254" name="X78B0ED8B80BF5254"></a></p>

<h4>6.5 <span class="Heading">Initial Object</span></h4>

<p>An initial object consists of two parts:</p>


<ul>
<li><p>an object <span class="Math">I</span>,</p>

</li>
<li><p>a function <span class="Math">u</span> mapping each object <span class="Math">A</span> to a morphism <span class="Math">u( A ): I \rightarrow A</span>.</p>

</li>
</ul>
<p>The pair <span class="Math">(I,u)</span> is called a <em>initial object</em> if the morphisms <span class="Math">u(A)</span> are uniquely determined up to congruence of morphisms. We denote the object <span class="Math">I</span> of such a triple by <span class="Math">\mathrm{InitialObject}</span>. We say that the morphism <span class="Math">u( A )</span> is induced by the <em>universal property of the initial object</em>. <span class="Math">\\ </span> <span class="Math">\mathrm{InitialObject}</span> is a functorial operation. This just means: There exists a unique morphisms <span class="Math">I \rightarrow I</span>.</p>

<p><a id="X7A70384E7F182B00" name="X7A70384E7F182B00"></a></p>

<h5>6.5-1 InitialObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InitialObject</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a category <span class="Math">C</span>. The output is an initial object <span class="Math">I</span> of <span class="Math">C</span>.</p>

<p><a id="X7E17CDF481C348B9" name="X7E17CDF481C348B9"></a></p>

<h5>6.5-2 InitialObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InitialObject</code>( <var class="Arg">c</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. The argument is a cell <span class="Math">c</span>. The output is an initial object <span class="Math">I</span> of the category <span class="Math">C</span> for which <span class="Math">c \in C</span>.</p>

<p><a id="X873FC2B087004DC3" name="X873FC2B087004DC3"></a></p>

<h5>6.5-3 UniversalMorphismFromInitialObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromInitialObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{InitialObject}, A)</span>.</p>

<p>The argument is an object <span class="Math">A</span>. The output is the universal morphism <span class="Math">u(A): \mathrm{InitialObject} \rightarrow A</span>.</p>

<p><a id="X7F7177F585576F6B" name="X7F7177F585576F6B"></a></p>

<h5>6.5-4 UniversalMorphismFromInitialObjectWithGivenInitialObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromInitialObjectWithGivenInitialObject</code>( <var class="Arg">A</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(I, A)</span>.</p>

<p>The arguments are an object <span class="Math">A</span>, and an object <span class="Math">I = \mathrm{InitialObject}</span>. The output is the universal morphism <span class="Math">u(A): \mathrm{InitialObject} \rightarrow A</span>.</p>

<p><a id="X87B1C71179F798C8" name="X87B1C71179F798C8"></a></p>

<h5>6.5-5 InitialObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InitialObjectFunctorial</code>( <var class="Arg">C</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{InitialObject}, \mathrm{InitialObject} )</span></p>

<p>The argument is a category <span class="Math">C</span>. The output is the unique morphism <span class="Math">\mathrm{InitialObject} \rightarrow \mathrm{InitialObject}</span>.</p>

<p><a id="X7CE9BBC27F70F3BD" name="X7CE9BBC27F70F3BD"></a></p>

<h5>6.5-6 InitialObjectFunctorialWithGivenInitialObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InitialObjectFunctorialWithGivenInitialObjects</code>( <var class="Arg">C</var>, <var class="Arg">initial_object1</var>, <var class="Arg">initial_object2</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(initial_object1, initial_object2)</span></p>

<p>The argument is a category <span class="Math">C</span> and an initial object <span class="Math">\mathrm{InitialObject}(C)</span> twice (for compatibility with other functorials). The output is the unique morphism <span class="Math">initial_object1 \rightarrow initial_object2</span>.</p>

<p><a id="X81FDB99378D1307A" name="X81FDB99378D1307A"></a></p>

<h4>6.6 <span class="Heading">Direct Sum</span></h4>

<p>For an integer <span class="Math">n \geq 1</span> and a given list <span class="Math">D = (S_1, \dots, S_n)</span> in an Ab-category, a direct sum consists of five parts:</p>


<ul>
<li><p>an object <span class="Math">S</span>,</p>

</li>
<li><p>a list of morphisms <span class="Math">\pi = (\pi_i: S \rightarrow S_i)_{i = 1 \dots n}</span>,</p>

</li>
<li><p>a list of morphisms <span class="Math">\iota = (\iota_i: S_i \rightarrow S)_{i = 1 \dots n}</span>,</p>

</li>
<li><p>a dependent function <span class="Math">u_{\mathrm{in}}</span> mapping every list <span class="Math">\tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}</span> to a morphism <span class="Math">u_{\mathrm{in}}(\tau): T \rightarrow S</span> such that <span class="Math">\pi_i \circ u_{\mathrm{in}}(\tau) \sim_{T,S_i} \tau_i</span> for all <span class="Math">i = 1, \dots, n</span>.</p>

</li>
<li><p>a dependent function <span class="Math">u_{\mathrm{out}}</span> mapping every list <span class="Math">\tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}</span> to a morphism <span class="Math">u_{\mathrm{out}}(\tau): S \rightarrow T</span> such that <span class="Math">u_{\mathrm{out}}(\tau) \circ \iota_i \sim_{S_i, T} \tau_i</span> for all <span class="Math">i = 1, \dots, n</span>,</p>

</li>
</ul>
<p>such that</p>


<ul>
<li><p><span class="Math">\sum_{i=1}^{n} \iota_i \circ \pi_i \sim_{S,S} \mathrm{id}_S</span>,</p>

</li>
<li><p><span class="Math">\pi_j \circ \iota_i \sim_{S_i, S_j} \delta_{i,j}</span>,</p>

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

<p><a id="X82AD6F187B550060" name="X82AD6F187B550060"></a></p>

<h5>6.6-1 DirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ DirectSum</code>( <var class="Arg">arg</var> )</td><td class="tdright">( function )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. There are two different ways to use this method:</p>


<ul>
<li><p>The argument is a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>.</p>

</li>
<li><p>The arguments are objects <span class="Math">S_1, \dots, S_n</span>.</p>

</li>
</ul>
<p>The output is the direct sum <span class="Math">\bigoplus_{i=1}^n S_i</span>.</p>

<p><a id="X7BC1F4728357D708" name="X7BC1F4728357D708"></a></p>

<h5>6.6-2 DirectSumOp</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ DirectSumOp</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>. The output is the direct sum <span class="Math">\bigoplus_{i=1}^n S_i</span>.</p>

<p><a id="X78E4506F7BBA7A9A" name="X78E4506F7BBA7A9A"></a></p>

<h5>6.6-3 ProjectionInFactorOfDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectionInFactorOfDirectSum</code>( <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \bigoplus_{i=1}^n S_i, S_k )</span></p>

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

<p><a id="X832F2E577B7B70BB" name="X832F2E577B7B70BB"></a></p>

<h5>6.6-4 ProjectionInFactorOfDirectSumWithGivenDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectionInFactorOfDirectSumWithGivenDirectSum</code>( <var class="Arg">D</var>, <var class="Arg">k</var>, <var class="Arg">S</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( S, S_k )</span></p>

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

<p><a id="X842743E97E2F28CD" name="X842743E97E2F28CD"></a></p>

<h5>6.6-5 InjectionOfCofactorOfDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InjectionOfCofactorOfDirectSum</code>( <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( S_k, \bigoplus_{i=1}^n S_i )</span></p>

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

<p><a id="X876493497F824480" name="X876493497F824480"></a></p>

<h5>6.6-6 InjectionOfCofactorOfDirectSumWithGivenDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InjectionOfCofactorOfDirectSumWithGivenDirectSum</code>( <var class="Arg">D</var>, <var class="Arg">k</var>, <var class="Arg">S</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( S_k, S )</span></p>

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

<p><a id="X84FCF65E798EBF7B" name="X84FCF65E798EBF7B"></a></p>

<h5>6.6-7 UniversalMorphismIntoDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoDirectSum</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(T, \bigoplus_{i=1}^n S_i)</span></p>

<p>The arguments are a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>, a test object <span class="Math">T</span>, and a list of morphisms <span class="Math">\tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}</span>. For convenience, the diagram <var class="Arg">D</var> and/or the test object <var class="Arg">T</var> can be omitted and are automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u_{\mathrm{in}}(\tau): T \rightarrow \bigoplus_{i=1}^n S_i</span> given by the universal property of the direct sum.</p>

<p><a id="X79EFDADB8276B639" name="X79EFDADB8276B639"></a></p>

<h5>6.6-8 UniversalMorphismIntoDirectSumWithGivenDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoDirectSumWithGivenDirectSum</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">S</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(T, S)</span></p>

<p>The arguments are a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>, a test object <span class="Math">T</span>, a list of morphisms <span class="Math">\tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}</span>, and an object <span class="Math">S = \bigoplus_{i=1}^n S_i</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u_{\mathrm{in}}(\tau): T \rightarrow S</span> given by the universal property of the direct sum.</p>

<p><a id="X812D12CF7AB6F499" name="X812D12CF7AB6F499"></a></p>

<h5>6.6-9 UniversalMorphismFromDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromDirectSum</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\bigoplus_{i=1}^n S_i, T)</span></p>

<p>The arguments are a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>, a test object <span class="Math">T</span>, and a list of morphisms <span class="Math">\tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}</span>. For convenience, the diagram <var class="Arg">D</var> and/or the test object <var class="Arg">T</var> can be omitted and are automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u_{\mathrm{out}}(\tau): \bigoplus_{i=1}^n S_i \rightarrow T</span> given by the universal property of the direct sum.</p>

<p><a id="X7B64A051814EFDDB" name="X7B64A051814EFDDB"></a></p>

<h5>6.6-10 UniversalMorphismFromDirectSumWithGivenDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromDirectSumWithGivenDirectSum</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">S</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(S, T)</span></p>

<p>The arguments are a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>, a test object <span class="Math">T</span>, a list of morphisms <span class="Math">\tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}</span>, and an object <span class="Math">S = \bigoplus_{i=1}^n S_i</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u_{\mathrm{out}}(\tau): S \rightarrow T</span> given by the universal property of the direct sum.</p>

<p><a id="X7AB9D34882B5EDDF" name="X7AB9D34882B5EDDF"></a></p>

<h5>6.6-11 IsomorphismFromDirectSumToDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromDirectSumToDirectProduct</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \bigoplus_{i=1}^n S_i, \prod_{i=1}^{n}S_i )</span></p>

<p>The argument is a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>. The output is the canonical isomorphism <span class="Math">\bigoplus_{i=1}^n S_i \rightarrow \prod_{i=1}^{n}S_i</span>.</p>

<p><a id="X7E87C9257A1BFFEE" name="X7E87C9257A1BFFEE"></a></p>

<h5>6.6-12 IsomorphismFromDirectProductToDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromDirectProductToDirectSum</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \prod_{i=1}^{n}S_i, \bigoplus_{i=1}^n S_i )</span></p>

<p>The argument is a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>. The output is the canonical isomorphism <span class="Math">\prod_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i</span>.</p>

<p><a id="X85599FEC812FD591" name="X85599FEC812FD591"></a></p>

<h5>6.6-13 IsomorphismFromDirectSumToCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromDirectSumToCoproduct</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \bigoplus_{i=1}^n S_i, \bigsqcup_{i=1}^{n}S_i )</span></p>

<p>The argument is a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>. The output is the canonical isomorphism <span class="Math">\bigoplus_{i=1}^n S_i \rightarrow \bigsqcup_{i=1}^{n}S_i</span>.</p>

<p><a id="X7CACFBCA7B9A4E19" name="X7CACFBCA7B9A4E19"></a></p>

<h5>6.6-14 IsomorphismFromCoproductToDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromCoproductToDirectSum</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \bigsqcup_{i=1}^{n}S_i, \bigoplus_{i=1}^n S_i )</span></p>

<p>The argument is a list of objects <span class="Math">D = (S_1, \dots, S_n)</span>. The output is the canonical isomorphism <span class="Math">\bigsqcup_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i</span>.</p>

<p><a id="X847C8B7E8646DF61" name="X847C8B7E8646DF61"></a></p>

<h5>6.6-15 MorphismBetweenDirectSums</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismBetweenDirectSums</code>( <var class="Arg">diagram_S</var>, <var class="Arg">M</var>, <var class="Arg">diagram_T</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\bigoplus_{i=1}^{m}A_i, \bigoplus_{j=1}^n B_j)</span></p>

<p>The arguments are given as follows:</p>


<ul>
<li><p><var class="Arg">diagram_S</var> is a list of objects <span class="Math">(A_i)_{i = 1 \dots m}</span>,</p>

</li>
<li><p><var class="Arg">diagram_T</var> is a list of objects <span class="Math">(B_j)_{j = 1 \dots n}</span>,</p>

</li>
<li><p><var class="Arg">M</var> is a list of lists of morphisms <span class="Math">( ( \phi_{i,j}: A_i \rightarrow B_j )_{j = 1 \dots n} )_{i = 1 \dots m}</span>.</p>

</li>
</ul>
<p>The output is the morphism <span class="Math">\bigoplus_{i=1}^{m}A_i \rightarrow \bigoplus_{j=1}^n B_j</span> defined by the matrix <span class="Math">M</span>.</p>

<p><a id="X7FDE63F78410A822" name="X7FDE63F78410A822"></a></p>

<h5>6.6-16 MorphismBetweenDirectSums</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismBetweenDirectSums</code>( <var class="Arg">M</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\bigoplus_{i=1}^{m}A_i, \bigoplus_{j=1}^n B_j)</span></p>

<p>This is a convenience method. The argument <span class="Math">M = ( ( \phi_{i,j}: A_i \rightarrow B_j )_{j = 1 \dots n} )_{i = 1 \dots m}</span> is a (non-empty) list of (non-empty) lists of morphisms. The output is the morphism <span class="Math">\bigoplus_{i=1}^{m}A_i \rightarrow \bigoplus_{j=1}^n B_j</span> defined by the matrix <span class="Math">M</span>.</p>

<p><a id="X7E020D2783A62178" name="X7E020D2783A62178"></a></p>

<h5>6.6-17 MorphismBetweenDirectSumsWithGivenDirectSums</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismBetweenDirectSumsWithGivenDirectSums</code>( <var class="Arg">S</var>, <var class="Arg">diagram_S</var>, <var class="Arg">M</var>, <var class="Arg">diagram_T</var>, <var class="Arg">T</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\bigoplus_{i=1}^{m}A_i, \bigoplus_{j=1}^n B_j)</span></p>

<p>The arguments are given as follows:</p>


<ul>
<li><p><var class="Arg">diagram_S</var> is a list of objects <span class="Math">(A_i)_{i = 1 \dots m}</span>,</p>

</li>
<li><p><var class="Arg">diagram_T</var> is a list of objects <span class="Math">(B_j)_{j = 1 \dots n}</span>,</p>

</li>
<li><p><var class="Arg">S</var> is the direct sum <span class="Math">\bigoplus_{i=1}^{m}A_i</span>,</p>

</li>
<li><p><var class="Arg">T</var> is the direct sum <span class="Math">\bigoplus_{j=1}^{n}B_j</span>,</p>

</li>
<li><p><var class="Arg">M</var> is a list of lists of morphisms <span class="Math">( ( \phi_{i,j}: A_i \rightarrow B_j )_{j = 1 \dots n} )_{i = 1 \dots m}</span>.</p>

</li>
</ul>
<p>The output is the morphism <span class="Math">\bigoplus_{i=1}^{m}A_i \rightarrow \bigoplus_{j=1}^n B_j</span> defined by the matrix <span class="Math">M</span>.</p>

<p><a id="X7A3400D485D0C438" name="X7A3400D485D0C438"></a></p>

<h5>6.6-18 ComponentOfMorphismIntoDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ComponentOfMorphismIntoDirectSum</code>( <var class="Arg">alpha</var>, <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, S_k)</span></p>

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

<p><a id="X7B71C4F4799263E6" name="X7B71C4F4799263E6"></a></p>

<h5>6.6-19 ComponentOfMorphismFromDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ComponentOfMorphismFromDirectSum</code>( <var class="Arg">alpha</var>, <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(S_k, A)</span></p>

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

<p><a id="X784D53A47F683192" name="X784D53A47F683192"></a></p>

<h5>6.6-20 DirectSumFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ DirectSumFunctorial</code>( <var class="Arg">source_diagram</var>, <var class="Arg">L</var>, <var class="Arg">range_diagram</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \bigoplus_{i=1}^n S_i, \bigoplus_{i=1}^n S_i' )</span></p>

<p>The arguments are a list of objects <span class="Math">(S_i)_{i = 1 \dots n}</span>, a list of morphisms <span class="Math">L = ( \mu_1: S_1 \rightarrow S_1', \dots, \mu_n: S_n \rightarrow S_n' )</span>, and a list of objects <span class="Math">(S_i')_{i = 1 \dots n}</span>. For convenience, <var class="Arg">source_diagram</var> and <var class="Arg">range_diagram</var> can be omitted and are automatically derived from <var class="Arg">L</var> in that case. The output is a morphism <span class="Math">\bigoplus_{i=1}^n S_i \rightarrow \bigoplus_{i=1}^n S_i'</span> given by the functoriality of the direct sum.</p>

<p><a id="X78B24593868483EE" name="X78B24593868483EE"></a></p>

<h5>6.6-21 DirectSumFunctorialWithGivenDirectSums</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ DirectSumFunctorialWithGivenDirectSums</code>( <var class="Arg">d_1</var>, <var class="Arg">source_diagram</var>, <var class="Arg">L</var>, <var class="Arg">range_diagram</var>, <var class="Arg">d_2</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( d_1, d_2 )</span></p>

<p>The arguments are an object <span class="Math">d_1 = \bigoplus_{i=1}^n S_i</span>, a list of objects <span class="Math">(S_i)_{i = 1 \dots n}</span>, a list of morphisms <span class="Math">L = ( \mu_1: S_1 \rightarrow S_1', \dots, \mu_n: S_n \rightarrow S_n' )</span>, a list of objects <span class="Math">(S_i')_{i = 1 \dots n}</span>, and an object <span class="Math">d_2 = \bigoplus_{i=1}^n S_i'</span>. For convenience, <var class="Arg">source_diagram</var> and <var class="Arg">range_diagram</var> can be omitted and are automatically derived from <var class="Arg">L</var> in that case. The output is a morphism <span class="Math">d_1 \rightarrow d_2</span> given by the functoriality of the direct sum.</p>

<p><a id="X7E8036DF7AC65994" name="X7E8036DF7AC65994"></a></p>

<h4>6.7 <span class="Heading">Coproduct</span></h4>

<p>For an integer <span class="Math">n \geq 1</span> and a given list of objects <span class="Math">D = ( I_1, \dots, I_n )</span>, a coproduct of <span class="Math">D</span> consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">I</span>,</p>

</li>
<li><p>a list of morphisms <span class="Math">\iota = ( \iota_i: I_i \rightarrow I )_{i = 1 \dots n}</span></p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each list of morphisms <span class="Math">\tau = ( \tau_i: I_i \rightarrow T )</span> to a morphism <span class="Math">u( \tau ): I \rightarrow T</span> such that <span class="Math">u( \tau ) \circ \iota_i \sim_{I_i, T} \tau_i</span> for all <span class="Math">i = 1, \dots, n</span>.</p>

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

<p><a id="X872D3F297979C7B8" name="X872D3F297979C7B8"></a></p>

<h5>6.7-1 Coproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ Coproduct</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a list of objects <span class="Math">D = ( I_1, \dots, I_n )</span>. The output is the coproduct <span class="Math">\bigsqcup_{i=1}^n I_i</span>.</p>

<p><a id="X7E3C6A0482E8CAB5" name="X7E3C6A0482E8CAB5"></a></p>

<h5>6.7-2 Coproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ Coproduct</code>( <var class="Arg">I1</var>, <var class="Arg">I2</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. The arguments are two objects <span class="Math">I_1, I_2</span>. The output is the coproduct <span class="Math">I_1 \bigsqcup I_2</span>.</p>

<p><a id="X82FCE4657D132584" name="X82FCE4657D132584"></a></p>

<h5>6.7-3 Coproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ Coproduct</code>( <var class="Arg">I1</var>, <var class="Arg">I2</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. The arguments are three objects <span class="Math">I_1, I_2, I_3</span>. The output is the coproduct <span class="Math">I_1 \bigsqcup I_2 \bigsqcup I_3</span>.</p>

<p><a id="X82D87B52862BB55C" name="X82D87B52862BB55C"></a></p>

<h5>6.7-4 InjectionOfCofactorOfCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InjectionOfCofactorOfCoproduct</code>( <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(I_k, \bigsqcup_{i=1}^n I_i)</span></p>

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

<p><a id="X83687CD9789CAB9C" name="X83687CD9789CAB9C"></a></p>

<h5>6.7-5 InjectionOfCofactorOfCoproductWithGivenCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InjectionOfCofactorOfCoproductWithGivenCoproduct</code>( <var class="Arg">D</var>, <var class="Arg">k</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(I_k, I)</span></p>

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

<p><a id="X7D002C7B82B26908" name="X7D002C7B82B26908"></a></p>

<h5>6.7-6 UniversalMorphismFromCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromCoproduct</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\bigsqcup_{i=1}^n I_i, T)</span></p>

<p>The arguments are a list of objects <span class="Math">D = ( I_1, \dots, I_n )</span>, a test object <span class="Math">T</span>, and a list of morphisms <span class="Math">\tau = ( \tau_i: I_i \rightarrow T )</span>. For convenience, the diagram <var class="Arg">D</var> and/or the test object <var class="Arg">T</var> can be omitted and are automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): \bigsqcup_{i=1}^n I_i \rightarrow T</span> given by the universal property of the coproduct.</p>

<p><a id="X85F392E5865012C7" name="X85F392E5865012C7"></a></p>

<h5>6.7-7 UniversalMorphismFromCoproductWithGivenCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromCoproductWithGivenCoproduct</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(I, T)</span></p>

<p>The arguments are a list of objects <span class="Math">D = ( I_1, \dots, I_n )</span>, a test object <span class="Math">T</span>, a list of morphisms <span class="Math">\tau = ( \tau_i: I_i \rightarrow T )</span>, and an object <span class="Math">I = \bigsqcup_{i=1}^n I_i</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): I \rightarrow T</span> given by the universal property of the coproduct.</p>

<p><a id="X7FDE92577EFB6866" name="X7FDE92577EFB6866"></a></p>

<h5>6.7-8 CoproductFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoproductFunctorial</code>( <var class="Arg">source_diagram</var>, <var class="Arg">L</var>, <var class="Arg">range_diagram</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\bigsqcup_{i=1}^n I_i, \bigsqcup_{i=1}^n I_i')</span></p>

<p>The arguments are a list of objects <span class="Math">(I_i)_{i = 1 \dots n}</span>, a list <span class="Math">L = ( \mu_1: I_1 \rightarrow I_1', \dots, \mu_n: I_n \rightarrow I_n' )</span>, and a list of objects <span class="Math">(I_i')_{i = 1 \dots n}</span>. For convenience, <var class="Arg">source_diagram</var> and <var class="Arg">range_diagram</var> can be omitted and are automatically derived from <var class="Arg">L</var> in that case. The output is a morphism <span class="Math">\bigsqcup_{i=1}^n I_i \rightarrow \bigsqcup_{i=1}^n I_i'</span> given by the functoriality of the coproduct.</p>

<p><a id="X85FFAD9E7FAFF9D4" name="X85FFAD9E7FAFF9D4"></a></p>

<h5>6.7-9 CoproductFunctorialWithGivenCoproducts</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoproductFunctorialWithGivenCoproducts</code>( <var class="Arg">s</var>, <var class="Arg">source_diagram</var>, <var class="Arg">L</var>, <var class="Arg">range_diagram</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(s, r)</span></p>

<p>The arguments are an object <span class="Math">s = \bigsqcup_{i=1}^n I_i</span>, a list of objects <span class="Math">(I_i)_{i = 1 \dots n}</span>, a list <span class="Math">L = ( \mu_1: I_1 \rightarrow I_1', \dots, \mu_n: I_n \rightarrow I_n' )</span>, a list of objects <span class="Math">(I_i')_{i = 1 \dots n}</span>, and an object <span class="Math">r = \bigsqcup_{i=1}^n I_i'</span>. For convenience, <var class="Arg">source_diagram</var> and <var class="Arg">range_diagram</var> can be omitted and are automatically derived from <var class="Arg">L</var> in that case. The output is a morphism <span class="Math">\bigsqcup_{i=1}^n I_i \rightarrow \bigsqcup_{i=1}^n I_i'</span> given by the functoriality of the coproduct.</p>

<p><a id="X82F0CBC179945B84" name="X82F0CBC179945B84"></a></p>

<h5>6.7-10 ComponentOfMorphismFromCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ComponentOfMorphismFromCoproduct</code>( <var class="Arg">alpha</var>, <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(I_k, A)</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: I \rightarrow A</span>, a list <span class="Math">D = (I_1, \dots, I_n)</span> of objects with <span class="Math">I = \bigsqcup_{j=1}^n I_j</span>, and an integer <span class="Math">k</span>. The output is the component morphism <span class="Math">I_k \rightarrow A</span>.</p>

<p><a id="X844C65417FBEA3C7" name="X844C65417FBEA3C7"></a></p>

<h4>6.8 <span class="Heading">Direct Product</span></h4>

<p>For an integer <span class="Math">n \geq 1</span> and a given list of objects <span class="Math">D = ( P_1, \dots, P_n )</span>, a direct product of <span class="Math">D</span> consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">P</span>,</p>

</li>
<li><p>a list of morphisms <span class="Math">\pi = ( \pi_i: P \rightarrow P_i )_{i = 1 \dots n}</span></p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each list of morphisms <span class="Math">\tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}</span> to a morphism <span class="Math">u(\tau): T \rightarrow P</span> such that <span class="Math">\pi_i \circ u( \tau ) \sim_{T,P_i} \tau_i</span> for all <span class="Math">i = 1, \dots, n</span>.</p>

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

<p><a id="X861BA02C7902A4F4" name="X861BA02C7902A4F4"></a></p>

<h5>6.8-1 DirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ DirectProduct</code>( <var class="Arg">arg</var> )</td><td class="tdright">( function )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. There are two different ways to use this method:</p>


<ul>
<li><p>The argument is a list of objects <span class="Math">D = ( P_1, \dots, P_n )</span>.</p>

</li>
<li><p>The arguments are objects <span class="Math">P_1, \dots, P_n</span>.</p>

</li>
</ul>
<p>The output is the direct product <span class="Math">\prod_{i=1}^n P_i</span>.</p>

<p><a id="X7AEF0CD1812F7EC8" name="X7AEF0CD1812F7EC8"></a></p>

<h5>6.8-2 DirectProductOp</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ DirectProductOp</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a list of objects <span class="Math">D = ( P_1, \dots, P_n )</span>. The output is the direct product <span class="Math">\prod_{i=1}^n P_i</span>.</p>

<p><a id="X7FFBE9EC7BEE7673" name="X7FFBE9EC7BEE7673"></a></p>

<h5>6.8-3 ProjectionInFactorOfDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectionInFactorOfDirectProduct</code>( <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\prod_{i=1}^n P_i, P_k)</span></p>

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

<p><a id="X8288ABA984EF9DED" name="X8288ABA984EF9DED"></a></p>

<h5>6.8-4 ProjectionInFactorOfDirectProductWithGivenDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectionInFactorOfDirectProductWithGivenDirectProduct</code>( <var class="Arg">D</var>, <var class="Arg">k</var>, <var class="Arg">P</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(P, P_k)</span></p>

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

<p><a id="X872189E4848F6863" name="X872189E4848F6863"></a></p>

<h5>6.8-5 UniversalMorphismIntoDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoDirectProduct</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(T, \prod_{i=1}^n P_i)</span></p>

<p>The arguments are a list of objects <span class="Math">D = ( P_1, \dots, P_n )</span>, a test object <span class="Math">T</span>, and a list of morphisms <span class="Math">\tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}</span>. For convenience, the diagram <var class="Arg">D</var> and/or the test object <var class="Arg">T</var> can be omitted and are automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u(\tau): T \rightarrow \prod_{i=1}^n P_i</span> given by the universal property of the direct product.</p>

<p><a id="X81A27DC180D751B8" name="X81A27DC180D751B8"></a></p>

<h5>6.8-6 UniversalMorphismIntoDirectProductWithGivenDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoDirectProductWithGivenDirectProduct</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">P</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(T, \prod_{i=1}^n P_i)</span></p>

<p>The arguments are a list of objects <span class="Math">D = ( P_1, \dots, P_n )</span>, a test object <span class="Math">T</span>, a list of morphisms <span class="Math">\tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}</span>, and an object <span class="Math">P = \prod_{i=1}^n P_i</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u(\tau): T \rightarrow \prod_{i=1}^n P_i</span> given by the universal property of the direct product.</p>

<p><a id="X79EB76507C8AB4A4" name="X79EB76507C8AB4A4"></a></p>

<h5>6.8-7 DirectProductFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ DirectProductFunctorial</code>( <var class="Arg">source_diagram</var>, <var class="Arg">L</var>, <var class="Arg">range_diagram</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \prod_{i=1}^n P_i, \prod_{i=1}^n P_i' )</span></p>

<p>The arguments are a list of objects <span class="Math">(P_i)_{i = 1 \dots n}</span>, a list of morphisms <span class="Math">L = (\mu_i: P_i \rightarrow P'_i)_{i=1\dots n}</span>, and a list of objects <span class="Math">(P_i')_{i = 1 \dots n}</span>. For convenience, <var class="Arg">source_diagram</var> and <var class="Arg">range_diagram</var> can be omitted and are automatically derived from <var class="Arg">L</var> in that case. The output is a morphism <span class="Math">\prod_{i=1}^n P_i \rightarrow \prod_{i=1}^n P_i'</span> given by the functoriality of the direct product.</p>

<p><a id="X7DD930FE78492D58" name="X7DD930FE78492D58"></a></p>

<h5>6.8-8 DirectProductFunctorialWithGivenDirectProducts</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ DirectProductFunctorialWithGivenDirectProducts</code>( <var class="Arg">s</var>, <var class="Arg">source_diagram</var>, <var class="Arg">L</var>, <var class="Arg">range_diagram</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( s, r )</span></p>

<p>The arguments are an object <span class="Math">s = \prod_{i=1}^n P_i</span>, a list of objects <span class="Math">(P_i)_{i = 1 \dots n}</span>, a list of morphisms <span class="Math">L = (\mu_i: P_i \rightarrow P'_i)_{i=1\dots n}</span>, a list of objects <span class="Math">(P_i')_{i = 1 \dots n}</span>, and an object <span class="Math">r = \prod_{i=1}^n P_i'</span>. For convenience, <var class="Arg">source_diagram</var> and <var class="Arg">range_diagram</var> can be omitted and are automatically derived from <var class="Arg">L</var> in that case. The output is a morphism <span class="Math">\prod_{i=1}^n P_i \rightarrow \prod_{i=1}^n P_i'</span> given by the functoriality of the direct product.</p>

<p><a id="X7C5769577CEAF2C4" name="X7C5769577CEAF2C4"></a></p>

<h5>6.8-9 ComponentOfMorphismIntoDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ComponentOfMorphismIntoDirectProduct</code>( <var class="Arg">alpha</var>, <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, P_k)</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow P</span>, a list <span class="Math">D = (P_1, \dots, P_n)</span> of objects with <span class="Math">P = \prod_{j=1}^n P_j</span>, and an integer <span class="Math">k</span>. The output is the component morphism <span class="Math">A \rightarrow P_k</span>.</p>

<p><a id="X824FD8F786D2350D" name="X824FD8F786D2350D"></a></p>

<h4>6.9 <span class="Heading">Equalizer</span></h4>

<p>For an integer <span class="Math">n \geq 1</span> and a given list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>, an equalizer of <span class="Math">D</span> consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">E</span>,</p>

</li>
<li><p>a morphism <span class="Math">\iota: E \rightarrow A </span> such that <span class="Math">\beta_i \circ \iota \sim_{E, B} \beta_j \circ \iota</span> for all pairs <span class="Math">i,j</span>.</p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each morphism <span class="Math">\tau = ( \tau: T \rightarrow A )</span> such that <span class="Math">\beta_i \circ \tau \sim_{T, B} \beta_j \circ \tau</span> for all pairs <span class="Math">i,j</span> to a morphism <span class="Math">u( \tau ): T \rightarrow E</span> such that <span class="Math">\iota \circ u( \tau ) \sim_{T, A} \tau</span>.</p>

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

<p><a id="X824FD8F786D2350D" name="X824FD8F786D2350D"></a></p>

<h5>6.9-1 Equalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ Equalizer</code>( <var class="Arg">arg</var> )</td><td class="tdright">( function )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. There are three different ways to use this method:</p>


<ul>
<li><p>The arguments are an object <span class="Math">A</span> and a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>.</p>

</li>
<li><p>The argument is a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>.</p>

</li>
<li><p>The arguments are morphisms <span class="Math">\beta_1: A \rightarrow B, \dots, \beta_n: A \rightarrow B</span>.</p>

</li>
</ul>
<p>The output is the equalizer <span class="Math">\mathrm{Equalizer}(D)</span>.</p>

<p><a id="X7B1937088320E680" name="X7B1937088320E680"></a></p>

<h5>6.9-2 EqualizerOp</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ EqualizerOp</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>The arguments are an object <span class="Math">A</span> and list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the equalizer <span class="Math">\mathrm{Equalizer}(D)</span>.</p>

<p><a id="X803E62B382D76E4F" name="X803E62B382D76E4F"></a></p>

<h5>6.9-3 EmbeddingOfEqualizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ EmbeddingOfEqualizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{Equalizer}(D), A )</span></p>

<p>The arguments are an object <span class="Math">A</span> and a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the equalizer embedding <span class="Math">\iota: \mathrm{Equalizer}(D) \rightarrow A</span>.</p>

<p><a id="X828423F283DF97BA" name="X828423F283DF97BA"></a></p>

<h5>6.9-4 EmbeddingOfEqualizerWithGivenEqualizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ EmbeddingOfEqualizerWithGivenEqualizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var>, <var class="Arg">E</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( E, A )</span></p>

<p>The arguments are an object <span class="Math">A</span>, a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>, and an object <span class="Math">E = \mathrm{Equalizer}(D)</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the equalizer embedding <span class="Math">\iota: E \rightarrow A</span>.</p>

<p><a id="X78A6E6AA87FADB13" name="X78A6E6AA87FADB13"></a></p>

<h5>6.9-5 MorphismFromEqualizerToSink</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromEqualizerToSink</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{Equalizer}(D), B )</span></p>

<p>The arguments are an object <span class="Math">A</span> and a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the composition <span class="Math">\mu: \mathrm{Equalizer}(D) \rightarrow B</span> of the embedding <span class="Math">\iota: \mathrm{Equalizer}(D) \rightarrow A</span> and <span class="Math">\beta_1</span>.</p>

<p><a id="X7CF04F98844789DE" name="X7CF04F98844789DE"></a></p>

<h5>6.9-6 MorphismFromEqualizerToSinkWithGivenEqualizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromEqualizerToSinkWithGivenEqualizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var>, <var class="Arg">E</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( E, B )</span></p>

<p>The arguments are an object <span class="Math">A</span>, a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span> and an object <span class="Math">E = \mathrm{Equalizer}(D)</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the composition <span class="Math">\mu: E \rightarrow B</span> of the embedding <span class="Math">\iota: E \rightarrow A</span> and <span class="Math">\beta_1</span>.</p>

<p><a id="X872F9E2E853EB91D" name="X872F9E2E853EB91D"></a></p>

<h5>6.9-7 UniversalMorphismIntoEqualizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoEqualizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( T, \mathrm{Equalizer}(D) )</span></p>

<p>The arguments are an object <span class="Math">A</span>, a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>, a test object <span class="Math">T</span>, and a morphism <span class="Math"> \tau: T \rightarrow A </span> such that <span class="Math">\beta_i \circ \tau \sim_{T, B} \beta_j \circ \tau</span> for all pairs <span class="Math">i,j</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): T \rightarrow \mathrm{Equalizer}(D)</span> given by the universal property of the equalizer.</p>

<p><a id="X7F7191B57D8AA456" name="X7F7191B57D8AA456"></a></p>

<h5>6.9-8 UniversalMorphismIntoEqualizerWithGivenEqualizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoEqualizerWithGivenEqualizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">E</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( T, E )</span></p>

<p>The arguments are an object <span class="Math">A</span>, a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>, a test object <span class="Math">T</span>, a morphism <span class="Math">\tau: T \rightarrow A )</span> such that <span class="Math">\beta_i \circ \tau \sim_{T, B} \beta_j \circ \tau</span> for all pairs <span class="Math">i,j</span>, and an object <span class="Math">E = \mathrm{Equalizer}(D)</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): T \rightarrow E</span> given by the universal property of the equalizer.</p>

<p><a id="X82400CA57F0E5585" name="X82400CA57F0E5585"></a></p>

<h5>6.9-9 EqualizerFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ EqualizerFunctorial</code>( <var class="Arg">Ls</var>, <var class="Arg">mu</var>, <var class="Arg">Lr</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{Equalizer}( ( \beta_i )_{i=1 \dots n} ), \mathrm{Equalizer}( ( \beta_i' )_{i=1 \dots n} ))</span></p>

<p>The arguments are a list of morphisms <span class="Math">L_s = (\beta_i: A \rightarrow B)_{i = 1 \dots n}</span>, a morphism <span class="Math">\mu: A \rightarrow A'</span>, and a list of morphisms <span class="Math">L_r = (\beta_i': A' \rightarrow B')_{i = 1 \dots n}</span> such that there exists a morphism <span class="Math">\beta: B \rightarrow B'</span> such that <span class="Math">\beta_i' \circ \mu \sim_{A,B'} \beta \circ \beta_i</span> for <span class="Math">i = 1, \dots, n</span>. The output is the morphism <span class="Math">\mathrm{Equalizer}( ( \beta_i )_{i=1 \dots n} ) \rightarrow \mathrm{Equalizer}( ( \beta_i' )_{i=1 \dots n} )</span> given by the functorality of the equalizer.</p>

<p><a id="X7804D05C7EFDC5CE" name="X7804D05C7EFDC5CE"></a></p>

<h5>6.9-10 EqualizerFunctorialWithGivenEqualizers</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ EqualizerFunctorialWithGivenEqualizers</code>( <var class="Arg">s</var>, <var class="Arg">Ls</var>, <var class="Arg">mu</var>, <var class="Arg">Lr</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(s, r)</span></p>

<p>The arguments are an object <span class="Math">s = \mathrm{Equalizer}( ( \beta_i )_{i=1 \dots n} )</span>, a list of morphisms <span class="Math">L_s = (\beta_i: A \rightarrow B)_{i = 1 \dots n}</span>, a morphism <span class="Math">\mu: A \rightarrow A'</span>, and a list of morphisms <span class="Math">L_r = (\beta_i': A' \rightarrow B')_{i = 1 \dots n}</span> such that there exists a morphism <span class="Math">\beta: B \rightarrow B'</span> such that <span class="Math">\beta_i' \circ \mu \sim_{A,B'} \beta \circ \beta_i</span> for <span class="Math">i = 1, \dots, n</span>, and an object <span class="Math">r = \mathrm{Equalizer}( ( \beta_i' )_{i=1 \dots n} )</span>. The output is the morphism <span class="Math">s \rightarrow r</span> given by the functorality of the equalizer.</p>

<p><a id="X7DD2167B7836DF62" name="X7DD2167B7836DF62"></a></p>

<h5>6.9-11 JointPairwiseDifferencesOfMorphismsIntoDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ JointPairwiseDifferencesOfMorphismsIntoDirectProduct</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( A, \prod_{i=1}^{n-1} B )</span></p>

<p>The arguments are an object A and a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>. The output is a morphism <span class="Math">A \rightarrow \prod_{i=1}^{n-1} B</span> such that its kernel equalizes the <span class="Math">\beta_i</span>.</p>

<p><a id="X7E8843F17F0F3D14" name="X7E8843F17F0F3D14"></a></p>

<h5>6.9-12 IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromEqualizerToKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProduct</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{Equalizer}(D), \Delta)</span></p>

<p>The arguments are an object A and a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>. The output is a morphism <span class="Math">\mathrm{Equalizer}(D) \rightarrow \Delta</span>, where <span class="Math">\Delta</span> denotes the kernel object equalizing the morphisms <span class="Math">\beta_i</span>.</p>

<p><a id="X7A96B57382715059" name="X7A96B57382715059"></a></p>

<h5>6.9-13 IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromKernelOfJointPairwiseDifferencesOfMorphismsIntoDirectProductToEqualizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\Delta, \mathrm{Equalizer}(D))</span></p>

<p>The arguments are an object A and a list of morphisms <span class="Math">D = ( \beta_i: A \rightarrow B )_{i = 1 \dots n}</span>. The output is a morphism <span class="Math">\Delta \rightarrow \mathrm{Equalizer}(D)</span>, where <span class="Math">\Delta</span> denotes the kernel object equalizing the morphisms <span class="Math">\beta_i</span>.</p>

<p><a id="X7BA8F7BD793CC288" name="X7BA8F7BD793CC288"></a></p>

<h4>6.10 <span class="Heading">Coequalizer</span></h4>

<p>For an integer <span class="Math">n \geq 1</span> and a given list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>, a coequalizer of <span class="Math">D</span> consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">C</span>,</p>

</li>
<li><p>a morphism <span class="Math">\pi: A \rightarrow C </span> such that <span class="Math">\pi \circ \beta_i \sim_{B,C} \pi \circ \beta_j</span> for all pairs <span class="Math">i,j</span>,</p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping the morphism <span class="Math">\tau: A \rightarrow T </span> such that <span class="Math">\tau \circ \beta_i \sim_{B,T} \tau \circ \beta_j</span> to a morphism <span class="Math">u( \tau ): C \rightarrow T</span> such that <span class="Math">u( \tau ) \circ \pi \sim_{A, T} \tau</span>.</p>

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

<p><a id="X7BA8F7BD793CC288" name="X7BA8F7BD793CC288"></a></p>

<h5>6.10-1 Coequalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ Coequalizer</code>( <var class="Arg">arg</var> )</td><td class="tdright">( function )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. There are three different ways to use this method:</p>


<ul>
<li><p>The arguments are an object <span class="Math">A</span> and a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>.</p>

</li>
<li><p>The argument is a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>.</p>

</li>
<li><p>The arguments are morphisms <span class="Math">\beta_1: B \rightarrow A, \dots, \beta_n: B \rightarrow A</span>.</p>

</li>
</ul>
<p>The output is the coequalizer <span class="Math">\mathrm{Coequalizer}(D)</span>.</p>

<p><a id="X80FCD6BE84781FE6" name="X80FCD6BE84781FE6"></a></p>

<h5>6.10-2 CoequalizerOp</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoequalizerOp</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>The arguments are an object <span class="Math">A</span> and a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the coequalizer <span class="Math">\mathrm{Coequalizer}(D)</span>.</p>

<p><a id="X7E0468077DE9EC3B" name="X7E0468077DE9EC3B"></a></p>

<h5>6.10-3 ProjectionOntoCoequalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectionOntoCoequalizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( A, \mathrm{Coequalizer}( D ) )</span>.</p>

<p>The arguments are an object <span class="Math">A</span> and a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the projection <span class="Math">\pi: A \rightarrow \mathrm{Coequalizer}( D )</span>.</p>

<p><a id="X78B7474384BAA57A" name="X78B7474384BAA57A"></a></p>

<h5>6.10-4 ProjectionOntoCoequalizerWithGivenCoequalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectionOntoCoequalizerWithGivenCoequalizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var>, <var class="Arg">C</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( A, C )</span>.</p>

<p>The arguments are an object <span class="Math">A</span>, a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>, and an object <span class="Math">C = \mathrm{Coequalizer}(D)</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the projection <span class="Math">\pi: A \rightarrow C</span>.</p>

<p><a id="X7D3F328F82CD8A49" name="X7D3F328F82CD8A49"></a></p>

<h5>6.10-5 MorphismFromSourceToCoequalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromSourceToCoequalizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( B, \mathrm{Coequalizer}( D ) )</span>.</p>

<p>The arguments are an object <span class="Math">A</span> and a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the composition <span class="Math">\mu: B \rightarrow \mathrm{Coequalizer}(D)</span> of <span class="Math">\beta_1</span> and the projection <span class="Math">\pi: A \rightarrow \mathrm{Coequalizer}( D )</span>.</p>

<p><a id="X82EB657782E82115" name="X82EB657782E82115"></a></p>

<h5>6.10-6 MorphismFromSourceToCoequalizerWithGivenCoequalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromSourceToCoequalizerWithGivenCoequalizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var>, <var class="Arg">C</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( B, C )</span>.</p>

<p>The arguments are an object <span class="Math">A</span>, a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span> and an object <span class="Math">C = \mathrm{Coequalizer}(D)</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. The output is the composition <span class="Math">\mu: B \rightarrow C</span> of <span class="Math">\beta_1</span> and the projection <span class="Math">\pi: A \rightarrow C</span>.</p>

<p><a id="X86EFF737796C2630" name="X86EFF737796C2630"></a></p>

<h5>6.10-7 UniversalMorphismFromCoequalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromCoequalizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{Coequalizer}(D), T )</span></p>

<p>The arguments are an object <span class="Math">A</span>, a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>, a test object <span class="Math">T</span>, and a morphism <span class="Math">\tau: A \rightarrow T </span> such that <span class="Math">\tau \circ \beta_i \sim_{B,T} \tau \circ \beta_j</span> for all pairs <span class="Math">i,j</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): \mathrm{Coequalizer}(D) \rightarrow T</span> given by the universal property of the coequalizer.</p>

<p><a id="X816990198092E8B6" name="X816990198092E8B6"></a></p>

<h5>6.10-8 UniversalMorphismFromCoequalizerWithGivenCoequalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromCoequalizerWithGivenCoequalizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">C</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( C, T )</span></p>

<p>The arguments are an object <span class="Math">A</span>, a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>, a test object <span class="Math">T</span>, a morphism <span class="Math">\tau: A \rightarrow T </span> such that <span class="Math">\tau \circ \beta_i \sim_{B,T} \tau \circ \beta_j</span>, and an object <span class="Math">C = \mathrm{Coequalizer}(D)</span>. For convenience, the object <span class="Math">A</span> can be omitted and is automatically derived from <span class="Math">D</span> in that case. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): C \rightarrow T</span> given by the universal property of the coequalizer.</p>

<p><a id="X818C5AD2794A2C7B" name="X818C5AD2794A2C7B"></a></p>

<h5>6.10-9 CoequalizerFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoequalizerFunctorial</code>( <var class="Arg">Ls</var>, <var class="Arg">mu</var>, <var class="Arg">Lr</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{Coequalizer}( ( \beta_i )_{i=1 \dots n} ), \mathrm{Coequalizer}( ( \beta_i' )_{i=1 \dots n} ))</span></p>

<p>The arguments are a list of morphisms <span class="Math">L_s = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>, a morphism <span class="Math">\mu: A \rightarrow A'</span>, and a list of morphisms <span class="Math">L_r = ( \beta_i': B' \rightarrow A' )_{i = 1 \dots n}</span> such that there exists a morphism <span class="Math">\beta: B \rightarrow B'</span> such that <span class="Math">\beta_i' \circ \beta \sim_{B, A'} \mu \circ \beta_i</span> for <span class="Math">i = 1, \dots n</span>. The output is the morphism <span class="Math">\mathrm{Coequalizer}( ( \beta_i )_{i=1}^n ) \rightarrow \mathrm{Coequalizer}( ( \beta_i' )_{i=1}^n )</span> given by the functorality of the coequalizer.</p>

<p><a id="X7CB3323C7B44B75F" name="X7CB3323C7B44B75F"></a></p>

<h5>6.10-10 CoequalizerFunctorialWithGivenCoequalizers</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoequalizerFunctorialWithGivenCoequalizers</code>( <var class="Arg">s</var>, <var class="Arg">Ls</var>, <var class="Arg">mu</var>, <var class="Arg">Lr</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(s, r)</span></p>

<p>The arguments are an object <span class="Math">s = \mathrm{Coequalizer}( ( \beta_i )_{i=1}^n )</span>, a list of morphisms <span class="Math">L_s = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>, a morphism <span class="Math">\mu: A \rightarrow A'</span>, and a list of morphisms <span class="Math">L_r = ( \beta_i': B' \rightarrow A' )_{i = 1 \dots n}</span> such that there exists a morphism <span class="Math">\beta: B \rightarrow B'</span> such that <span class="Math">\beta_i' \circ \beta \sim_{B, A'} \mu \circ \beta_i</span> for <span class="Math">i = 1, \dots n</span>, and an object <span class="Math">r = \mathrm{Coequalizer}( ( \beta_i' )_{i=1}^n )</span>. The output is the morphism <span class="Math">s \rightarrow r</span> given by the functorality of the coequalizer.</p>

<p><a id="X7AE156547D6F06CE" name="X7AE156547D6F06CE"></a></p>

<h5>6.10-11 JointPairwiseDifferencesOfMorphismsFromCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ JointPairwiseDifferencesOfMorphismsFromCoproduct</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\bigsqcup_{i=1}^{n-1} B, A)</span></p>

<p>The arguments are an object A and a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>. The output is a morphism <span class="Math">\bigsqcup_{i=1}^{n-1} B \rightarrow A</span> such that its cokernel coequalizes the <span class="Math">\beta_i</span>.</p>

<p><a id="X80AFEE3579EB987A" name="X80AFEE3579EB987A"></a></p>

<h5>6.10-12 IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromCoequalizerToCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproduct</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{Coequalizer}(D), \Delta)</span></p>

<p>The arguments are an object A and a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>. The output is a morphism <span class="Math">\mathrm{Coequalizer}(D) \rightarrow \Delta</span>, where <span class="Math">\Delta</span> denotes the cokernel object coequalizing the morphisms <span class="Math">\beta_i</span>.</p>

<p><a id="X78A3F1087B86E650" name="X78A3F1087B86E650"></a></p>

<h5>6.10-13 IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromCokernelOfJointPairwiseDifferencesOfMorphismsFromCoproductToCoequalizer</code>( <var class="Arg">A</var>, <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\Delta, \mathrm{Coequalizer}(D))</span></p>

<p>The arguments are an object A and a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow A )_{i = 1 \dots n}</span>. The output is a morphism <span class="Math">\Delta \rightarrow \mathrm{Coequalizer}(D)</span>, where <span class="Math">\Delta</span> denotes the cokernel object coequalizing the morphisms <span class="Math">\beta_i</span>.</p>

<p><a id="X8038824E84B571F8" name="X8038824E84B571F8"></a></p>

<h4>6.11 <span class="Heading">Fiber Product (= Pullback)</span></h4>

<p>For an integer <span class="Math">n \geq 1</span> and a given list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span>, a fiber product of <span class="Math">D</span> consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">P</span>,</p>

</li>
<li><p>a list of morphisms <span class="Math">\pi = ( \pi_i: P \rightarrow P_i )_{i = 1 \dots n}</span> such that <span class="Math">\beta_i \circ \pi_i \sim_{P, B} \beta_j \circ \pi_j</span> for all pairs <span class="Math">i,j</span>.</p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each list of morphisms <span class="Math">\tau = ( \tau_i: T \rightarrow P_i )</span> such that <span class="Math">\beta_i \circ \tau_i \sim_{T, B} \beta_j \circ \tau_j</span> for all pairs <span class="Math">i,j</span> to a morphism <span class="Math">u( \tau ): T \rightarrow P</span> such that <span class="Math">\pi_i \circ u( \tau ) \sim_{T, P_i} \tau_i</span> for all <span class="Math">i = 1, \dots, n</span>.</p>

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

<p><a id="X7DAB395584678429" name="X7DAB395584678429"></a></p>

<h5>6.11-1 IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{FiberProduct}(D), \Delta)</span></p>

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

<p><a id="X8190FBB47DB6307D" name="X8190FBB47DB6307D"></a></p>

<h5>6.11-2 IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromEqualizerOfDirectProductDiagramToFiberProduct</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\Delta, \mathrm{FiberProduct}(D))</span></p>

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

<p><a id="X82157EF887CC99D1" name="X82157EF887CC99D1"></a></p>

<h5>6.11-3 FiberProductEmbeddingInDirectProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ FiberProductEmbeddingInDirectProduct</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{FiberProduct}(D), \prod_{i=1}^n P_i )</span></p>

<p>This is a convenience method. The argument is a list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span>. The output is the natural embedding <span class="Math">\mathrm{FiberProduct}(D) \rightarrow \prod_{i=1}^n P_i</span>.</p>

<p><a id="X7919AF7486FA42C5" name="X7919AF7486FA42C5"></a></p>

<h5>6.11-4 FiberProductEmbeddingInDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ FiberProductEmbeddingInDirectSum</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{FiberProduct}(D), \bigoplus_{i=1}^n P_i )</span></p>

<p>This is a convenience method. The argument is a list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span>. The output is the natural embedding <span class="Math">\mathrm{FiberProduct}(D) \rightarrow \bigoplus_{i=1}^n P_i</span>.</p>

<p><a id="X7DE20941803BFBD9" name="X7DE20941803BFBD9"></a></p>

<h5>6.11-5 FiberProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ FiberProduct</code>( <var class="Arg">arg</var> )</td><td class="tdright">( function )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. There are two different ways to use this method:</p>


<ul>
<li><p>The argument is a list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span>.</p>

</li>
<li><p>The arguments are morphisms <span class="Math">\beta_1: P_1 \rightarrow B, \dots, \beta_n: P_n \rightarrow B</span>.</p>

</li>
</ul>
<p>The output is the fiber product <span class="Math">\mathrm{FiberProduct}(D)</span>.</p>

<p><a id="X8000EEB77D6E8B7C" name="X8000EEB77D6E8B7C"></a></p>

<h5>6.11-6 FiberProductOp</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ FiberProductOp</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span>. The output is the fiber product <span class="Math">\mathrm{FiberProduct}(D)</span>.</p>

<p><a id="X8104B3717D3B646F" name="X8104B3717D3B646F"></a></p>

<h5>6.11-7 ProjectionInFactorOfFiberProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectionInFactorOfFiberProduct</code>( <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{FiberProduct}(D), P_k )</span></p>

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

<p><a id="X8085606A7B09071F" name="X8085606A7B09071F"></a></p>

<h5>6.11-8 ProjectionInFactorOfFiberProductWithGivenFiberProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectionInFactorOfFiberProductWithGivenFiberProduct</code>( <var class="Arg">D</var>, <var class="Arg">k</var>, <var class="Arg">P</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( P, P_k )</span></p>

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

<p><a id="X7C6EF50085D13D12" name="X7C6EF50085D13D12"></a></p>

<h5>6.11-9 MorphismFromFiberProductToSink</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromFiberProductToSink</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{FiberProduct}(D), B )</span></p>

<p>The arguments are a list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span>. The output is the composition <span class="Math">\mu: \mathrm{FiberProduct}(D) \rightarrow B</span> of the <span class="Math">1</span>-st projection <span class="Math">\pi_1: \mathrm{FiberProduct}(D) \rightarrow P_1</span> and <span class="Math">\beta_1</span>.</p>

<p><a id="X866ED61786F4C76C" name="X866ED61786F4C76C"></a></p>

<h5>6.11-10 MorphismFromFiberProductToSinkWithGivenFiberProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromFiberProductToSinkWithGivenFiberProduct</code>( <var class="Arg">D</var>, <var class="Arg">P</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( P, B )</span></p>

<p>The arguments are a list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span> and an object <span class="Math">P = \mathrm{FiberProduct}(D)</span>. The output is the composition <span class="Math">\mu: P \rightarrow B</span> of the <span class="Math">1</span>-st projection <span class="Math">\pi_1: P \rightarrow P_1</span> and <span class="Math">\beta_1</span>.</p>

<p><a id="X8441CF7F8140E8C2" name="X8441CF7F8140E8C2"></a></p>

<h5>6.11-11 UniversalMorphismIntoFiberProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoFiberProduct</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( T, \mathrm{FiberProduct}(D) )</span></p>

<p>The arguments are a list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span>, a test object <span class="Math">T</span>, and a list of morphisms <span class="Math">\tau = ( \tau_i: T \rightarrow P_i )</span> such that <span class="Math">\beta_i \circ \tau_i \sim_{T, B} \beta_j \circ \tau_j</span> for all pairs <span class="Math">i,j</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): T \rightarrow \mathrm{FiberProduct}(D)</span> given by the universal property of the fiber product.</p>

<p><a id="X7A6A890D85F01977" name="X7A6A890D85F01977"></a></p>

<h5>6.11-12 UniversalMorphismIntoFiberProductWithGivenFiberProduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoFiberProductWithGivenFiberProduct</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">P</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( T, P )</span></p>

<p>The arguments are a list of morphisms <span class="Math">D = ( \beta_i: P_i \rightarrow B )_{i = 1 \dots n}</span>, a test object <span class="Math">T</span>, a list of morphisms <span class="Math">\tau = ( \tau_i: T \rightarrow P_i )</span> such that <span class="Math">\beta_i \circ \tau_i \sim_{T, B} \beta_j \circ \tau_j</span> for all pairs <span class="Math">i,j</span>, and an object <span class="Math">P = \mathrm{FiberProduct}(D)</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): T \rightarrow P</span> given by the universal property of the fiber product.</p>

<p><a id="X791F33AB7EAF6A2A" name="X791F33AB7EAF6A2A"></a></p>

<h5>6.11-13 FiberProductFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ FiberProductFunctorial</code>( <var class="Arg">Ls</var>, <var class="Arg">Lm</var>, <var class="Arg">Lr</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{FiberProduct}( ( \beta_i )_{i=1 \dots n} ), \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} ))</span></p>

<p>The arguments are three lists of morphisms <span class="Math">L_s = ( \beta_i: P_i \rightarrow B)_{i = 1 \dots n}</span>, <span class="Math">L_m = ( \mu_i: P_i \rightarrow P_i' )_{i = 1 \dots n}</span>, <span class="Math">L_r = ( \beta_i': P_i' \rightarrow B')_{i = 1 \dots n}</span> having the same length <span class="Math">n</span> such that there exists a morphism <span class="Math">\beta: B \rightarrow B'</span> such that <span class="Math">\beta_i' \circ \mu_i \sim_{P_i,B'} \beta \circ \beta_i</span> for <span class="Math">i = 1, \dots, n</span>. The output is the morphism <span class="Math">\mathrm{FiberProduct}( ( \beta_i )_{i=1 \dots n} ) \rightarrow \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} )</span> given by the functoriality of the fiber product.</p>

<p><a id="X83A9F01A82894F65" name="X83A9F01A82894F65"></a></p>

<h5>6.11-14 FiberProductFunctorialWithGivenFiberProducts</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ FiberProductFunctorialWithGivenFiberProducts</code>( <var class="Arg">s</var>, <var class="Arg">Ls</var>, <var class="Arg">Lm</var>, <var class="Arg">Lr</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(s, r)</span></p>

<p>The arguments are an object <span class="Math">s = \mathrm{FiberProduct}( ( \beta_i )_{i=1 \dots n} )</span>, three lists of morphisms <span class="Math">L_s = ( \beta_i: P_i \rightarrow B)_{i = 1 \dots n}</span>, <span class="Math">L_m = ( \mu_i: P_i \rightarrow P_i' )_{i = 1 \dots n}</span>, <span class="Math">L_r = ( \beta_i': P_i' \rightarrow B')_{i = 1 \dots n}</span> having the same length <span class="Math">n</span> such that there exists a morphism <span class="Math">\beta: B \rightarrow B'</span> such that <span class="Math">\beta_i' \circ \mu_i \sim_{P_i,B'} \beta \circ \beta_i</span> for <span class="Math">i = 1, \dots, n</span>, and an object <span class="Math">r = \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} )</span>. The output is the morphism <span class="Math">s \rightarrow r</span> given by the functoriality of the fiber product.</p>

<p><a id="X81A2D49D85923894" name="X81A2D49D85923894"></a></p>

<h4>6.12 <span class="Heading">Pushout</span></h4>

<p>For an integer <span class="Math">n \geq 1</span> and a given list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>, a pushout of <span class="Math">D</span> consists of three parts:</p>


<ul>
<li><p>an object <span class="Math">I</span>,</p>

</li>
<li><p>a list of morphisms <span class="Math">\iota = ( \iota_i: I_i \rightarrow I )_{i = 1 \dots n}</span> such that <span class="Math">\iota_i \circ \beta_i \sim_{B,I} \iota_j \circ \beta_j</span> for all pairs <span class="Math">i,j</span>,</p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each list of morphisms <span class="Math">\tau = ( \tau_i: I_i \rightarrow T )_{i = 1 \dots n}</span> such that <span class="Math">\tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j</span> to a morphism <span class="Math">u( \tau ): I \rightarrow T</span> such that <span class="Math">u( \tau ) \circ \iota_i \sim_{I_i, T} \tau_i</span> for all <span class="Math">i = 1, \dots, n</span>.</p>

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

<p><a id="X87C495A782BE3433" name="X87C495A782BE3433"></a></p>

<h5>6.12-1 IsomorphismFromPushoutToCoequalizerOfCoproductDiagram</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromPushoutToCoequalizerOfCoproductDiagram</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{Pushout}(D), \Delta)</span></p>

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

<p><a id="X7EAFDD727D94E932" name="X7EAFDD727D94E932"></a></p>

<h5>6.12-2 IsomorphismFromCoequalizerOfCoproductDiagramToPushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromCoequalizerOfCoproductDiagramToPushout</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \Delta, \mathrm{Pushout}(D))</span></p>

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

<p><a id="X7E718F228767638A" name="X7E718F228767638A"></a></p>

<h5>6.12-3 PushoutProjectionFromCoproduct</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ PushoutProjectionFromCoproduct</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \bigsqcup {i=1}^n I_i, \mathrm{Pushout}(D) )</span></p>

<p>This is a convenience method. The argument is a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>. The output is the natural projection <span class="Math">\bigsqcup_{i=1}^n I_i \rightarrow \mathrm{Pushout}(D)</span>.</p>

<p><a id="X837467847F63FE1B" name="X837467847F63FE1B"></a></p>

<h5>6.12-4 PushoutProjectionFromDirectSum</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ PushoutProjectionFromDirectSum</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \bigoplus_{i=1}^n I_i, \mathrm{Pushout}(D) )</span></p>

<p>This is a convenience method. The argument is a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>. The output is the natural projection <span class="Math">\bigoplus_{i=1}^n I_i \rightarrow \mathrm{Pushout}(D)</span>.</p>

<p><a id="X78E10D9E849FE214" name="X78E10D9E849FE214"></a></p>

<h5>6.12-5 Pushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ Pushout</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>. The output is the pushout <span class="Math">\mathrm{Pushout}(D)</span>.</p>

<p><a id="X78D93A2883C83CAC" name="X78D93A2883C83CAC"></a></p>

<h5>6.12-6 Pushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ Pushout</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>This is a convenience method. The arguments are a morphism <span class="Math">\alpha</span> and a morphism <span class="Math">\beta</span>. The output is the pushout <span class="Math">\mathrm{Pushout}(\alpha, \beta)</span>.</p>

<p><a id="X7CF12E527805752F" name="X7CF12E527805752F"></a></p>

<h5>6.12-7 InjectionOfCofactorOfPushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InjectionOfCofactorOfPushout</code>( <var class="Arg">D</var>, <var class="Arg">k</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( I_k, \mathrm{Pushout}( D ) )</span>.</p>

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

<p><a id="X7E54DB957B5F9157" name="X7E54DB957B5F9157"></a></p>

<h5>6.12-8 InjectionOfCofactorOfPushoutWithGivenPushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InjectionOfCofactorOfPushoutWithGivenPushout</code>( <var class="Arg">D</var>, <var class="Arg">k</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( I_k, I )</span>.</p>

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

<p><a id="X84B182F882D1F039" name="X84B182F882D1F039"></a></p>

<h5>6.12-9 MorphismFromSourceToPushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromSourceToPushout</code>( <var class="Arg">D</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( B, \mathrm{Pushout}( D ) )</span>.</p>

<p>The arguments are a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>. The output is the composition <span class="Math">\mu: B \rightarrow \mathrm{Pushout}(D)</span> of <span class="Math">\beta_1</span> and the <span class="Math">1</span>-st injection <span class="Math">\iota_1: I_1 \rightarrow \mathrm{Pushout}( D )</span>.</p>

<p><a id="X7D3DAF80816918A4" name="X7D3DAF80816918A4"></a></p>

<h5>6.12-10 MorphismFromSourceToPushoutWithGivenPushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromSourceToPushoutWithGivenPushout</code>( <var class="Arg">D</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( B, I )</span>.</p>

<p>The arguments are a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span> and an object <span class="Math">I = \mathrm{Pushout}(D)</span>. The output is the composition <span class="Math">\mu: B \rightarrow I</span> of <span class="Math">\beta_1</span> and the <span class="Math">1</span>-st injection <span class="Math">\iota_1: I_1 \rightarrow I</span>.</p>

<p><a id="X84F299F47BFB39F8" name="X84F299F47BFB39F8"></a></p>

<h5>6.12-11 UniversalMorphismFromPushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromPushout</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{Pushout}(D), T )</span></p>

<p>The arguments are a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>, a test object <span class="Math">T</span>, and a list of morphisms <span class="Math">\tau = ( \tau_i: I_i \rightarrow T )_{i = 1 \dots n}</span> such that <span class="Math">\tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): \mathrm{Pushout}(D) \rightarrow T</span> given by the universal property of the pushout.</p>

<p><a id="X7E3C69767F1C3B30" name="X7E3C69767F1C3B30"></a></p>

<h5>6.12-12 UniversalMorphismFromPushoutWithGivenPushout</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromPushoutWithGivenPushout</code>( <var class="Arg">D</var>, <var class="Arg">T</var>, <var class="Arg">tau</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( I, T )</span></p>

<p>The arguments are a list of morphisms <span class="Math">D = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>, a test object <span class="Math">T</span>, a list of morphisms <span class="Math">\tau = ( \tau_i: I_i \rightarrow T )_{i = 1 \dots n}</span> such that <span class="Math">\tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j</span>, and an object <span class="Math">I = \mathrm{Pushout}(D)</span>. For convenience, the test object <var class="Arg">T</var> can be omitted and is automatically derived from <var class="Arg">tau</var> in that case. The output is the morphism <span class="Math">u( \tau ): I \rightarrow T</span> given by the universal property of the pushout.</p>

<p><a id="X80494AF087F5DE4B" name="X80494AF087F5DE4B"></a></p>

<h5>6.12-13 PushoutFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ PushoutFunctorial</code>( <var class="Arg">Ls</var>, <var class="Arg">Lm</var>, <var class="Arg">Lr</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{Pushout}( ( \beta_i )_{i=1}^n ), \mathrm{Pushout}( ( \beta_i' )_{i=1}^n ))</span></p>

<p>The arguments are three lists of morphisms <span class="Math">L_s = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>, <span class="Math">L_m = ( \mu_i: I_i \rightarrow I_i' )_{i = 1 \dots n}</span>, <span class="Math">L_r = ( \beta_i': B' \rightarrow I_i' )_{i = 1 \dots n}</span> having the same length <span class="Math">n</span> such that there exists a morphism <span class="Math">\beta: B \rightarrow B'</span> such that <span class="Math">\beta_i' \circ \beta \sim_{B, I_i'} \mu_i \circ \beta_i</span> for <span class="Math">i = 1, \dots n</span>. The output is the morphism <span class="Math">\mathrm{Pushout}( ( \beta_i )_{i=1}^n ) \rightarrow \mathrm{Pushout}( ( \beta_i' )_{i=1}^n )</span> given by the functoriality of the pushout.</p>

<p><a id="X7DAF60808113D76B" name="X7DAF60808113D76B"></a></p>

<h5>6.12-14 PushoutFunctorialWithGivenPushouts</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ PushoutFunctorialWithGivenPushouts</code>( <var class="Arg">s</var>, <var class="Arg">Ls</var>, <var class="Arg">Lm</var>, <var class="Arg">Lr</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(s, r)</span></p>

<p>The arguments are an object <span class="Math">s = \mathrm{Pushout}( ( \beta_i )_{i=1}^n )</span>, three lists of morphisms <span class="Math">L_s = ( \beta_i: B \rightarrow I_i )_{i = 1 \dots n}</span>, <span class="Math">L_m = ( \mu_i: I_i \rightarrow I_i' )_{i = 1 \dots n}</span>, <span class="Math">L_r = ( \beta_i': B' \rightarrow I_i' )_{i = 1 \dots n}</span> having the same length <span class="Math">n</span> such that there exists a morphism <span class="Math">\beta: B \rightarrow B'</span> such that <span class="Math">\beta_i' \circ \beta \sim_{B, I_i'} \mu_i \circ \beta_i</span> for <span class="Math">i = 1, \dots n</span>, and an object <span class="Math">r = \mathrm{Pushout}( ( \beta_i' )_{i=1}^n )</span>. The output is the morphism <span class="Math">s \rightarrow r</span> given by the functoriality of the pushout.</p>

<p><a id="X87F4D35A826599C6" name="X87F4D35A826599C6"></a></p>

<h4>6.13 <span class="Heading">Image</span></h4>

<p>For a given morphism <span class="Math">\alpha: A \rightarrow B</span>, an image of <span class="Math">\alpha</span> consists of four parts:</p>


<ul>
<li><p>an object <span class="Math">I</span>,</p>

</li>
<li><p>a morphism <span class="Math">c: A \rightarrow I</span>,</p>

</li>
<li><p>a monomorphism <span class="Math">\iota: I \hookrightarrow B</span> such that <span class="Math">\iota \circ c \sim_{A,B} \alpha</span>,</p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each pair of morphisms <span class="Math">\tau = ( \tau_1: A \rightarrow T, \tau_2: T \hookrightarrow B )</span> where <span class="Math">\tau_2</span> is a monomorphism such that <span class="Math">\tau_2 \circ \tau_1 \sim_{A,B} \alpha</span> to a morphism <span class="Math">u(\tau): I \rightarrow T</span> such that <span class="Math">\tau_2 \circ u(\tau) \sim_{I,B} \iota</span> and <span class="Math">u(\tau) \circ c \sim_{A,T} \tau_1</span>.</p>

</li>
</ul>
<p>The <span class="Math">4</span>-tuple <span class="Math">( I, c, \iota, u )</span> is called an <em>image</em> of <span class="Math">\alpha</span> if the morphisms <span class="Math">u( \tau )</span> are uniquely determined up to congruence of morphisms. We denote the object <span class="Math">I</span> of such a <span class="Math">4</span>-tuple by <span class="Math">\mathrm{im}(\alpha)</span>. We say that the morphism <span class="Math">u( \tau )</span> is induced by the <em>universal property of the image</em>.</p>

<p><a id="X80490BD785CA695A" name="X80490BD785CA695A"></a></p>

<h5>6.13-1 IsomorphismFromImageObjectToKernelOfCokernel</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromImageObjectToKernelOfCokernel</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{im}(\alpha), \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ) )</span></p>

<p>The argument is a morphism <span class="Math">\alpha</span>. The output is the canonical morphism <span class="Math">\mathrm{im}(\alpha) \rightarrow \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) )</span>.</p>

<p><a id="X7CAA3342865B456B" name="X7CAA3342865B456B"></a></p>

<h5>6.13-2 IsomorphismFromKernelOfCokernelToImageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromKernelOfCokernelToImageObject</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ), \mathrm{im}(\alpha) )</span></p>

<p>The argument is a morphism <span class="Math">\alpha</span>. The output is the canonical morphism <span class="Math">\mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ) \rightarrow \mathrm{im}(\alpha)</span>.</p>

<p><a id="X83B457FF79AC5AC6" name="X83B457FF79AC5AC6"></a></p>

<h5>6.13-3 ImageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ImageObject</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a morphism <span class="Math">\alpha</span>. The output is the image <span class="Math">\mathrm{im}( \alpha )</span>.</p>

<p><a id="X86CEE2D1876EC2B9" name="X86CEE2D1876EC2B9"></a></p>

<h5>6.13-4 ImageEmbedding</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ImageEmbedding</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{im}(\alpha), B)</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the image embedding <span class="Math">\iota: \mathrm{im}(\alpha) \hookrightarrow B</span>.</p>

<p><a id="X82991FA17B460744" name="X82991FA17B460744"></a></p>

<h5>6.13-5 ImageEmbeddingWithGivenImageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ImageEmbeddingWithGivenImageObject</code>( <var class="Arg">alpha</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(I, B)</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span> and an object <span class="Math">I = \mathrm{im}( \alpha )</span>. The output is the image embedding <span class="Math">\iota: I \hookrightarrow B</span>.</p>

<p><a id="X8144201987A27661" name="X8144201987A27661"></a></p>

<h5>6.13-6 CoastrictionToImage</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoastrictionToImage</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, \mathrm{im}( \alpha ))</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the coastriction to image <span class="Math">c: A \rightarrow \mathrm{im}( \alpha )</span>.</p>

<p><a id="X78BE36EA83BEF493" name="X78BE36EA83BEF493"></a></p>

<h5>6.13-7 CoastrictionToImageWithGivenImageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoastrictionToImageWithGivenImageObject</code>( <var class="Arg">alpha</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, I)</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span> and an object <span class="Math">I = \mathrm{im}( \alpha )</span>. The output is the coastriction to image <span class="Math">c: A \rightarrow I</span>.</p>

<p><a id="X7989B1FB811D2033" name="X7989B1FB811D2033"></a></p>

<h5>6.13-8 UniversalMorphismFromImage</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromImage</code>( <var class="Arg">alpha</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{im}(\alpha), T)</span></p>

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

<p><a id="X86E557097CFB4430" name="X86E557097CFB4430"></a></p>

<h5>6.13-9 UniversalMorphismFromImageWithGivenImageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismFromImageWithGivenImageObject</code>( <var class="Arg">alpha</var>, <var class="Arg">tau</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(I, T)</span></p>

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

<p><a id="X7A46647F7AA9C398" name="X7A46647F7AA9C398"></a></p>

<h5>6.13-10 ImageObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ImageObjectFunctorial</code>( <var class="Arg">alpha</var>, <var class="Arg">nu</var>, <var class="Arg">alpha_prime</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{ImageObject}( \alpha ), \mathrm{ImageObject}( \alpha' ) )</span></p>

<p>The arguments are three morphisms <span class="Math">\alpha: A \rightarrow B</span>, <span class="Math">\nu: B \rightarrow B'</span>, <span class="Math">\alpha': A' \rightarrow B'</span>. The output is the morphism <span class="Math">\mathrm{ImageObject}( \alpha ) \rightarrow \mathrm{ImageObject}( \alpha' )</span> given by the functoriality of the image.</p>

<p><a id="X85F174A07A09B04C" name="X85F174A07A09B04C"></a></p>

<h5>6.13-11 ImageObjectFunctorialWithGivenImageObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ImageObjectFunctorialWithGivenImageObjects</code>( <var class="Arg">s</var>, <var class="Arg">alpha</var>, <var class="Arg">nu</var>, <var class="Arg">alpha_prime</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( s, r )</span></p>

<p>The arguments are an object <span class="Math">s = \mathrm{ImageObject}( \alpha )</span>, three morphisms <span class="Math">\alpha: A \rightarrow B</span>, <span class="Math">\nu: B \rightarrow B'</span>, <span class="Math">\alpha': A' \rightarrow B'</span>, and an object <span class="Math">r = \mathrm{ImageObject}( \alpha' )</span>. The output is the morphism <span class="Math">\mathrm{ImageObject}( \alpha ) \rightarrow \mathrm{ImageObject}( \alpha' )</span> given by the functoriality of the image.</p>

<p><a id="X7EB02EC487B586E5" name="X7EB02EC487B586E5"></a></p>

<h4>6.14 <span class="Heading">Coimage</span></h4>

<p>For a given morphism <span class="Math">\alpha: A \rightarrow B</span>, a coimage of <span class="Math">\alpha</span> consists of four parts:</p>


<ul>
<li><p>an object <span class="Math">C</span>,</p>

</li>
<li><p>an epimorphism <span class="Math">\pi: A \twoheadrightarrow C</span>,</p>

</li>
<li><p>a morphism <span class="Math">a: C \rightarrow B</span> such that <span class="Math">a \circ \pi \sim_{A,B} \alpha</span>,</p>

</li>
<li><p>a dependent function <span class="Math">u</span> mapping each pair of morphisms <span class="Math">\tau = ( \tau_1: A \twoheadrightarrow T, \tau_2: T \rightarrow B )</span> where <span class="Math">\tau_1</span> is an epimorphism such that <span class="Math">\tau_2 \circ \tau_1 \sim_{A,B} \alpha</span> to a morphism <span class="Math">u(\tau): T \rightarrow C</span> such that <span class="Math">u( \tau ) \circ \tau_1 \sim_{A,C} \pi</span> and <span class="Math">a \circ u( \tau ) \sim_{T,B} \tau_2</span>.</p>

</li>
</ul>
<p>The <span class="Math">4</span>-tuple <span class="Math">( C, \pi, a, u )</span> is called a <em>coimage</em> of <span class="Math">\alpha</span> if the morphisms <span class="Math">u( \tau )</span> are uniquely determined up to congruence of morphisms. We denote the object <span class="Math">C</span> of such a <span class="Math">4</span>-tuple by <span class="Math">\mathrm{coim}(\alpha)</span>. We say that the morphism <span class="Math">u( \tau )</span> is induced by the <em>universal property of the coimage</em>.</p>

<p><a id="X7C594E227D8DB0ED" name="X7C594E227D8DB0ED"></a></p>

<h5>6.14-1 IsomorphismFromCoimageToCokernelOfKernel</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromCoimageToCokernelOfKernel</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{coim}( \alpha ), \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ) )</span>.</p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the canonical morphism <span class="Math">\mathrm{coim}( \alpha ) \rightarrow \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) )</span>.</p>

<p><a id="X7CF7E7E47A460E56" name="X7CF7E7E47A460E56"></a></p>

<h5>6.14-2 IsomorphismFromCokernelOfKernelToCoimage</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromCokernelOfKernelToCoimage</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ), \mathrm{coim}( \alpha ) )</span>.</p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the canonical morphism <span class="Math">\mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ) \rightarrow \mathrm{coim}( \alpha )</span>.</p>

<p><a id="X82318F9B876ACB1A" name="X82318F9B876ACB1A"></a></p>

<h5>6.14-3 CoimageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoimageObject</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is a morphism <span class="Math">\alpha</span>. The output is the coimage <span class="Math">\mathrm{coim}( \alpha )</span>.</p>

<p><a id="X788E717C7CCC6645" name="X788E717C7CCC6645"></a></p>

<h5>6.14-4 CoimageProjection</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoimageProjection</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, \mathrm{coim}( \alpha ))</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the coimage projection <span class="Math">\pi: A \twoheadrightarrow \mathrm{coim}( \alpha )</span>.</p>

<p><a id="X836301DF80A22C5C" name="X836301DF80A22C5C"></a></p>

<h5>6.14-5 CoimageProjectionWithGivenCoimageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoimageProjectionWithGivenCoimageObject</code>( <var class="Arg">alpha</var>, <var class="Arg">C</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(A, C)</span></p>

<p>The arguments are a morphism <span class="Math">\alpha: A \rightarrow B</span> and an object <span class="Math">C = \mathrm{coim}(\alpha)</span>. The output is the coimage projection <span class="Math">\pi: A \twoheadrightarrow C</span>.</p>

<p><a id="X805108BF8047357E" name="X805108BF8047357E"></a></p>

<h5>6.14-6 AstrictionToCoimage</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ AstrictionToCoimage</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{coim}( \alpha ),B)</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the astriction to coimage <span class="Math">a: \mathrm{coim}( \alpha ) \rightarrow B</span>.</p>

<p><a id="X78AC1C7384A60A5E" name="X78AC1C7384A60A5E"></a></p>

<h5>6.14-7 AstrictionToCoimageWithGivenCoimageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ AstrictionToCoimageWithGivenCoimageObject</code>( <var class="Arg">alpha</var>, <var class="Arg">C</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(C,B)</span></p>

<p>The argument are a morphism <span class="Math">\alpha: A \rightarrow B</span> and an object <span class="Math">C = \mathrm{coim}( \alpha )</span>. The output is the astriction to coimage <span class="Math">a: C \rightarrow B</span>.</p>

<p><a id="X7D051DDF7A68BFFB" name="X7D051DDF7A68BFFB"></a></p>

<h5>6.14-8 UniversalMorphismIntoCoimage</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoCoimage</code>( <var class="Arg">alpha</var>, <var class="Arg">tau</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(T, \mathrm{coim}( \alpha ))</span></p>

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

<p><a id="X87AACC0083B6D49F" name="X87AACC0083B6D49F"></a></p>

<h5>6.14-9 UniversalMorphismIntoCoimageWithGivenCoimageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ UniversalMorphismIntoCoimageWithGivenCoimageObject</code>( <var class="Arg">alpha</var>, <var class="Arg">tau</var>, <var class="Arg">C</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(T, C)</span></p>

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

<p>Whenever the <code class="code">CoastrictionToImage</code> is an epi, or the <code class="code">AstrictionToCoimage</code> is a mono, there is a canonical morphism from the image to the coimage. If this canonical morphism is an isomorphism, we call it the <em>canonical identification</em> (between image and coimage).</p>

<p><a id="X852EFBA87E7F6831" name="X852EFBA87E7F6831"></a></p>

<h5>6.14-10 CoimageObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoimageObjectFunctorial</code>( <var class="Arg">alpha</var>, <var class="Arg">mu</var>, <var class="Arg">alpha_prime</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{CoimageObject}( \alpha ), \mathrm{CoimageObject}( \alpha' ))</span></p>

<p>The arguments are three morphisms <span class="Math">\alpha: A \rightarrow B, \mu: A \rightarrow A', \alpha': A' \rightarrow B'</span>. The output is the morphism <span class="Math">\mathrm{CoimageObject}( \alpha ) \rightarrow \mathrm{CoimageObject}( \alpha' )</span> given by the functoriality of the coimage.</p>

<p><a id="X7FB58F087D65DB38" name="X7FB58F087D65DB38"></a></p>

<h5>6.14-11 CoimageObjectFunctorialWithGivenCoimageObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ CoimageObjectFunctorialWithGivenCoimageObjects</code>( <var class="Arg">s</var>, <var class="Arg">alpha</var>, <var class="Arg">mu</var>, <var class="Arg">alpha_prime</var>, <var class="Arg">r</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(s, r)</span></p>

<p>The arguments are an object <span class="Math">s = \mathrm{CoimageObject}( \alpha )</span>, three morphisms <span class="Math">\alpha: A \rightarrow B, \mu: A \rightarrow A', \alpha': A' \rightarrow B'</span>, and an object <span class="Math">r = \mathrm{CoimageObject}( \alpha' )</span>. The output is the morphism <span class="Math">\mathrm{CoimageObject}( \alpha ) \rightarrow \mathrm{CoimageObject}( \alpha' )</span> given by the functoriality of the coimage.</p>

<p><a id="X8047F7C57B874495" name="X8047F7C57B874495"></a></p>

<h4>6.15 <span class="Heading">Morphism between Coimage and Image</span></h4>

<p><a id="X7F7BD6A18581671E" name="X7F7BD6A18581671E"></a></p>

<h5>6.15-1 MorphismFromCoimageToImage</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromCoimageToImage</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{coim}(\alpha), \mathrm{im}(\alpha))</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the canonical morphism (in a preabelian category) <span class="Math">\mathrm{coim}(\alpha) \rightarrow \mathrm{im}(\alpha)</span>.</p>

<p><a id="X8025749B78E12A2B" name="X8025749B78E12A2B"></a></p>

<h5>6.15-2 MorphismFromCoimageToImageWithGivenObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MorphismFromCoimageToImageWithGivenObjects</code>( <var class="Arg">C</var>, <var class="Arg">alpha</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(C,I)</span></p>

<p>The argument is an object <span class="Math">C = \mathrm{coim}(\alpha)</span>, a morphism <span class="Math">\alpha: A \rightarrow B</span>, and an object <span class="Math">I = \mathrm{im}(\alpha)</span>. The output is the canonical morphism (in a preabelian category) <span class="Math">C \rightarrow I</span>.</p>

<p><a id="X86692249870B0EC6" name="X86692249870B0EC6"></a></p>

<h5>6.15-3 InverseOfMorphismFromCoimageToImage</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InverseOfMorphismFromCoimageToImage</code>( <var class="Arg">alpha</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(\mathrm{im}(\alpha), \mathrm{coim}(\alpha))</span></p>

<p>The argument is a morphism <span class="Math">\alpha: A \rightarrow B</span>. The output is the inverse of the canonical morphism (in an abelian category) <span class="Math">\mathrm{im}(\alpha) \rightarrow \mathrm{coim}(\alpha)</span>.</p>

<p><a id="X7B32041F7C9427E4" name="X7B32041F7C9427E4"></a></p>

<h5>6.15-4 InverseOfMorphismFromCoimageToImageWithGivenObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InverseOfMorphismFromCoimageToImageWithGivenObjects</code>( <var class="Arg">I</var>, <var class="Arg">alpha</var>, <var class="Arg">C</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}(I,C)</span></p>

<p>The argument is an object <span class="Math">C = \mathrm{coim}(\alpha)</span>, a morphism <span class="Math">\alpha: A \rightarrow B</span>, and an object <span class="Math">I = \mathrm{im}(\alpha)</span>. The output is the inverse of the canonical morphism (in an abelian category) <span class="Math">I \rightarrow C</span>.</p>

<p><a id="X87F38F8284D3137C" name="X87F38F8284D3137C"></a></p>

<h4>6.16 <span class="Heading">Homology objects</span></h4>

<p>In an abelian category, we can define the operation that takes as an input a pair of morphisms <span class="Math">\alpha: A \rightarrow B</span>, <span class="Math">\beta: B \rightarrow C</span> and outputs the subquotient of <span class="Math">B</span> given by</p>


<ul>
<li><p><span class="Math">H := \mathrm{KernelObject}( \beta )/ (\mathrm{KernelObject}( \beta ) \cap \mathrm{ImageObject( \alpha )}</span>).</p>

</li>
</ul>
<p>This object is called a <em>homology object</em> of the pair <span class="Math">\alpha, \beta</span>. Note that we do not need the precomposition of <span class="Math">\alpha</span> and <span class="Math">\beta</span> to be zero in order to make sense of this notion. Moreover, given a second pair <span class="Math">\gamma: D \rightarrow E</span>, <span class="Math">\delta: E \rightarrow F</span> of morphisms, and a morphism <span class="Math">\epsilon: B \rightarrow E</span> such that there exists <span class="Math">\omega_1: A \rightarrow D</span>, <span class="Math">\omega_2: C \rightarrow F</span> with <span class="Math">\epsilon \circ \alpha \sim_{A,E} \gamma \circ \omega_1</span> and <span class="Math">\omega_2 \circ \beta \sim_{B,F} \delta \circ \epsilon</span> there is a functorial way to obtain from these data a morphism between the two corresponding homology objects.</p>

<p><a id="X8713652D7B7E1418" name="X8713652D7B7E1418"></a></p>

<h5>6.16-1 HomologyObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ HomologyObject</code>( <var class="Arg">alpha</var>, <var class="Arg">beta</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an object</p>

<p>The arguments are two morphisms <span class="Math">\alpha: A \rightarrow B, \beta: B \rightarrow C</span>. The output is the homology object <span class="Math">H</span> of this pair.</p>

<p><a id="X8647C62283C9B921" name="X8647C62283C9B921"></a></p>

<h5>6.16-2 HomologyObjectFunctorial</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ HomologyObjectFunctorial</code>( <var class="Arg">alpha</var>, <var class="Arg">beta</var>, <var class="Arg">epsilon</var>, <var class="Arg">gamma</var>, <var class="Arg">delta</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( H_1, H_2 )</span></p>

<p>The argument are five morphisms <span class="Math">\alpha: A \rightarrow B</span>, <span class="Math">\beta: B \rightarrow C</span>, <span class="Math">\epsilon: B \rightarrow E</span>, <span class="Math">\gamma: D \rightarrow E, \delta: E \rightarrow F</span> such that there exists <span class="Math">\omega_1: A \rightarrow D</span>, <span class="Math">\omega_2: C \rightarrow F</span> with <span class="Math">\epsilon \circ \alpha \sim_{A,E} \gamma \circ \omega_1</span> and <span class="Math">\omega_2 \circ \beta \sim_{B,F} \delta \circ \epsilon</span>. The output is the functorial morphism induced by <span class="Math">\epsilon</span> between the corresponding homology objects <span class="Math">H_1</span> and <span class="Math">H_2</span>, where <span class="Math">H_1</span> denotes the homology object of the pair <span class="Math">\alpha, \beta</span>, and <span class="Math">H_2</span> denotes the homology object of the pair <span class="Math">\gamma, \delta</span>.</p>

<p><a id="X81012CC0845DE717" name="X81012CC0845DE717"></a></p>

<h5>6.16-3 HomologyObjectFunctorialWithGivenHomologyObjects</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ HomologyObjectFunctorialWithGivenHomologyObjects</code>( <var class="Arg">H_1</var>, <var class="Arg">L</var>, <var class="Arg">H_2</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( H_1, H_2 )</span></p>

<p>The arguments are an object <span class="Math">H_1</span>, a list <span class="Math">L</span> consisting of five morphisms <span class="Math">\alpha: A \rightarrow B</span>, <span class="Math">\beta: B \rightarrow C</span>, <span class="Math">\epsilon: B \rightarrow E</span>, <span class="Math">\gamma: D \rightarrow E, \delta: E \rightarrow F</span>, and an object <span class="Math">H_2</span>, such that <span class="Math">H_1 = \mathrm{HomologyObject}( \alpha, \beta )</span> and <span class="Math">H_2 = \mathrm{HomologyObject}( \gamma, \delta )</span>, and such that there exists <span class="Math">\omega_1: A \rightarrow D</span>, <span class="Math">\omega_2: C \rightarrow F</span> with <span class="Math">\epsilon \circ \alpha \sim_{A,E} \gamma \circ \omega_1</span> and <span class="Math">\omega_2 \circ \beta \sim_{B,F} \delta \circ \epsilon</span>. The output is the functorial morphism induced by <span class="Math">\epsilon</span> between the corresponding homology objects <span class="Math">H_1</span> and <span class="Math">H_2</span>, where <span class="Math">H_1</span> denotes the homology object of the pair <span class="Math">\alpha, \beta</span>, and <span class="Math">H_2</span> denotes the homology object of the pair <span class="Math">\gamma, \delta</span>.</p>

<p><a id="X8799E88E79EFE007" name="X8799E88E79EFE007"></a></p>

<h5>6.16-4 IsomorphismFromHomologyObjectToItsConstructionAsAnImageObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromHomologyObjectToItsConstructionAsAnImageObject</code>( <var class="Arg">alpha</var>, <var class="Arg">beta</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( \mathrm{HomologyObject}( \alpha, \beta ), I )</span></p>

<p>The arguments are two morphisms <span class="Math">\alpha: A \rightarrow B, \beta: B \rightarrow C</span>. The output is the natural isomorphism from the homology object <span class="Math">H</span> of <span class="Math">\alpha</span> and <span class="Math">\beta</span> to the construction of the homology object as <span class="Math">\mathrm{ImageObject}( \mathrm{PreCompose}( \mathrm{KernelEmbedding}( \beta ), \mathrm{CokernelProjection}( \alpha ) ) )</span>, denoted by <span class="Math">I</span>.</p>

<p><a id="X828E94BA7CF6FB71" name="X828E94BA7CF6FB71"></a></p>

<h5>6.16-5 IsomorphismFromItsConstructionAsAnImageObjectToHomologyObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ IsomorphismFromItsConstructionAsAnImageObjectToHomologyObject</code>( <var class="Arg">alpha</var>, <var class="Arg">beta</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a morphism in <span class="Math">\mathrm{Hom}( I, \mathrm{HomologyObject}( \alpha, \beta ) )</span></p>

<p>The arguments are two morphisms <span class="Math">\alpha: A \rightarrow B, \beta: B \rightarrow C</span>. The output is the natural isomorphism from the construction of the homology object as <span class="Math">\mathrm{ImageObject}( \mathrm{PreCompose}( \mathrm{KernelEmbedding}( \beta ), \mathrm{CokernelProjection}( \alpha ) ) )</span>, denoted by <span class="Math">I</span>, to the homology object <span class="Math">H</span> of <span class="Math">\alpha</span> and <span class="Math">\beta</span>.</p>

<p><a id="X81E4AE0B7876230B" name="X81E4AE0B7876230B"></a></p>

<h4>6.17 <span class="Heading">Projective covers and injective envelopes</span></h4>

<p><a id="X790C931979343CFF" name="X790C931979343CFF"></a></p>

<h5>6.17-1 ProjectiveCoverObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ ProjectiveCoverObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is an object <span class="Math">A</span>. The output is a projective cover of <span class="Math">A</span>.</p>

<p><a id="X851836CC829092D9" name="X851836CC829092D9"></a></p>

<h5>6.17-2 EpimorphismFromProjectiveCoverObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ EpimorphismFromProjectiveCoverObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an epimorphism</p>

<p>The argument is an object <span class="Math">A</span>. The output is an epimorphism from a projective cover of <span class="Math">A</span>.</p>

<p><a id="X7C9F2CC480C7DA1D" name="X7C9F2CC480C7DA1D"></a></p>

<h5>6.17-3 EpimorphismFromProjectiveCoverObjectWithGivenProjectiveCoverObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ EpimorphismFromProjectiveCoverObjectWithGivenProjectiveCoverObject</code>( <var class="Arg">A</var>, <var class="Arg">P</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: an epimorphism</p>

<p>The argument is an object <span class="Math">A</span>. The output is the epimorphism from the projective cover <span class="Math">P</span> of <span class="Math">A</span>.</p>

<p><a id="X791CA23A8401BF2F" name="X791CA23A8401BF2F"></a></p>

<h5>6.17-4 InjectiveEnvelopeObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ InjectiveEnvelopeObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: an object</p>

<p>The argument is an object <span class="Math">A</span>. The output is an injective envelope of <span class="Math">A</span>.</p>

<p><a id="X879A01DD7DC8AB13" name="X879A01DD7DC8AB13"></a></p>

<h5>6.17-5 MonomorphismIntoInjectiveEnvelopeObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MonomorphismIntoInjectiveEnvelopeObject</code>( <var class="Arg">A</var> )</td><td class="tdright">( attribute )</td></tr></table></div>
<p>Returns: a monomorphism</p>

<p>The argument is an object <span class="Math">A</span>. The output is a monomorphism into an injective envelope of <span class="Math">A</span>.</p>

<p><a id="X781E3ED78574B379" name="X781E3ED78574B379"></a></p>

<h5>6.17-6 MonomorphismIntoInjectiveEnvelopeObjectWithGivenInjectiveEnvelopeObject</h5>

<div class="func"><table class="func" width="100%"><tr><td class="tdleft"><code class="func">‣ MonomorphismIntoInjectiveEnvelopeObjectWithGivenInjectiveEnvelopeObject</code>( <var class="Arg">A</var>, <var class="Arg">I</var> )</td><td class="tdright">( operation )</td></tr></table></div>
<p>Returns: a monomorphism</p>

<p>The argument is an object <span class="Math">A</span>. The output is a monomorphism into an injective envelope <span class="Math">I</span> of <span class="Math">A</span>.</p>


<div class="chlinkprevnextbot"> <a href="chap0.html">[Top of Book]</a>   <a href="chap0.html#contents">[Contents]</a>    <a href="chap5.html">[Previous Chapter]</a>    <a href="chap7.html">[Next Chapter]</a>   </div>


<div class="chlinkbot"><span class="chlink1">Goto Chapter: </span><a href="chap0.html">Top</a>  <a href="chap1.html">1</a>  <a href="chap2.html">2</a>  <a href="chap3.html">3</a>  <a href="chap4.html">4</a>  <a href="chap5.html">5</a>  <a href="chap6.html">6</a>  <a href="chap7.html">7</a>  <a href="chap8.html">8</a>  <a href="chap9.html">9</a>  <a href="chap10.html">10</a>  <a href="chap11.html">11</a>  <a href="chap12.html">12</a>  <a href="chap13.html">13</a>  <a href="chap14.html">14</a>  <a href="chap15.html">15</a>  <a href="chap16.html">16</a>  <a href="chap17.html">17</a>  <a href="chap18.html">18</a>  <a href="chapInd.html">Ind</a>  </div>

<hr />
<p class="foot">generated by <a href="https://www.math.rwth-aachen.de/~Frank.Luebeck/GAPDoc">GAPDoc2HTML</a></p>
</body>
</html>

Messung V0.5 in Prozent
C=100 H=100 G=100

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.75Angebot  (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤

*Eine klare Vorstellung vom Zielzustand




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.