Deploying to gh-pages from @ 413de48 🚀

Author: felixwellen

Cubical.Algebra.CommAlgebra.Ideal.html

@@ -6,8 +6,8 @@
 <a id="151" class="Keyword">open</a> <a id="156" class="Keyword">import</a> <a id="163" href="Cubical.Foundations.Powerset.html" class="Module">Cubical.Foundations.Powerset</a>
 
 <a id="193" class="Keyword">open</a> <a id="198" class="Keyword">import</a> <a id="205" href="Cubical.Algebra.CommRing.html" class="Module">Cubical.Algebra.CommRing</a>
-<a id="230" class="Keyword">open</a> <a id="235" class="Keyword">import</a> <a id="242" href="Cubical.Algebra.CommRing.Ideal.html" class="Module">Cubical.Algebra.CommRing.Ideal</a> <a id="273" class="Keyword">renaming</a> <a id="282" class="Symbol">(</a><a id="283" href="Cubical.Algebra.CommRing.Ideal.Base.html#3666" class="Function">IdealsIn</a> <a id="292" class="Symbol">to</a> <a id="295" class="Function">IdealsInCommRing</a><a id="311" class="Symbol">;</a>
-                                                     <a id="366" href="Cubical.Algebra.CommRing.Ideal.Base.html#3853" class="Function">makeIdeal</a> <a id="376" class="Symbol">to</a> <a id="379" class="Function">makeIdealCommRing</a><a id="396" class="Symbol">)</a>
+<a id="230" class="Keyword">open</a> <a id="235" class="Keyword">import</a> <a id="242" href="Cubical.Algebra.CommRing.Ideal.html" class="Module">Cubical.Algebra.CommRing.Ideal</a> <a id="273" class="Keyword">renaming</a> <a id="282" class="Symbol">(</a><a id="283" href="Cubical.Algebra.CommRing.Ideal.Base.html#3842" class="Function">IdealsIn</a> <a id="292" class="Symbol">to</a> <a id="295" class="Function">IdealsInCommRing</a><a id="311" class="Symbol">;</a>
+                                                     <a id="366" href="Cubical.Algebra.CommRing.Ideal.Base.html#4029" class="Function">makeIdeal</a> <a id="376" class="Symbol">to</a> <a id="379" class="Function">makeIdealCommRing</a><a id="396" class="Symbol">)</a>
 <a id="398" class="Keyword">open</a> <a id="403" class="Keyword">import</a> <a id="410" href="Cubical.Algebra.CommAlgebra.html" class="Module">Cubical.Algebra.CommAlgebra</a>
 <a id="438" class="Keyword">open</a> <a id="443" class="Keyword">import</a> <a id="450" href="Cubical.Algebra.Ring.html" class="Module">Cubical.Algebra.Ring</a>
 
@@ -31,8 +31,8 @@
   <a id="949" href="Cubical.Algebra.CommAlgebra.Ideal.html#700" class="Function">makeIdeal</a> <a id="959" class="Symbol">=</a> <a id="961" href="Cubical.Algebra.CommAlgebra.Ideal.html#379" class="Function">makeIdealCommRing</a> <a id="979" class="Symbol">{</a><a id="980" class="Argument">R</a> <a id="982" class="Symbol">=</a> <a id="984" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1005" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1006" class="Symbol">}</a>
 
   <a id="1011" href="Cubical.Algebra.CommAlgebra.Ideal.html#1011" class="Function">0Ideal</a> <a id="1018" class="Symbol">:</a> <a id="1020" href="Cubical.Algebra.CommAlgebra.Ideal.html#593" class="Function">IdealsIn</a>
