Skip to content

Commit

Permalink
Deploying to gh-pages from @ fce3814 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@maxsnew
maxsnew committed Sep 10, 2024
1 parent 29ff7bd commit f931a6a
Show file tree
Hide file tree
Showing 44 changed files with 1,449 additions and 1,207 deletions.
4 changes: 2 additions & 2 deletions Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,8 +63,8 @@


<a id="1882" class="Comment">-- using the naming conventions of Demazure &amp; Gabriel</a>
<a id="1938" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1938" class="Function">ℤFunctor</a> <a id="1947" class="Symbol">=</a> <a id="1949" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="1957" class="Symbol">(</a><a id="1958" href="Cubical.Categories.Instances.CommRings.html#1142" class="Function">CommRingsCategory</a> <a id="1976" class="Symbol">{</a><a id="1977" class="Argument">ℓ</a> <a id="1979" class="Symbol">=</a> <a id="1981" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1787" class="Bound">ℓ</a><a id="1982" class="Symbol">})</a> <a id="1985" class="Symbol">(</a><a id="1986" href="Cubical.Categories.Instances.Sets.html#551" class="Function">SET</a> <a id="1990" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1787" class="Bound">ℓ</a><a id="1991" class="Symbol">)</a>
<a id="1995" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1995" class="Function">ℤFUNCTOR</a> <a id="2004" class="Symbol">=</a> <a id="2006" href="Cubical.Categories.Instances.Functors.html#992" class="Function">FUNCTOR</a> <a id="2014" class="Symbol">(</a><a id="2015" href="Cubical.Categories.Instances.CommRings.html#1142" class="Function">CommRingsCategory</a> <a id="2033" class="Symbol">{</a><a id="2034" class="Argument">ℓ</a> <a id="2036" class="Symbol">=</a> <a id="2038" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1787" class="Bound">ℓ</a><a id="2039" class="Symbol">})</a> <a id="2042" class="Symbol">(</a><a id="2043" href="Cubical.Categories.Instances.Sets.html#551" class="Function">SET</a> <a id="2047" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1787" class="Bound">ℓ</a><a id="2048" class="Symbol">)</a>
<a id="1938" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1938" class="Function">ℤFunctor</a> <a id="1947" class="Symbol">=</a> <a id="1949" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="1957" class="Symbol">(</a><a id="1958" href="Cubical.Categories.Instances.CommRings.html#1142" class="Function">CommRingsCategory</a> <a id="1976" class="Symbol">{</a><a id="1977" class="Argument">ℓ</a> <a id="1979" class="Symbol">=</a> <a id="1981" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1787" class="Bound">ℓ</a><a id="1982" class="Symbol">})</a> <a id="1985" class="Symbol">(</a><a id="1986" href="Cubical.Categories.Instances.Sets.html#605" class="Function">SET</a> <a id="1990" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1787" class="Bound">ℓ</a><a id="1991" class="Symbol">)</a>
<a id="1995" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1995" class="Function">ℤFUNCTOR</a> <a id="2004" class="Symbol">=</a> <a id="2006" href="Cubical.Categories.Instances.Functors.html#992" class="Function">FUNCTOR</a> <a id="2014" class="Symbol">(</a><a id="2015" href="Cubical.Categories.Instances.CommRings.html#1142" class="Function">CommRingsCategory</a> <a id="2033" class="Symbol">{</a><a id="2034" class="Argument">ℓ</a> <a id="2036" class="Symbol">=</a> <a id="2038" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1787" class="Bound">ℓ</a><a id="2039" class="Symbol">})</a> <a id="2042" class="Symbol">(</a><a id="2043" href="Cubical.Categories.Instances.Sets.html#605" class="Function">SET</a> <a id="2047" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html#1787" class="Bound">ℓ</a><a id="2048" class="Symbol">)</a>

<a id="2053" class="Comment">-- Yoneda in the notation of Demazure &amp; Gabriel,</a>
<a id="2104" class="Comment">-- uses that double op is original category definitionally</a>
Expand Down
708 changes: 361 additions & 347 deletions Cubical.Categories.Adjoint.html
View file

