bump

hejohns · May 11, 2024 · 21d8869 · 21d8869
1 parent 7022566
commit 21d8869
Show file tree

Hide file tree

Showing 26 changed files with 335 additions and 451 deletions.
diff --git a/_forest b/_forest
diff --git a/_site/2023/04/09/gsi-applications.html b/_site/2023/04/09/gsi-applications.html
@@ -83,8 +83,8 @@ <h2 id="engr-101-f23">ENGR 101 (F23)</h2>
 
 <iframe width="560" height="315" src="https://www.youtube.com/embed/Cd9Tq7s_BhQ" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" allowfullscreen=""></iframe>
 
-<style> .pdf-embed-wrap-24d4e83d-8b5a-4a52-8622-9bde4234c74e { display: flex; flex-direction: column; width: 100%; height: 650px; } .pdf-embed-container-24d4e83d-8b5a-4a52-8622-9bde4234c74e { height: 100%; } .pdf-link-24d4e83d-8b5a-4a52-8622-9bde4234c74e { background-color: white; text-align: center; border-style: solid; } .pdf-embed-container-24d4e83d-8b5a-4a52-8622-9bde4234c74e iframe { width: 100%; height: 100%; } </style>
-<div class="pdf-embed-wrap-24d4e83d-8b5a-4a52-8622-9bde4234c74e"> <div class="pdf-link-24d4e83d-8b5a-4a52-8622-9bde4234c74e"> <a href="/files/101-gsi-application.pdf" target="_blank">View PDF</a> </div> <div class="pdf-embed-container-24d4e83d-8b5a-4a52-8622-9bde4234c74e"> <iframe src="/files/101-gsi-application.pdf" frameborder="0" allowfullscreen=""></iframe> </div> </div>
+<style> .pdf-embed-wrap-02c01dbc-89de-488a-8762-b4cc2a74c04c { display: flex; flex-direction: column; width: 100%; height: 650px; } .pdf-embed-container-02c01dbc-89de-488a-8762-b4cc2a74c04c { height: 100%; } .pdf-link-02c01dbc-89de-488a-8762-b4cc2a74c04c { background-color: white; text-align: center; border-style: solid; } .pdf-embed-container-02c01dbc-89de-488a-8762-b4cc2a74c04c iframe { width: 100%; height: 100%; } </style>
+<div class="pdf-embed-wrap-02c01dbc-89de-488a-8762-b4cc2a74c04c"> <div class="pdf-link-02c01dbc-89de-488a-8762-b4cc2a74c04c"> <a href="/files/101-gsi-application.pdf" target="_blank">View PDF</a> </div> <div class="pdf-embed-container-02c01dbc-89de-488a-8762-b4cc2a74c04c"> <iframe src="/files/101-gsi-application.pdf" frameborder="0" allowfullscreen=""></iframe> </div> </div>
 <h2 id="eecs-376-f23">EECS 376 (F23)</h2>
 <p><strong>outcome</strong>: rejected. No response.</p>
 <h3 id="too-long-version">too long version</h3>

diff --git a/_site/feed.xml b/_site/feed.xml
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?><feed xmlns="http://www.w3.org/2005/Atom" ><generator uri="https://jekyllrb.com/" version="4.3.3">Jekyll</generator><link href="https://hejohns.github.io/feed.xml" rel="self" type="application/atom+xml" /><link href="https://hejohns.github.io/" rel="alternate" type="text/html" /><updated>2024-05-11T06:41:21-04:00</updated><id>https://hejohns.github.io/feed.xml</id><title type="html">hejohns’ jekyll site</title><subtitle>a pure waste of space</subtitle><author><name>Johnson He</name><email>hejohns α umich δ edu</email></author><entry><title type="html">fountain pen nibs</title><link href="https://hejohns.github.io/2024/04/11/fountain-pen-nibs.html" rel="alternate" type="text/html" title="fountain pen nibs" /><published>2024-04-11T00:00:00-04:00</published><updated>2024-04-11T17:48:22-04:00</updated><id>https://hejohns.github.io/2024/04/11/fountain-pen-nibs</id><content type="html" xml:base="https://hejohns.github.io/2024/04/11/fountain-pen-nibs.html"><![CDATA[<p>Several weeks ago, I lost my other TWSBI 580 (technically, the 580 ALR)
+<?xml version="1.0" encoding="utf-8"?><feed xmlns="http://www.w3.org/2005/Atom" ><generator uri="https://jekyllrb.com/" version="4.3.3">Jekyll</generator><link href="https://hejohns.github.io/feed.xml" rel="self" type="application/atom+xml" /><link href="https://hejohns.github.io/" rel="alternate" type="text/html" /><updated>2024-05-11T07:14:46-04:00</updated><id>https://hejohns.github.io/feed.xml</id><title type="html">hejohns’ jekyll site</title><subtitle>a pure waste of space</subtitle><author><name>Johnson He</name><email>hejohns α umich δ edu</email></author><entry><title type="html">fountain pen nibs</title><link href="https://hejohns.github.io/2024/04/11/fountain-pen-nibs.html" rel="alternate" type="text/html" title="fountain pen nibs" /><published>2024-04-11T00:00:00-04:00</published><updated>2024-04-11T17:48:22-04:00</updated><id>https://hejohns.github.io/2024/04/11/fountain-pen-nibs</id><content type="html" xml:base="https://hejohns.github.io/2024/04/11/fountain-pen-nibs.html"><![CDATA[<p>Several weeks ago, I lost my other TWSBI 580 (technically, the 580 ALR)
 which meant that I didn’t have any EF nibs left<sup id="fnref:1" role="doc-noteref"><a href="#fn:1" class="footnote" rel="footnote">1</a></sup>.</p>
 
 <p>Through the process of sourcing nibs, I learned a lot about the details so:</p>