-  <a id="1031" href="Cubical.Algebra.CommAlgebra.Ideal.html#1011" class="Function">0Ideal</a> <a id="1038" class="Symbol">=</a> <a id="1040" href="Cubical.Algebra.CommRing.Ideal.Base.html#3126" class="Function">CommIdeal.0Ideal</a> <a id="1057" class="Symbol">(</a><a id="1058" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1079" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1080" class="Symbol">)</a>
+  <a id="1031" href="Cubical.Algebra.CommAlgebra.Ideal.html#1011" class="Function">0Ideal</a> <a id="1038" class="Symbol">=</a> <a id="1040" href="Cubical.Algebra.CommRing.Ideal.Base.html#3302" class="Function">CommIdeal.0Ideal</a> <a id="1057" class="Symbol">(</a><a id="1058" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1079" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1080" class="Symbol">)</a>
 
   <a id="1085" href="Cubical.Algebra.CommAlgebra.Ideal.html#1085" class="Function">1Ideal</a> <a id="1092" class="Symbol">:</a> <a id="1094" href="Cubical.Algebra.CommAlgebra.Ideal.html#593" class="Function">IdealsIn</a>
-  <a id="1105" href="Cubical.Algebra.CommAlgebra.Ideal.html#1085" class="Function">1Ideal</a> <a id="1112" class="Symbol">=</a> <a id="1114" href="Cubical.Algebra.CommRing.Ideal.Base.html#3345" class="Function">CommIdeal.1Ideal</a> <a id="1131" class="Symbol">(</a><a id="1132" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1153" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1154" class="Symbol">)</a>
+  <a id="1105" href="Cubical.Algebra.CommAlgebra.Ideal.html#1085" class="Function">1Ideal</a> <a id="1112" class="Symbol">=</a> <a id="1114" href="Cubical.Algebra.CommRing.Ideal.Base.html#3521" class="Function">CommIdeal.1Ideal</a> <a id="1131" class="Symbol">(</a><a id="1132" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1153" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1154" class="Symbol">)</a>
 </pre></body></html>

Cubical.Algebra.CommAlgebra.Kernel.html

@@ -6,7 +6,7 @@
 <a id="113" class="Keyword">open</a> <a id="118" class="Keyword">import</a> <a id="125" href="Cubical.Foundations.Equiv.html" class="Module">Cubical.Foundations.Equiv</a>
 
 <a id="152" class="Keyword">open</a> <a id="157" class="Keyword">import</a> <a id="164" href="Cubical.Algebra.CommRing.Base.html" class="Module">Cubical.Algebra.CommRing.Base</a>
-<a id="194" class="Keyword">open</a> <a id="199" class="Keyword">import</a> <a id="206" href="Cubical.Algebra.CommRing.Ideal.html" class="Module">Cubical.Algebra.CommRing.Ideal</a> <a id="237" class="Keyword">using</a> <a id="243" class="Symbol">(</a><a id="244" href="Cubical.Algebra.CommRing.Ideal.Base.html#5087" class="Function">Ideal→CommIdeal</a><a id="259" class="Symbol">)</a>
+<a id="194" class="Keyword">open</a> <a id="199" class="Keyword">import</a> <a id="206" href="Cubical.Algebra.CommRing.Ideal.html" class="Module">Cubical.Algebra.CommRing.Ideal</a> <a id="237" class="Keyword">using</a> <a id="243" class="Symbol">(</a><a id="244" href="Cubical.Algebra.CommRing.Ideal.Base.html#5263" class="Function">Ideal→CommIdeal</a><a id="259" class="Symbol">)</a>
 <a id="261" class="Keyword">open</a> <a id="266" class="Keyword">import</a> <a id="273" href="Cubical.Algebra.Ring.Kernel.html" class="Module">Cubical.Algebra.Ring.Kernel</a> <a id="301" class="Keyword">using</a> <a id="307" class="Symbol">()</a> <a id="310" class="Keyword">renaming</a> <a id="319" class="Symbol">(</a><a id="320" href="Cubical.Algebra.Ring.Kernel.html#1581" class="Function">kernelIdeal</a> <a id="332" class="Symbol">to</a> <a id="335" class="Function">ringKernel</a><a id="345" class="Symbol">)</a>
 <a id="347" class="Keyword">open</a> <a id="352" class="Keyword">import</a> <a id="359" href="Cubical.Algebra.CommAlgebra.Base.html" class="Module">Cubical.Algebra.CommAlgebra.Base</a>
 <a id="392" class="Keyword">open</a> <a id="397" class="Keyword">import</a> <a id="404" href="Cubical.Algebra.CommAlgebra.Properties.html" class="Module">Cubical.Algebra.CommAlgebra.Properties</a>