Large diffs are not rendered by default.

47 changes: 24 additions & 23 deletions Cubical.Categories.Category.Properties.html
View file

Large diffs are not rendered by default.

14 changes: 7 additions & 7 deletions Cubical.Categories.Constructions.Elements.html
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions Cubical.Categories.Constructions.Power.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@
<a id="419" href="Cubical.Categories.Constructions.Power.html#353" class="Function">PowerCategory</a> <a id="433" href="Cubical.Categories.Constructions.Power.html#433" class="Bound">X</a> <a id="435" href="Cubical.Categories.Constructions.Power.html#435" class="Bound">C</a> <a id="437" class="Symbol">=</a> <a id="439" href="Cubical.Categories.Constructions.Product.html#423" class="Function">ΠC</a> <a id="442" href="Cubical.Categories.Constructions.Power.html#433" class="Bound">X</a> <a id="444" class="Symbol">(λ</a> <a id="447" href="Cubical.Categories.Constructions.Power.html#447" class="Bound">_</a> <a id="449" class="Symbol">→</a> <a id="451" href="Cubical.Categories.Constructions.Power.html#435" class="Bound">C</a><a id="452" class="Symbol">)</a>

<a id="PseudoYoneda"></a><a id="455" href="Cubical.Categories.Constructions.Power.html#455" class="Function">PseudoYoneda</a> <a id="468" class="Symbol">:</a> <a id="470" class="Symbol">{</a><a id="471" href="Cubical.Categories.Constructions.Power.html#471" class="Bound">C</a> <a id="473" class="Symbol">:</a> <a id="475" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="484" href="Cubical.Categories.Constructions.Power.html#322" class="Generalizable">ℓc</a> <a id="487" href="Cubical.Categories.Constructions.Power.html#325" class="Generalizable">ℓc&#39;</a><a id="490" class="Symbol">}</a>
<a id="505" class="Symbol">→</a> <a id="507" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="515" href="Cubical.Categories.Constructions.Power.html#471" class="Bound">C</a> <a id="517" class="Symbol">(</a><a id="518" href="Cubical.Categories.Constructions.Power.html#353" class="Function">PowerCategory</a> <a id="532" class="Symbol">(</a><a id="533" href="Cubical.Categories.Constructions.Power.html#471" class="Bound">C</a> <a id="535" class="Symbol">.</a><a id="536" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="538" class="Symbol">)</a> <a id="540" class="Symbol">(</a><a id="541" href="Cubical.Categories.Instances.Sets.html#551" class="Function">SET</a> <a id="545" href="Cubical.Categories.Constructions.Power.html#325" class="Generalizable">ℓc&#39;</a><a id="548" class="Symbol">))</a>
<a id="551" href="Cubical.Categories.Constructions.Power.html#455" class="Function">PseudoYoneda</a> <a id="564" class="Symbol">{</a><a id="565" class="Argument">C</a> <a id="567" class="Symbol">=</a> <a id="569" href="Cubical.Categories.Constructions.Power.html#569" class="Bound">C</a><a id="570" class="Symbol">}</a> <a id="572" class="Symbol">=</a> <a id="574" href="Cubical.Categories.Constructions.Product.html#833" class="Function">Π-intro</a> <a id="582" class="Symbol">_</a> <a id="584" class="Symbol">(λ</a> <a id="587" href="Cubical.Categories.Constructions.Power.html#587" class="Bound">_</a> <a id="589" class="Symbol">→</a> <a id="591" href="Cubical.Categories.Instances.Sets.html#551" class="Function">SET</a> <a id="595" class="Symbol">_)</a> <a id="598" class="Symbol">λ</a> <a id="600" href="Cubical.Categories.Constructions.Power.html#600" class="Bound">a</a> <a id="602" class="Symbol">→</a> <a id="604" href="Cubical.Categories.Constructions.Power.html#569" class="Bound">C</a> <a id="606" href="Cubical.Categories.Instances.Sets.html#1118" class="Function Operator">[</a> <a id="608" href="Cubical.Categories.Constructions.Power.html#600" class="Bound">a</a> <a id="610" href="Cubical.Categories.Instances.Sets.html#1118" class="Function Operator">,-]</a>
<a id="505" class="Symbol">→</a> <a id="507" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="515" href="Cubical.Categories.Constructions.Power.html#471" class="Bound">C</a> <a id="517" class="Symbol">(</a><a id="518" href="Cubical.Categories.Constructions.Power.html#353" class="Function">PowerCategory</a> <a id="532" class="Symbol">(</a><a id="533" href="Cubical.Categories.Constructions.Power.html#471" class="Bound">C</a> <a id="535" class="Symbol">.</a><a id="536" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="538" class="Symbol">)</a> <a id="540" class="Symbol">(</a><a id="541" href="Cubical.Categories.Instances.Sets.html#605" class="Function">SET</a> <a id="545" href="Cubical.Categories.Constructions.Power.html#325" class="Generalizable">ℓc&#39;</a><a id="548" class="Symbol">))</a>
<a id="551" href="Cubical.Categories.Constructions.Power.html#455" class="Function">PseudoYoneda</a> <a id="564" class="Symbol">{</a><a id="565" class="Argument">C</a> <a id="567" class="Symbol">=</a> <a id="569" href="Cubical.Categories.Constructions.Power.html#569" class="Bound">C</a><a id="570" class="Symbol">}</a> <a id="572" class="Symbol">=</a> <a id="574" href="Cubical.Categories.Constructions.Product.html#833" class="Function">Π-intro</a> <a id="582" class="Symbol">_</a> <a id="584" class="Symbol">(λ</a> <a id="587" href="Cubical.Categories.Constructions.Power.html#587" class="Bound">_</a> <a id="589" class="Symbol">→</a> <a id="591" href="Cubical.Categories.Instances.Sets.html#605" class="Function">SET</a> <a id="595" class="Symbol">_)</a> <a id="598" class="Symbol">λ</a> <a id="600" href="Cubical.Categories.Constructions.Power.html#600" class="Bound">a</a> <a id="602" class="Symbol">→</a> <a id="604" href="Cubical.Categories.Constructions.Power.html#569" class="Bound">C</a> <a id="606" href="Cubical.Categories.Instances.Sets.html#1172" class="Function Operator">[</a> <a id="608" href="Cubical.Categories.Constructions.Power.html#600" class="Bound">a</a> <a id="610" href="Cubical.Categories.Instances.Sets.html#1172" class="Function Operator">,-]</a>

<a id="isFaithfulPseudoYoneda"></a><a id="615" href="Cubical.Categories.Constructions.Power.html#615" class="Function">isFaithfulPseudoYoneda</a> <a id="638" class="Symbol">:</a> <a id="640" class="Symbol">{</a><a id="641" href="Cubical.Categories.Constructions.Power.html#641" class="Bound">C</a> <a id="643" class="Symbol">:</a> <a id="645" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="654" href="Cubical.Categories.Constructions.Power.html#322" class="Generalizable">ℓc</a> <a id="657" href="Cubical.Categories.Constructions.Power.html#325" class="Generalizable">ℓc&#39;</a><a id="660" class="Symbol">}</a>
<a id="685" class="Symbol">→</a> <a id="687" href="Cubical.Categories.Functor.Base.html#965" class="Function">Functor.isFaithful</a> <a id="706" class="Symbol">(</a><a id="707" href="Cubical.Categories.Constructions.Power.html#455" class="Function">PseudoYoneda</a> <a id="720" class="Symbol">{</a><a id="721" class="Argument">C</a> <a id="723" class="Symbol">=</a> <a id="725" href="Cubical.Categories.Constructions.Power.html#641" class="Bound">C</a><a id="726" class="Symbol">})</a>
Expand Down
Loading

0 comments on commit f931a6a

Please sign in to comment.