Deploying to gh-pages from @ 3306f5b 🚀

Author: mortberg

Cubical.Algebra.AbGroup.Base.html

@@ -155,7 +155,7 @@
                 <a id="4938" class="Symbol">→</a> <a id="4940" href="Cubical.Foundations.Prelude.html#15524" class="Function">isProp</a> <a id="4947" class="Symbol">(</a><a id="4948" href="Cubical.Algebra.AbGroup.Base.html#933" class="Record">IsAbGroup</a> <a id="4958" href="Cubical.Algebra.AbGroup.Base.html#4883" class="Bound">0g</a> <a id="4961" href="Cubical.Algebra.AbGroup.Base.html#4892" class="Bound Operator">_+_</a> <a id="4965" class="Symbol">(</a><a id="4966" href="Cubical.Algebra.AbGroup.Base.html#4910" class="Bound Operator">-_</a><a id="4968" class="Symbol">))</a>
 <a id="4971" href="Cubical.Algebra.AbGroup.Base.html#4851" class="Function">isPropIsAbGroup</a> <a id="4987" href="Cubical.Algebra.AbGroup.Base.html#4987" class="Bound">0g</a> <a id="4990" href="Cubical.Algebra.AbGroup.Base.html#4990" class="Bound Operator">_+_</a> <a id="4994" href="Cubical.Algebra.AbGroup.Base.html#4994" class="Bound Operator">-_</a> <a id="4997" class="Symbol">=</a>
   <a id="5001" href="Cubical.Foundations.HLevels.html#9379" class="Function">isOfHLevelRetractFromIso</a> <a id="5026" class="Number">1</a> <a id="5028" href="Cubical.Algebra.AbGroup.Base.html#1433" class="Function">IsAbGroupIsoΣ</a>