@@ -19,5 +19,5 @@
 <a id="524" class="Keyword">module</a> <a id="531" href="Cubical.Algebra.CommAlgebra.Kernel.html#531" class="Module">_</a> <a id="533" class="Symbol">{</a><a id="534" href="Cubical.Algebra.CommAlgebra.Kernel.html#534" class="Bound">R</a> <a id="536" class="Symbol">:</a> <a id="538" href="Cubical.Algebra.CommRing.Base.html#1279" class="Function">CommRing</a> <a id="547" href="Cubical.Algebra.CommAlgebra.Kernel.html#513" class="Generalizable">ℓ</a><a id="548" class="Symbol">}</a> <a id="550" class="Symbol">(</a><a id="551" href="Cubical.Algebra.CommAlgebra.Kernel.html#551" class="Bound">A</a> <a id="553" href="Cubical.Algebra.CommAlgebra.Kernel.html#553" class="Bound">B</a> <a id="555" class="Symbol">:</a> <a id="557" href="Cubical.Algebra.CommAlgebra.Base.html#1625" class="Function">CommAlgebra</a> <a id="569" href="Cubical.Algebra.CommAlgebra.Kernel.html#534" class="Bound">R</a> <a id="571" href="Cubical.Algebra.CommAlgebra.Kernel.html#513" class="Generalizable">ℓ</a><a id="572" class="Symbol">)</a> <a id="574" class="Symbol">(</a><a id="575" href="Cubical.Algebra.CommAlgebra.Kernel.html#575" class="Bound">ϕ</a> <a id="577" class="Symbol">:</a> <a id="579" href="Cubical.Algebra.CommAlgebra.Base.html#7059" class="Function">CommAlgebraHom</a> <a id="594" href="Cubical.Algebra.CommAlgebra.Kernel.html#551" class="Bound">A</a> <a id="596" href="Cubical.Algebra.CommAlgebra.Kernel.html#553" class="Bound">B</a><a id="597" class="Symbol">)</a> <a id="599" class="Keyword">where</a>
 
   <a id="608" href="Cubical.Algebra.CommAlgebra.Kernel.html#608" class="Function">kernel</a> <a id="615" class="Symbol">:</a> <a id="617" href="Cubical.Algebra.CommAlgebra.Ideal.html#593" class="Function">IdealsIn</a> <a id="626" href="Cubical.Algebra.CommAlgebra.Kernel.html#551" class="Bound">A</a>