diff --git a/_site/forest.html b/_site/forest.html
@@ -17,7 +17,7 @@
 <meta name="twitter:card" content="summary" />
 <meta property="twitter:title" content="forest" />
 <script type="application/ld+json">
-{"@context":"https://schema.org","@type":"WebPage","author":{"@type":"Person","name":"Johnson He"},"dateModified":"2024-05-06T05:53:00-04:00","description":"a pure waste of space","headline":"forest","url":"https://hejohns.github.io/forest.html"}</script>
+{"@context":"https://schema.org","@type":"WebPage","author":{"@type":"Person","name":"Johnson He"},"dateModified":"2024-05-11T06:42:31-04:00","description":"a pure waste of space","headline":"forest","url":"https://hejohns.github.io/forest.html"}</script>
 <!-- End Jekyll SEO tag -->
 <link rel="stylesheet" href="/assets/css/style.css"><link type="application/atom+xml" rel="alternate" href="https://hejohns.github.io/feed.xml" title="hejohns&apos; jekyll site" />  <!-- see: -->
   <!-- https://codewrites.me/jekyll/katex/blog/2020/08/26/use-katex-gh-pages/ -->
@@ -54,7 +54,7 @@
 <main class="page-content" aria-label="Content">
       <div class="wrapper">
           <h3>
-            page version: May 6, 2024
+            page version: May 11, 2024
           </h3>
         <meta http-equiv="refresh" content="0; url=forest/index.xml" />
 

diff --git a/_site/forest/hejohns-0006.xml b/_site/forest/hejohns-0006.xml
@@ -530,15 +530,15 @@ root="false"><fr:frontmatter><fr:anchor>265</fr:anchor><fr:taxon>Proposition</fr
 href="hejohns.xml"
 type="local"
 addr="hejohns">Johnson He</fr:link></fr:author></fr:authors><fr:parent>hejohns-000E</fr:parent></fr:frontmatter><fr:mainmatter><fr:p>
-        An adjunction core extends to an adjuction iff (<fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex>
+        An adjunction core extends to an adjuction iff <fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex>
         <fr:link
 href="subb-000E.xml"
 type="local"
-addr="subb-000E">I</fr:link> commutes) or (<fr:tex>∀x,y ∈ X. a ∈ A.</fr:tex> <fr:link
+addr="subb-000E">I</fr:link> commutes, and iff <fr:tex>∀x,y ∈ X. a ∈ A.</fr:tex> <fr:link
 href="subbb-000E.xml"
 type="local"
 addr="subbb-000E">II</fr:link>
-        commutes).
+        commutes.
         The adjunction is unique when it exists.
     </fr:p><fr:p>
         The <fr:link
@@ -610,14 +610,14 @@ addr="sub-0007">the short proof</fr:link>
 href="street-2012.xml"
 type="local"
 addr="street-2012">the
-        paper</fr:link>.  It's also how you'd attack <fr:link
+        paper</fr:link>. It's also how you'd attack <fr:link
 href="hejohns-0007.xml"
 type="local"
 addr="hejohns-0007">the
         precursor</fr:link> head-on. The utility is that it holds in
         enriched categories.
     </fr:p><fr:p>