-    <a id="5046" class="Symbol">(</a><a id="5047" href="Cubical.Foundations.HLevels.html#12907" class="Function">isPropΣ</a> <a id="5055" class="Symbol">(</a><a id="5056" href="Cubical.Algebra.Group.Properties.html#471" class="Function">isPropIsGroup</a> <a id="5070" href="Cubical.Algebra.AbGroup.Base.html#4987" class="Bound">0g</a> <a id="5073" href="Cubical.Algebra.AbGroup.Base.html#4990" class="Bound Operator">_+_</a> <a id="5077" class="Symbol">(</a><a id="5078" href="Cubical.Algebra.AbGroup.Base.html#4994" class="Bound Operator">-_</a><a id="5080" class="Symbol">))</a>
+    <a id="5046" class="Symbol">(</a><a id="5047" href="Cubical.Foundations.HLevels.html#12907" class="Function">isPropΣ</a> <a id="5055" class="Symbol">(</a><a id="5056" href="Cubical.Algebra.Group.Properties.html#515" class="Function">isPropIsGroup</a> <a id="5070" href="Cubical.Algebra.AbGroup.Base.html#4987" class="Bound">0g</a> <a id="5073" href="Cubical.Algebra.AbGroup.Base.html#4990" class="Bound Operator">_+_</a> <a id="5077" class="Symbol">(</a><a id="5078" href="Cubical.Algebra.AbGroup.Base.html#4994" class="Bound Operator">-_</a><a id="5080" class="Symbol">))</a>
              <a id="5096" class="Symbol">(λ</a> <a id="5099" href="Cubical.Algebra.AbGroup.Base.html#5099" class="Bound">grp</a> <a id="5103" class="Symbol">→</a> <a id="5105" href="Cubical.Foundations.HLevels.html#16972" class="Function">isPropΠ2</a> <a id="5114" class="Symbol">(λ</a> <a id="5117" href="Cubical.Algebra.AbGroup.Base.html#5117" class="Bound">_</a> <a id="5119" href="Cubical.Algebra.AbGroup.Base.html#5119" class="Bound">_</a> <a id="5121" class="Symbol">→</a> <a id="5123" href="Cubical.Algebra.AbGroup.Base.html#5099" class="Bound">grp</a> <a id="5127" class="Symbol">.</a><a id="5128" href="Cubical.Algebra.Semigroup.Base.html#987" class="Field">is-set</a> <a id="5135" class="Symbol">_</a> <a id="5137" class="Symbol">_)))</a>
   <a id="5144" class="Keyword">where</a>
   <a id="5152" class="Keyword">open</a> <a id="5157" href="Cubical.Algebra.Group.Base.html#576" class="Module">IsGroup</a>
@@ -328,7 +328,7 @@
   <a id="10807" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="10811" class="Symbol">(</a><a id="10812" href="Cubical.Algebra.AbGroup.Base.html#10718" class="Function">invHom</a> <a id="10819" class="Symbol">(</a><a id="10820" href="Cubical.Algebra.AbGroup.Base.html#10820" class="Bound">f</a> <a id="10822" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="10824" href="Cubical.Algebra.AbGroup.Base.html#10824" class="Bound">p</a><a id="10825" class="Symbol">))</a> <a id="10828" class="Symbol">=</a>
     <a id="10834" href="Cubical.Algebra.Group.MorphismProperties.html#2383" class="Function">makeIsGroupHom</a>
       <a id="10855" class="Symbol">λ</a> <a id="10857" href="Cubical.Algebra.AbGroup.Base.html#10857" class="Bound">x</a> <a id="10859" href="Cubical.Algebra.AbGroup.Base.html#10859" class="Bound">y</a> <a id="10861" class="Symbol">→</a> <a id="10863" href="Cubical.Foundations.Prelude.html#1407" class="Function">cong</a> <a id="10868" href="Cubical.Algebra.AbGroup.Base.html#10124" class="Function Operator">-B_</a> <a id="10872" class="Symbol">(</a><a id="10873" href="Cubical.Algebra.Group.Morphisms.html#934" class="Field">pres·</a> <a id="10879" href="Cubical.Algebra.AbGroup.Base.html#10824" class="Bound">p</a> <a id="10881" href="Cubical.Algebra.AbGroup.Base.html#10857" class="Bound">x</a> <a id="10883" href="Cubical.Algebra.AbGroup.Base.html#10859" class="Bound">y</a><a id="10884" class="Symbol">)</a>
-            <a id="10898" href="Cubical.Foundations.Prelude.html#3984" class="Function Operator">∙∙</a> <a id="10901" href="Cubical.Algebra.Group.Properties.html#2823" class="Function">GroupTheory.invDistr</a> <a id="10922" class="Symbol">(</a><a id="10923" href="Cubical.Algebra.AbGroup.Base.html#9913" class="Bound">BGr</a> <a id="10927" href="Cubical.Algebra.AbGroup.Base.html#9990" class="Function Operator">*</a><a id="10928" class="Symbol">)</a> <a id="10930" class="Symbol">(</a><a id="10931" href="Cubical.Algebra.AbGroup.Base.html#10820" class="Bound">f</a> <a id="10933" href="Cubical.Algebra.AbGroup.Base.html#10857" class="Bound">x</a><a id="10934" class="Symbol">)</a> <a id="10936" class="Symbol">(</a><a id="10937" href="Cubical.Algebra.AbGroup.Base.html#10820" class="Bound">f</a> <a id="10939" href="Cubical.Algebra.AbGroup.Base.html#10859" class="Bound">y</a><a id="10940" class="Symbol">)</a>
+            <a id="10898" href="Cubical.Foundations.Prelude.html#3984" class="Function Operator">∙∙</a> <a id="10901" href="Cubical.Algebra.Group.Properties.html#2867" class="Function">GroupTheory.invDistr</a> <a id="10922" class="Symbol">(</a><a id="10923" href="Cubical.Algebra.AbGroup.Base.html#9913" class="Bound">BGr</a> <a id="10927" href="Cubical.Algebra.AbGroup.Base.html#9990" class="Function Operator">*</a><a id="10928" class="Symbol">)</a> <a id="10930" class="Symbol">(</a><a id="10931" href="Cubical.Algebra.AbGroup.Base.html#10820" class="Bound">f</a> <a id="10933" href="Cubical.Algebra.AbGroup.Base.html#10857" class="Bound">x</a><a id="10934" class="Symbol">)</a> <a id="10936" class="Symbol">(</a><a id="10937" href="Cubical.Algebra.AbGroup.Base.html#10820" class="Bound">f</a> <a id="10939" href="Cubical.Algebra.AbGroup.Base.html#10859" class="Bound">y</a><a id="10940" class="Symbol">)</a>
             <a id="10954" href="Cubical.Foundations.Prelude.html#3984" class="Function Operator">∙∙</a> <a id="10957" href="Cubical.Algebra.AbGroup.Base.html#10230" class="Function">+CommB</a> <a id="10964" class="Symbol">_</a> <a id="10966" class="Symbol">_</a>
 
   <a id="10971" class="Keyword">open</a> <a id="10976" href="Cubical.Algebra.AbGroup.Base.html#1507" class="Module">AbGroupStr</a>

Cubical.Algebra.AbGroup.FinitePresentation.html

@@ -0,0 +1,42 @@
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Cubical.Algebra.AbGroup.FinitePresentation</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">module</a> <a id="8" href="Cubical.Algebra.AbGroup.FinitePresentation.html" class="Module">Cubical.Algebra.AbGroup.FinitePresentation</a> <a id="51" class="Keyword">where</a>
+
+<a id="58" class="Keyword">open</a> <a id="63" class="Keyword">import</a> <a id="70" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>
+
+<a id="99" class="Keyword">open</a> <a id="104" class="Keyword">import</a> <a id="111" href="Cubical.Data.Nat.html" class="Module">Cubical.Data.Nat</a>
+<a id="128" class="Keyword">open</a> <a id="133" class="Keyword">import</a> <a id="140" href="Cubical.Data.Int.html" class="Module">Cubical.Data.Int</a>
+
+<a id="158" class="Keyword">open</a> <a id="163" class="Keyword">import</a> <a id="170" href="Cubical.HITs.PropositionalTruncation.html" class="Module">Cubical.HITs.PropositionalTruncation</a>
+
+<a id="208" class="Keyword">open</a> <a id="213" class="Keyword">import</a> <a id="220" href="Cubical.Algebra.Group.html" class="Module">Cubical.Algebra.Group</a>
+<a id="242" class="Keyword">open</a> <a id="247" class="Keyword">import</a> <a id="254" href="Cubical.Algebra.Group.Morphisms.html" class="Module">Cubical.Algebra.Group.Morphisms</a>
+<a id="286" class="Keyword">open</a> <a id="291" class="Keyword">import</a> <a id="298" href="Cubical.Algebra.Group.MorphismProperties.html" class="Module">Cubical.Algebra.Group.MorphismProperties</a>
+<a id="339" class="Keyword">open</a> <a id="344" class="Keyword">import</a> <a id="351" href="Cubical.Algebra.AbGroup.html" class="Module">Cubical.Algebra.AbGroup</a>
+<a id="375" class="Keyword">open</a> <a id="380" class="Keyword">import</a> <a id="387" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html" class="Module">Cubical.Algebra.AbGroup.Instances.FreeAbGroup</a>
+
+<a id="434" class="Keyword">open</a> <a id="439" class="Keyword">import</a> <a id="446" href="Cubical.Algebra.Group.QuotientGroup.html" class="Module">Cubical.Algebra.Group.QuotientGroup</a>
+<a id="482" class="Keyword">open</a> <a id="487" class="Keyword">import</a> <a id="494" href="Cubical.Algebra.Group.Subgroup.html" class="Module">Cubical.Algebra.Group.Subgroup</a>
+
+<a id="526" class="Keyword">private</a>
+  <a id="536" class="Keyword">variable</a>
+    <a id="549" href="Cubical.Algebra.AbGroup.FinitePresentation.html#549" class="Generalizable">ℓ</a> <a id="551" class="Symbol">:</a> <a id="553" href="Agda.Primitive.html#742" class="Postulate">Level</a>
+
+<a id="560" class="Keyword">record</a> <a id="FinitePresentation"></a><a id="567" href="Cubical.Algebra.AbGroup.FinitePresentation.html#567" class="Record">FinitePresentation</a> <a id="586" class="Symbol">(</a><a id="587" href="Cubical.Algebra.AbGroup.FinitePresentation.html#587" class="Bound">A</a> <a id="589" class="Symbol">:</a> <a id="591" href="Cubical.Algebra.AbGroup.Base.html#1758" class="Function">AbGroup</a> <a id="599" href="Cubical.Algebra.AbGroup.FinitePresentation.html#549" class="Generalizable">ℓ</a><a id="600" class="Symbol">)</a> <a id="602" class="Symbol">:</a> <a id="604" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="609" href="Cubical.Algebra.AbGroup.FinitePresentation.html#599" class="Bound">ℓ</a> <a id="611" class="Keyword">where</a>
+  <a id="619" class="Keyword">field</a>
+    <a id="FinitePresentation.nGens"></a><a id="629" href="Cubical.Algebra.AbGroup.FinitePresentation.html#629" class="Field">nGens</a> <a id="635" class="Symbol">:</a> <a id="637" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a>
+    <a id="FinitePresentation.nRels"></a><a id="643" href="Cubical.Algebra.AbGroup.FinitePresentation.html#643" class="Field">nRels</a> <a id="649" class="Symbol">:</a> <a id="651" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a>
+    <a id="FinitePresentation.rels"></a><a id="657" href="Cubical.Algebra.AbGroup.FinitePresentation.html#657" class="Field">rels</a> <a id="662" class="Symbol">:</a> <a id="664" href="Cubical.Algebra.AbGroup.Base.html#4235" class="Function">AbGroupHom</a> <a id="675" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#4192" class="Function Operator">ℤ[Fin</a> <a id="681" href="Cubical.Algebra.AbGroup.FinitePresentation.html#643" class="Field">nRels</a> <a id="687" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#4192" class="Function Operator">]</a> <a id="689" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#4192" class="Function Operator">ℤ[Fin</a> <a id="695" href="Cubical.Algebra.AbGroup.FinitePresentation.html#629" class="Field">nGens</a> <a id="701" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#4192" class="Function Operator">]</a>
+    <a id="FinitePresentation.fpiso"></a><a id="707" href="Cubical.Algebra.AbGroup.FinitePresentation.html#707" class="Field">fpiso</a> <a id="713" class="Symbol">:</a> <a id="715" href="Cubical.Algebra.AbGroup.Base.html#4364" class="Function">AbGroupIso</a> <a id="726" href="Cubical.Algebra.AbGroup.FinitePresentation.html#587" class="Bound">A</a> <a id="728" class="Symbol">(</a><a id="729" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#4192" class="Function Operator">ℤ[Fin</a> <a id="735" href="Cubical.Algebra.AbGroup.FinitePresentation.html#629" class="Field">nGens</a> <a id="741" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#4192" class="Function Operator">]</a> <a id="743" href="Cubical.Algebra.AbGroup.Properties.html#2532" class="Function Operator">/Im</a> <a id="747" href="Cubical.Algebra.AbGroup.FinitePresentation.html#657" class="Field">rels</a><a id="751" class="Symbol">)</a>
+
+<a id="isFinitelyPresented"></a><a id="754" href="Cubical.Algebra.AbGroup.FinitePresentation.html#754" class="Function">isFinitelyPresented</a> <a id="774" class="Symbol">:</a> <a id="776" href="Cubical.Algebra.AbGroup.Base.html#1758" class="Function">AbGroup</a> <a id="784" href="Cubical.Algebra.AbGroup.FinitePresentation.html#549" class="Generalizable">ℓ</a> <a id="786" class="Symbol">→</a> <a id="788" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="793" href="Cubical.Algebra.AbGroup.FinitePresentation.html#549" class="Generalizable">ℓ</a>
+<a id="795" href="Cubical.Algebra.AbGroup.FinitePresentation.html#754" class="Function">isFinitelyPresented</a> <a id="815" href="Cubical.Algebra.AbGroup.FinitePresentation.html#815" class="Bound">G</a> <a id="817" class="Symbol">=</a> <a id="819" href="Cubical.HITs.PropositionalTruncation.Base.html#226" class="Datatype Operator">∥</a> <a id="821" href="Cubical.Algebra.AbGroup.FinitePresentation.html#567" class="Record">FinitePresentation</a> <a id="840" href="Cubical.Algebra.AbGroup.FinitePresentation.html#815" class="Bound">G</a> <a id="842" href="Cubical.HITs.PropositionalTruncation.Base.html#226" class="Datatype Operator">∥₁</a>
+
+<a id="846" class="Keyword">open</a> <a id="851" href="Cubical.Algebra.AbGroup.FinitePresentation.html#567" class="Module">FinitePresentation</a>
+<a id="GrIsoPresFinitePresentation"></a><a id="870" href="Cubical.Algebra.AbGroup.FinitePresentation.html#870" class="Function">GrIsoPresFinitePresentation</a> <a id="898" class="Symbol">:</a> <a id="900" class="Symbol">∀</a> <a id="902" class="Symbol">{</a><a id="903" href="Cubical.Algebra.AbGroup.FinitePresentation.html#903" class="Bound">ℓ</a> <a id="905" href="Cubical.Algebra.AbGroup.FinitePresentation.html#905" class="Bound">ℓ&#39;</a><a id="907" class="Symbol">}</a> <a id="909" class="Symbol">{</a><a id="910" href="Cubical.Algebra.AbGroup.FinitePresentation.html#910" class="Bound">A</a> <a id="912" class="Symbol">:</a> <a id="914" href="Cubical.Algebra.AbGroup.Base.html#1758" class="Function">AbGroup</a> <a id="922" href="Cubical.Algebra.AbGroup.FinitePresentation.html#903" class="Bound">ℓ</a><a id="923" class="Symbol">}</a> <a id="925" class="Symbol">{</a><a id="926" href="Cubical.Algebra.AbGroup.FinitePresentation.html#926" class="Bound">B</a> <a id="928" class="Symbol">:</a> <a id="930" href="Cubical.Algebra.AbGroup.Base.html#1758" class="Function">AbGroup</a> <a id="938" href="Cubical.Algebra.AbGroup.FinitePresentation.html#905" class="Bound">ℓ&#39;</a><a id="940" class="Symbol">}</a>
+  <a id="944" class="Symbol">→</a> <a id="946" href="Cubical.Algebra.AbGroup.Base.html#4364" class="Function">AbGroupIso</a> <a id="957" href="Cubical.Algebra.AbGroup.FinitePresentation.html#910" class="Bound">A</a> <a id="959" href="Cubical.Algebra.AbGroup.FinitePresentation.html#926" class="Bound">B</a> <a id="961" class="Symbol">→</a> <a id="963" href="Cubical.Algebra.AbGroup.FinitePresentation.html#567" class="Record">FinitePresentation</a> <a id="982" href="Cubical.Algebra.AbGroup.FinitePresentation.html#910" class="Bound">A</a> <a id="984" class="Symbol">→</a> <a id="986" href="Cubical.Algebra.AbGroup.FinitePresentation.html#567" class="Record">FinitePresentation</a> <a id="1005" href="Cubical.Algebra.AbGroup.FinitePresentation.html#926" class="Bound">B</a>
+<a id="1007" href="Cubical.Algebra.AbGroup.FinitePresentation.html#629" class="Field">nGens</a> <a id="1013" class="Symbol">(</a><a id="1014" href="Cubical.Algebra.AbGroup.FinitePresentation.html#870" class="Function">GrIsoPresFinitePresentation</a> <a id="1042" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1042" class="Bound">abG</a> <a id="1046" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1046" class="Bound">fpA</a><a id="1049" class="Symbol">)</a> <a id="1051" class="Symbol">=</a> <a id="1053" href="Cubical.Algebra.AbGroup.FinitePresentation.html#629" class="Field">nGens</a> <a id="1059" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1046" class="Bound">fpA</a>
+<a id="1063" href="Cubical.Algebra.AbGroup.FinitePresentation.html#643" class="Field">nRels</a> <a id="1069" class="Symbol">(</a><a id="1070" href="Cubical.Algebra.AbGroup.FinitePresentation.html#870" class="Function">GrIsoPresFinitePresentation</a> <a id="1098" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1098" class="Bound">abG</a> <a id="1102" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1102" class="Bound">fpA</a><a id="1105" class="Symbol">)</a> <a id="1107" class="Symbol">=</a> <a id="1109" href="Cubical.Algebra.AbGroup.FinitePresentation.html#643" class="Field">nRels</a> <a id="1115" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1102" class="Bound">fpA</a>
+<a id="1119" href="Cubical.Algebra.AbGroup.FinitePresentation.html#657" class="Field">rels</a> <a id="1124" class="Symbol">(</a><a id="1125" href="Cubical.Algebra.AbGroup.FinitePresentation.html#870" class="Function">GrIsoPresFinitePresentation</a> <a id="1153" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1153" class="Bound">abG</a> <a id="1157" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1157" class="Bound">fpA</a><a id="1160" class="Symbol">)</a> <a id="1162" class="Symbol">=</a> <a id="1164" href="Cubical.Algebra.AbGroup.FinitePresentation.html#657" class="Field">rels</a> <a id="1169" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1157" class="Bound">fpA</a>
+<a id="1173" href="Cubical.Algebra.AbGroup.FinitePresentation.html#707" class="Field">fpiso</a> <a id="1179" class="Symbol">(</a><a id="1180" href="Cubical.Algebra.AbGroup.FinitePresentation.html#870" class="Function">GrIsoPresFinitePresentation</a> <a id="1208" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1208" class="Bound">abG</a> <a id="1212" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1212" class="Bound">fpA</a><a id="1215" class="Symbol">)</a> <a id="1217" class="Symbol">=</a>
+  <a id="1221" href="Cubical.Algebra.Group.MorphismProperties.html#9259" class="Function">compGroupIso</a> <a id="1234" class="Symbol">(</a><a id="1235" href="Cubical.Algebra.Group.MorphismProperties.html#9455" class="Function">invGroupIso</a> <a id="1247" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1208" class="Bound">abG</a><a id="1250" class="Symbol">)</a> <a id="1252" class="Symbol">(</a><a id="1253" href="Cubical.Algebra.AbGroup.FinitePresentation.html#707" class="Field">fpiso</a> <a id="1259" href="Cubical.Algebra.AbGroup.FinitePresentation.html#1212" class="Bound">fpA</a><a id="1262" class="Symbol">)</a>
+</pre></body></html>