-  <a id="630" href="Cubical.Algebra.CommAlgebra.Kernel.html#608" class="Function">kernel</a> <a id="637" class="Symbol">=</a> <a id="639" href="Cubical.Algebra.CommRing.Ideal.Base.html#5087" class="Function">Ideal→CommIdeal</a> <a id="655" class="Symbol">(</a><a id="656" href="Cubical.Algebra.CommAlgebra.Kernel.html#335" class="Function">ringKernel</a> <a id="667" class="Symbol">(</a><a id="668" href="Cubical.Algebra.CommAlgebra.Properties.html#14655" class="Function">CommAlgebraHom→RingHom</a> <a id="691" class="Symbol">{</a><a id="692" class="Argument">A</a> <a id="694" class="Symbol">=</a> <a id="696" href="Cubical.Algebra.CommAlgebra.Kernel.html#551" class="Bound">A</a><a id="697" class="Symbol">}</a> <a id="699" class="Symbol">{</a><a id="700" class="Argument">B</a> <a id="702" class="Symbol">=</a> <a id="704" href="Cubical.Algebra.CommAlgebra.Kernel.html#553" class="Bound">B</a><a id="705" class="Symbol">}</a> <a id="707" href="Cubical.Algebra.CommAlgebra.Kernel.html#575" class="Bound">ϕ</a><a id="708" class="Symbol">))</a>
+  <a id="630" href="Cubical.Algebra.CommAlgebra.Kernel.html#608" class="Function">kernel</a> <a id="637" class="Symbol">=</a> <a id="639" href="Cubical.Algebra.CommRing.Ideal.Base.html#5263" class="Function">Ideal→CommIdeal</a> <a id="655" class="Symbol">(</a><a id="656" href="Cubical.Algebra.CommAlgebra.Kernel.html#335" class="Function">ringKernel</a> <a id="667" class="Symbol">(</a><a id="668" href="Cubical.Algebra.CommAlgebra.Properties.html#14655" class="Function">CommAlgebraHom→RingHom</a> <a id="691" class="Symbol">{</a><a id="692" class="Argument">A</a> <a id="694" class="Symbol">=</a> <a id="696" href="Cubical.Algebra.CommAlgebra.Kernel.html#551" class="Bound">A</a><a id="697" class="Symbol">}</a> <a id="699" class="Symbol">{</a><a id="700" class="Argument">B</a> <a id="702" class="Symbol">=</a> <a id="704" href="Cubical.Algebra.CommAlgebra.Kernel.html#553" class="Bound">B</a><a id="705" class="Symbol">}</a> <a id="707" href="Cubical.Algebra.CommAlgebra.Kernel.html#575" class="Bound">ϕ</a><a id="708" class="Symbol">))</a>
 </pre></body></html>

Cubical.Algebra.CommAlgebra.QuotientAlgebra.html

@@ -15,7 +15,7 @@
 <a id="483" class="Keyword">open</a> <a id="488" class="Keyword">import</a> <a id="495" href="Cubical.Algebra.CommRing.html" class="Module">Cubical.Algebra.CommRing</a>
 <a id="520" class="Keyword">import</a> <a id="527" href="Cubical.Algebra.CommRing.Quotient.html" class="Module">Cubical.Algebra.CommRing.Quotient</a> <a id="561" class="Symbol">as</a> <a id="564" class="Module">CommRing</a>
 <a id="573" class="Keyword">import</a> <a id="580" href="Cubical.Algebra.Ring.Quotient.html" class="Module">Cubical.Algebra.Ring.Quotient</a> <a id="610" class="Symbol">as</a> <a id="613" class="Module">Ring</a>
-<a id="618" class="Keyword">open</a> <a id="623" class="Keyword">import</a> <a id="630" href="Cubical.Algebra.CommRing.Ideal.html" class="Module">Cubical.Algebra.CommRing.Ideal</a> <a id="661" class="Keyword">hiding</a> <a id="668" class="Symbol">(</a><a id="669" href="Cubical.Algebra.CommRing.Ideal.Base.html#3666" class="Function">IdealsIn</a><a id="677" class="Symbol">)</a>
+<a id="618" class="Keyword">open</a> <a id="623" class="Keyword">import</a> <a id="630" href="Cubical.Algebra.CommRing.Ideal.html" class="Module">Cubical.Algebra.CommRing.Ideal</a> <a id="661" class="Keyword">hiding</a> <a id="668" class="Symbol">(</a><a id="669" href="Cubical.Algebra.CommRing.Ideal.Base.html#3842" class="Function">IdealsIn</a><a id="677" class="Symbol">)</a>
 <a id="679" class="Keyword">open</a> <a id="684" class="Keyword">import</a> <a id="691" href="Cubical.Algebra.CommAlgebra.html" class="Module">Cubical.Algebra.CommAlgebra</a>
 <a id="719" class="Keyword">open</a> <a id="724" class="Keyword">import</a> <a id="731" href="Cubical.Algebra.CommAlgebra.Ideal.html" class="Module">Cubical.Algebra.CommAlgebra.Ideal</a>
 <a id="765" class="Keyword">open</a> <a id="770" class="Keyword">import</a> <a id="777" href="Cubical.Algebra.CommAlgebra.Kernel.html" class="Module">Cubical.Algebra.CommAlgebra.Kernel</a>
