Deploying to gh-pages from @ 0dc865a 🚀

agda · Feb 16, 2024 · 30a2dac · 30a2dac
1 parent b0abefb
commit 30a2dac
Show file tree

Hide file tree

Showing 8 changed files with 1,245 additions and 1,270 deletions.
diff --git a/Cubical.Algebra.CommAlgebra.Localisation.html b/Cubical.Algebra.CommAlgebra.Localisation.html
diff --git a/Cubical.Algebra.CommRing.Localisation.InvertingElements.html b/Cubical.Algebra.CommRing.Localisation.InvertingElements.html
diff --git a/Cubical.Algebra.CommRing.Localisation.Limit.html b/Cubical.Algebra.CommRing.Localisation.Limit.html
diff --git a/Cubical.Algebra.CommRing.Localisation.PullbackSquare.html b/Cubical.Algebra.CommRing.Localisation.PullbackSquare.html
diff --git a/Cubical.Algebra.ZariskiLattice.StructureSheaf.html b/Cubical.Algebra.ZariskiLattice.StructureSheaf.html
diff --git a/Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html b/Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html
diff --git a/Cubical.Categories.Site.Instances.ZariskiCommRing.html b/Cubical.Categories.Site.Instances.ZariskiCommRing.html
diff --git a/Cubical.Papers.AffineSchemes.html b/Cubical.Papers.AffineSchemes.html
@@ -137,10 +137,10 @@
 
 <a id="4449" class="Comment">-- Lemma 3</a>
 <a id="4460" class="Comment">-- 1.</a>
-<a id="4466" class="Keyword">open</a> <a id="4471" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#14651" class="Module">LocalizationInvEl.DoubleLoc</a> <a id="4499" class="Keyword">using</a> <a id="4505" class="Symbol">(</a><a id="4506" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#26354" class="Function">R[1/fg]≡R[1/f][1/g]</a><a id="4525" class="Symbol">)</a>
+<a id="4466" class="Keyword">open</a> <a id="4471" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#14399" class="Module">LocalizationInvEl.DoubleLoc</a> <a id="4499" class="Keyword">using</a> <a id="4505" class="Symbol">(</a><a id="4506" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#26102" class="Function">R[1/fg]≡R[1/f][1/g]</a><a id="4525" class="Symbol">)</a>
 <a id="4527" class="Keyword">open</a> <a id="4532" href="Cubical.Algebra.CommAlgebra.Localisation.html#10303" class="Module">LocalizationR-Alg.DoubleAlgLoc</a> <a id="4563" class="Keyword">using</a> <a id="4569" class="Symbol">(</a><a id="4570" href="Cubical.Algebra.CommAlgebra.Localisation.html#11290" class="Function">R[1/fg]≡R[1/f][1/g]</a><a id="4589" class="Symbol">)</a>
 <a id="4591" class="Comment">-- 2.</a>
-<a id="4597" class="Keyword">open</a> <a id="4602" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html" class="Module">LocalizationInvEl</a> <a id="4620" class="Keyword">using</a> <a id="4626" class="Symbol">(</a><a id="4627" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#12677" class="Function">invertingUnitsPath</a><a id="4645" class="Symbol">)</a>
+<a id="4597" class="Keyword">open</a> <a id="4602" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html" class="Module">LocalizationInvEl</a> <a id="4620" class="Keyword">using</a> <a id="4626" class="Symbol">(</a><a id="4627" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#12425" class="Function">invertingUnitsPath</a><a id="4645" class="Symbol">)</a>
 <a id="4647" class="Comment">-- 3.</a>
 <a id="4653" class="Keyword">open</a> <a id="4658" href="Cubical.Algebra.CommAlgebra.Localisation.html#6151" class="Module">LocalizationR-Alg.AlgLocTwoSubsets</a> <a id="4693" class="Keyword">using</a> <a id="4699" class="Symbol">(</a><a id="4700" href="Cubical.Algebra.CommAlgebra.Localisation.html#7690" class="Function">isContrS₁⁻¹R≡S₂⁻¹R</a><a id="4718" class="Symbol">)</a>
 
@@ -233,11 +233,11 @@
 <a id="6791" class="Keyword">open</a> <a id="6796" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html" class="Module">StructureSheaf</a> <a id="6811" class="Keyword">using</a> <a id="6817" class="Symbol">(</a><a id="6818" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html#7854" class="Function">globalSection</a><a id="6831" class="Symbol">)</a>
 
 <a id="6834" class="Comment">-- Lemma 15</a>
-<a id="6846" class="Keyword">open</a> <a id="6851" href="Cubical.Algebra.CommRing.Localisation.Limit.html" class="Module">LocalizationLimit</a> <a id="6869" class="Keyword">using</a> <a id="6875" class="Symbol">(</a><a id="6876" href="Cubical.Algebra.CommRing.Localisation.Limit.html#22535" class="Function">isLimConeLocCone</a><a id="6892" class="Symbol">)</a>
+<a id="6846" class="Keyword">open</a> <a id="6851" href="Cubical.Algebra.CommRing.Localisation.Limit.html" class="Module">LocalizationLimit</a> <a id="6869" class="Keyword">using</a> <a id="6875" class="Symbol">(</a><a id="6876" href="Cubical.Algebra.CommRing.Localisation.Limit.html#22373" class="Function">isLimConeLocCone</a><a id="6892" class="Symbol">)</a>
 
 <a id="6895" class="Comment">-- Theorem 16</a>
 <a id="6909" class="Keyword">open</a> <a id="6914" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html" class="Module">StructureSheaf</a> <a id="6929" class="Keyword">using</a> <a id="6935" class="Symbol">(</a><a id="6936" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html#8137" class="Function">isSheaf𝓞ᴮ</a><a id="6945" class="Symbol">)</a>
 
 <a id="6948" class="Comment">-- Corollary 17</a>
-<a id="6964" class="Keyword">open</a> <a id="6969" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html" class="Module">StructureSheaf</a> <a id="6984" class="Keyword">using</a> <a id="6990" class="Symbol">(</a><a id="6991" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html#17743" class="Function">isSheaf𝓞</a><a id="6999" class="Symbol">)</a>
+<a id="6964" class="Keyword">open</a> <a id="6969" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html" class="Module">StructureSheaf</a> <a id="6984" class="Keyword">using</a> <a id="6990" class="Symbol">(</a><a id="6991" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html#16885" class="Function">isSheaf𝓞</a><a id="6999" class="Symbol">)</a>
 </pre></body></html>