-        The forwards direction is trivial.
+        The forward directions are trivial.
         Suppose <fr:tex>(F, U, (π_{a, x})_{a ∈ A, x ∈ X})</fr:tex> extends to <fr:tex>\overline {F}  ⊣_π  \overline {U}</fr:tex>.
         Then <fr:link
 href="subb-000E.xml"
@@ -628,14 +628,11 @@ addr="subb-000E">I</fr:link> expresses that <fr:tex>∀g : A(a, b). ∀f : A(F(x
         <fr:link
 href="subbb-000E.xml"
 type="local"
-addr="subbb-000E">II</fr:link> expresses something similar, but we've already shown
-        the forwards direction.
+addr="subbb-000E">II</fr:link> expresses something similar (dual).
     </fr:p><fr:p>
-        The nontrivial direction is the backwards direction.
-        We case on whether I or II holds.
-    </fr:p><fr:ul><fr:li>
-            (I) wts I <fr:tex>⟹  \overline {U}</fr:tex> is a functor.
-            <fr:p>
+        The nontrivial directions are the backward directions.
+    </fr:p><fr:ul><fr:li><fr:p>
+                (I) wts I <fr:tex>⟹  \overline {U}</fr:tex> is a functor.
                 Suppose <fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex> I holds.
                 Then in particular, <fr:tex>∀c ∈ A. </fr:tex>I holds at <fr:tex>x = U(c)</fr:tex>.
             </fr:p>
@@ -722,9 +719,8 @@ addr="hejohns-0007">the precusor</fr:link> to each
                     functor in turn, just knowing the other is a well-defined
                     functor.
                 </fr:li></fr:ul></fr:li>
-        <fr:li>
-            (II) wts II <fr:tex>⟹  \overline {F}</fr:tex> is a functor.
-            <fr:p>
+        <fr:li><fr:p>
+                (II) wts II <fr:tex>⟹  \overline {F}</fr:tex> is a functor.
                 This is dual.
             </fr:p></fr:li></fr:ul></fr:mainmatter></fr:tree><fr:tree
 xmlns:fr="http://www.jonmsterling.com/jms-005P.xml"

diff --git a/_site/forest/hejohns-0007.xml b/_site/forest/hejohns-0007.xml
@@ -784,15 +784,15 @@ root="false"><fr:frontmatter><fr:anchor>265</fr:anchor><fr:taxon>Proposition</fr
 href="hejohns.xml"
 type="local"
 addr="hejohns">Johnson He</fr:link></fr:author></fr:authors><fr:parent>hejohns-000E</fr:parent></fr:frontmatter><fr:mainmatter><fr:p>
-        An adjunction core extends to an adjuction iff (<fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex>
+        An adjunction core extends to an adjuction iff <fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex>
         <fr:link
 href="subb-000E.xml"
 type="local"
-addr="subb-000E">I</fr:link> commutes) or (<fr:tex>∀x,y ∈ X. a ∈ A.</fr:tex> <fr:link
+addr="subb-000E">I</fr:link> commutes, and iff <fr:tex>∀x,y ∈ X. a ∈ A.</fr:tex> <fr:link
 href="subbb-000E.xml"
 type="local"
 addr="subbb-000E">II</fr:link>
-        commutes).
+        commutes.
         The adjunction is unique when it exists.
     </fr:p><fr:p>
         The <fr:link
@@ -864,14 +864,14 @@ addr="sub-0007">the short proof</fr:link>
 href="street-2012.xml"
 type="local"
 addr="street-2012">the
-        paper</fr:link>.  It's also how you'd attack <fr:link
+        paper</fr:link>. It's also how you'd attack <fr:link
 href="hejohns-0007.xml"
 type="local"
 addr="hejohns-0007">the
         precursor</fr:link> head-on. The utility is that it holds in
         enriched categories.
     </fr:p><fr:p>
-        The forwards direction is trivial.
+        The forward directions are trivial.
         Suppose <fr:tex>(F, U, (π_{a, x})_{a ∈ A, x ∈ X})</fr:tex> extends to <fr:tex>\overline {F}  ⊣_π  \overline {U}</fr:tex>.
         Then <fr:link
 href="subb-000E.xml"
@@ -882,14 +882,11 @@ addr="subb-000E">I</fr:link> expresses that <fr:tex>∀g : A(a, b). ∀f : A(F(x
         <fr:link
 href="subbb-000E.xml"
 type="local"
-addr="subbb-000E">II</fr:link> expresses something similar, but we've already shown
-        the forwards direction.
+addr="subbb-000E">II</fr:link> expresses something similar (dual).
     </fr:p><fr:p>
-        The nontrivial direction is the backwards direction.
-        We case on whether I or II holds.
-    </fr:p><fr:ul><fr:li>
-            (I) wts I <fr:tex>⟹  \overline {U}</fr:tex> is a functor.
-            <fr:p>
+        The nontrivial directions are the backward directions.
+    </fr:p><fr:ul><fr:li><fr:p>
+                (I) wts I <fr:tex>⟹  \overline {U}</fr:tex> is a functor.
                 Suppose <fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex> I holds.
                 Then in particular, <fr:tex>∀c ∈ A. </fr:tex>I holds at <fr:tex>x = U(c)</fr:tex>.
             </fr:p>
@@ -976,9 +973,8 @@ addr="hejohns-0007">the precusor</fr:link> to each
                     functor in turn, just knowing the other is a well-defined
                     functor.
                 </fr:li></fr:ul></fr:li>
-        <fr:li>
-            (II) wts II <fr:tex>⟹  \overline {F}</fr:tex> is a functor.
-            <fr:p>
+        <fr:li><fr:p>
+                (II) wts II <fr:tex>⟹  \overline {F}</fr:tex> is a functor.
                 This is dual.
             </fr:p></fr:li></fr:ul></fr:mainmatter></fr:tree><fr:tree
 xmlns:fr="http://www.jonmsterling.com/jms-005P.xml"
@@ -1113,15 +1109,15 @@ root="false"><fr:frontmatter><fr:anchor>265</fr:anchor><fr:taxon>Proposition</fr
 href="hejohns.xml"
 type="local"
 addr="hejohns">Johnson He</fr:link></fr:author></fr:authors><fr:parent>hejohns-000E</fr:parent></fr:frontmatter><fr:mainmatter><fr:p>
-        An adjunction core extends to an adjuction iff (<fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex>
+        An adjunction core extends to an adjuction iff <fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex>
         <fr:link
 href="subb-000E.xml"
 type="local"
-addr="subb-000E">I</fr:link> commutes) or (<fr:tex>∀x,y ∈ X. a ∈ A.</fr:tex> <fr:link
+addr="subb-000E">I</fr:link> commutes, and iff <fr:tex>∀x,y ∈ X. a ∈ A.</fr:tex> <fr:link
 href="subbb-000E.xml"
 type="local"
 addr="subbb-000E">II</fr:link>
-        commutes).
+        commutes.
         The adjunction is unique when it exists.
     </fr:p><fr:p>
         The <fr:link
@@ -1193,14 +1189,14 @@ addr="sub-0007">the short proof</fr:link>
 href="street-2012.xml"
 type="local"
 addr="street-2012">the
-        paper</fr:link>.  It's also how you'd attack <fr:link
+        paper</fr:link>. It's also how you'd attack <fr:link
 href="hejohns-0007.xml"
 type="local"
 addr="hejohns-0007">the
         precursor</fr:link> head-on. The utility is that it holds in
         enriched categories.
     </fr:p><fr:p>
-        The forwards direction is trivial.
+        The forward directions are trivial.
         Suppose <fr:tex>(F, U, (π_{a, x})_{a ∈ A, x ∈ X})</fr:tex> extends to <fr:tex>\overline {F}  ⊣_π  \overline {U}</fr:tex>.
         Then <fr:link
 href="subb-000E.xml"
@@ -1211,14 +1207,11 @@ addr="subb-000E">I</fr:link> expresses that <fr:tex>∀g : A(a, b). ∀f : A(F(x
         <fr:link
 href="subbb-000E.xml"
 type="local"
-addr="subbb-000E">II</fr:link> expresses something similar, but we've already shown
-        the forwards direction.
+addr="subbb-000E">II</fr:link> expresses something similar (dual).
     </fr:p><fr:p>
-        The nontrivial direction is the backwards direction.
-        We case on whether I or II holds.
-    </fr:p><fr:ul><fr:li>
-            (I) wts I <fr:tex>⟹  \overline {U}</fr:tex> is a functor.
-            <fr:p>
+        The nontrivial directions are the backward directions.
+    </fr:p><fr:ul><fr:li><fr:p>
+                (I) wts I <fr:tex>⟹  \overline {U}</fr:tex> is a functor.
                 Suppose <fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex> I holds.
                 Then in particular, <fr:tex>∀c ∈ A. </fr:tex>I holds at <fr:tex>x = U(c)</fr:tex>.
             </fr:p>
@@ -1305,9 +1298,8 @@ addr="hejohns-0007">the precusor</fr:link> to each
                     functor in turn, just knowing the other is a well-defined
                     functor.
                 </fr:li></fr:ul></fr:li>
-        <fr:li>
-            (II) wts II <fr:tex>⟹  \overline {F}</fr:tex> is a functor.
-            <fr:p>
+        <fr:li><fr:p>
+                (II) wts II <fr:tex>⟹  \overline {F}</fr:tex> is a functor.
                 This is dual.
             </fr:p></fr:li></fr:ul></fr:mainmatter></fr:tree><fr:tree
 xmlns:fr="http://www.jonmsterling.com/jms-005P.xml"

diff --git a/_site/forest/hejohns-0008.xml b/_site/forest/hejohns-0008.xml
@@ -454,15 +454,15 @@ root="false"><fr:frontmatter><fr:anchor>265</fr:anchor><fr:taxon>Proposition</fr
 href="hejohns.xml"
 type="local"
 addr="hejohns">Johnson He</fr:link></fr:author></fr:authors><fr:parent>hejohns-000E</fr:parent></fr:frontmatter><fr:mainmatter><fr:p>
-        An adjunction core extends to an adjuction iff (<fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex>
+        An adjunction core extends to an adjuction iff <fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex>
         <fr:link
 href="subb-000E.xml"
 type="local"
-addr="subb-000E">I</fr:link> commutes) or (<fr:tex>∀x,y ∈ X. a ∈ A.</fr:tex> <fr:link
+addr="subb-000E">I</fr:link> commutes, and iff <fr:tex>∀x,y ∈ X. a ∈ A.</fr:tex> <fr:link
 href="subbb-000E.xml"
 type="local"
 addr="subbb-000E">II</fr:link>
-        commutes).
+        commutes.
         The adjunction is unique when it exists.
     </fr:p><fr:p>
         The <fr:link
@@ -534,14 +534,14 @@ addr="sub-0007">the short proof</fr:link>
 href="street-2012.xml"
 type="local"
 addr="street-2012">the
-        paper</fr:link>.  It's also how you'd attack <fr:link
+        paper</fr:link>. It's also how you'd attack <fr:link
 href="hejohns-0007.xml"
 type="local"
 addr="hejohns-0007">the
         precursor</fr:link> head-on. The utility is that it holds in
         enriched categories.
     </fr:p><fr:p>
-        The forwards direction is trivial.
+        The forward directions are trivial.
         Suppose <fr:tex>(F, U, (π_{a, x})_{a ∈ A, x ∈ X})</fr:tex> extends to <fr:tex>\overline {F}  ⊣_π  \overline {U}</fr:tex>.
         Then <fr:link
 href="subb-000E.xml"
@@ -552,14 +552,11 @@ addr="subb-000E">I</fr:link> expresses that <fr:tex>∀g : A(a, b). ∀f : A(F(x
         <fr:link
 href="subbb-000E.xml"
 type="local"
-addr="subbb-000E">II</fr:link> expresses something similar, but we've already shown
-        the forwards direction.
+addr="subbb-000E">II</fr:link> expresses something similar (dual).
     </fr:p><fr:p>
-        The nontrivial direction is the backwards direction.
-        We case on whether I or II holds.
-    </fr:p><fr:ul><fr:li>
-            (I) wts I <fr:tex>⟹  \overline {U}</fr:tex> is a functor.
-            <fr:p>
+        The nontrivial directions are the backward directions.
+    </fr:p><fr:ul><fr:li><fr:p>
+                (I) wts I <fr:tex>⟹  \overline {U}</fr:tex> is a functor.
                 Suppose <fr:tex>∀a,b ∈ A. ∀x ∈ X.</fr:tex> I holds.
                 Then in particular, <fr:tex>∀c ∈ A. </fr:tex>I holds at <fr:tex>x = U(c)</fr:tex>.
             </fr:p>
@@ -646,9 +643,8 @@ addr="hejohns-0007">the precusor</fr:link> to each
                     functor in turn, just knowing the other is a well-defined
                     functor.
                 </fr:li></fr:ul></fr:li>
-        <fr:li>
-            (II) wts II <fr:tex>⟹  \overline {F}</fr:tex> is a functor.
-            <fr:p>
+        <fr:li><fr:p>
+                (II) wts II <fr:tex>⟹  \overline {F}</fr:tex> is a functor.
                 This is dual.
             </fr:p></fr:li></fr:ul></fr:mainmatter></fr:tree><fr:tree
 xmlns:fr="http://www.jonmsterling.com/jms-005P.xml"