@@ -113,7 +113,7 @@
 
     <a id="4567" class="Comment">-- sanity check / maybe a helper function some day</a>
     <a id="4622" class="Comment">-- (These two rings are not definitionally equal, but only because of proofs, not data.)</a>
-    <a id="4715" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4715" class="Function">CommForget/</a> <a id="4727" class="Symbol">:</a> <a id="4729" href="Cubical.Algebra.Ring.Base.html#4647" class="Function">RingEquiv</a> <a id="4739" class="Symbol">(</a><a id="4740" href="Cubical.Algebra.CommAlgebra.Properties.html#14388" class="Function">CommAlgebra→Ring</a> <a id="4757" class="Symbol">(</a><a id="4758" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4254" class="Bound">A</a> <a id="4760" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#1823" class="Function Operator">/</a> <a id="4762" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4276" class="Bound">I</a><a id="4763" class="Symbol">))</a> <a id="4766" class="Symbol">((</a><a id="4768" href="Cubical.Algebra.CommAlgebra.Properties.html#14388" class="Function">CommAlgebra→Ring</a> <a id="4785" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4254" class="Bound">A</a><a id="4786" class="Symbol">)</a> <a id="4788" href="Cubical.Algebra.Ring.Quotient.html#7223" class="Function Operator">Ring./</a> <a id="4795" class="Symbol">(</a><a id="4796" href="Cubical.Algebra.CommRing.Ideal.Base.html#4395" class="Function">CommIdeal→Ideal</a> <a id="4812" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4276" class="Bound">I</a><a id="4813" class="Symbol">))</a>
+    <a id="4715" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4715" class="Function">CommForget/</a> <a id="4727" class="Symbol">:</a> <a id="4729" href="Cubical.Algebra.Ring.Base.html#4647" class="Function">RingEquiv</a> <a id="4739" class="Symbol">(</a><a id="4740" href="Cubical.Algebra.CommAlgebra.Properties.html#14388" class="Function">CommAlgebra→Ring</a> <a id="4757" class="Symbol">(</a><a id="4758" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4254" class="Bound">A</a> <a id="4760" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#1823" class="Function Operator">/</a> <a id="4762" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4276" class="Bound">I</a><a id="4763" class="Symbol">))</a> <a id="4766" class="Symbol">((</a><a id="4768" href="Cubical.Algebra.CommAlgebra.Properties.html#14388" class="Function">CommAlgebra→Ring</a> <a id="4785" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4254" class="Bound">A</a><a id="4786" class="Symbol">)</a> <a id="4788" href="Cubical.Algebra.Ring.Quotient.html#7223" class="Function Operator">Ring./</a> <a id="4795" class="Symbol">(</a><a id="4796" href="Cubical.Algebra.CommRing.Ideal.Base.html#4571" class="Function">CommIdeal→Ideal</a> <a id="4812" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4276" class="Bound">I</a><a id="4813" class="Symbol">))</a>
     <a id="4820" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="4824" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4715" class="Function">CommForget/</a> <a id="4836" class="Symbol">=</a> <a id="4838" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="4846" class="Symbol">_</a>
     <a id="4852" href="Cubical.Algebra.Ring.Base.html#4097" class="Field">IsRingHom.pres0</a> <a id="4868" class="Symbol">(</a><a id="4869" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="4873" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4715" class="Function">CommForget/</a><a id="4884" class="Symbol">)</a> <a id="4886" class="Symbol">=</a> <a id="4888" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
     <a id="4897" href="Cubical.Algebra.Ring.Base.html#4123" class="Field">IsRingHom.pres1</a> <a id="4913" class="Symbol">(</a><a id="4914" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="4918" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#4715" class="Function">CommForget/</a><a id="4929" class="Symbol">)</a> <a id="4931" class="Symbol">=</a> <a id="4933" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>