tag:blogger.com,1999:blog-37766505901765525302024-03-05T12:45:52.311-08:00TeX-nical StuffRandom scratchwork on Mathematical Physics and sometimes Programming. Diagrams done with <a href="http://www.paultaylor.eu/diagrams/"><code>commutative</code></a> and <a href="http://www.nought.de/tex2im.php"><code>tex2im</code></a>. <br><br>"<em>Dimidium facti qui coepit habet: sapere aude!</em>" (He who has begun is half done: dare to know!) - Horace.pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.comBlogger82125tag:blogger.com,1999:blog-3776650590176552530.post-91372280269163161172022-11-21T15:30:00.001-08:002022-11-21T15:30:00.155-08:00Emacs Macro: PDF Creation Date for LaTeX<p>
I have been using Emacs...for a while now. I've found it useful to automate away common tasks using Lisp functions. One that has been recurring: write the creation date. Using something like <code>datetime2</code> package in LaTeX (and assuming you're using PDFlatex), then the following command can be used to automatically determine the date and time you started writing:
</p>
<pre>
(defun latex-created ()
(interactive)
(insert (format-time-string "\\DTMsavetimestamp{creation}{%FT%T%z}\n"))
(insert "{\\DTMsetstyle{pdf}\\pdfinfo{/CreationDate (\\DTMuse{creation})}}\n")
(insert "\\date{\\DTMusedate{creation}}\n"))
</pre>
<p>
The other bit of advice I have is to use Yasnippets. It's so much easier to start a new line, enter "d", hit tab, and have it expand to a definition environment (or have "thm" expand to a theorem environment). I have written a <a href="https://github.com/pqnelson/dotfiles/tree/master/.emacs.d/snippets/latex-mode">few snippets</a> and found them wonderful.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-61192630547854583552022-04-26T16:30:00.089-07:002022-04-27T11:27:03.840-07:00Zettelkasten workflow<p>
I was asked about the details concerning my Zettelkasten (last time I checked, I had an estimated 7920 slips in it, which motivated the question). I thought I would write them down here with some examples.
</p>
<p>
The basic workflow boils down to:
</p>
<ol>
<li>Pick some reading material</li>
<li>Read it</li>
<li>Summarize the reading material in "literature notes"</li>
<li>Write some "permanent notes"</li>
<li>Integrate the "permanent notes" in my "zoo" [Zettelkasten]</li>
<li>Think about stuff</li>
<li>Write a manuscript using my permanent notes</li>
<li>Questions tend to crop up while writing a manuscript, which guides my choice of next reading material</li>
</ol>
<h1>Literature Notes</h1>
<section class="definition" style="border: 1px solid black">
<p><b>Definition.</b>
A <dfn>Literature Note</dfn> is some writing which occurs when reading an article or book. Its contents vary considerably, but are used to create permanent notes. The literature notes are stored in a separate "shoe box".
</p>
</section>
<p>
The content of the literatuer notes varies depending on how familiar I am with the subject, or whether I can "see where it's going". These are written on quarter-slips of printer paper which are 4.25-inches wide and 5.5-inches tall. I also draw a stripe down the "top" using a blue highlighter, so I can see if I accidentally placed one in my Zettelkasten. [I store literature notes in a "bibliography shoe box".]
</p>
<figure>
<div class="separator" style="clear: both;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgmTdeRVZw8yP0xwI-jPUn-yPzp94cGrxN5LOFo1NhmZN6tZYjtgCB51ipP1rccv53alTlD1Z3igWoXToazoJS16OUtqReMrsVCOivQagyJlURB4T7vUsCzUfpj24p-cAIuOyk1GaTd1-D0sYnJbd0QSkBpe7wXXiq0jvxUz3s6tgj0Pxq4M0YREX9h/s1600/literature-notes-mac-lane.png" style="display: block; padding: 1em 0; text-align: center; "><img style="border: 1px solid black" alt="" border="0" data-original-height="534" data-original-width="416" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgmTdeRVZw8yP0xwI-jPUn-yPzp94cGrxN5LOFo1NhmZN6tZYjtgCB51ipP1rccv53alTlD1Z3igWoXToazoJS16OUtqReMrsVCOivQagyJlURB4T7vUsCzUfpj24p-cAIuOyk1GaTd1-D0sYnJbd0QSkBpe7wXXiq0jvxUz3s6tgj0Pxq4M0YREX9h/s1600/literature-notes-mac-lane.png"/></a></div>
<figcaption>Figure 1. A [clipped] literature note from Mac Lane's <cite class="book">Categories for the Working Mathematician</cite>.</figcaption>
</figure>
<p>
If I'm having difficulty with some portion of an article or book, I sometimes look for other explanations, and insert "citations" to them. (Basically, a sentence like, "I honestly cannot follow [author] here, but I found [other reference] useful, specifically [section].")
</p>
<p>
Note I usually write small, and this is kinda large for my writing: it's about 3/16 inches, or 0.5 centimeters, for a line's height. I do not place lined paper behind the slip as I write, so it can get pretty curvy by accident.
</p>
<p>
The back of the literature notes include bibliographic information, and when I read it. This may include a "counter" for long chapters, which is just something like "(part 3 of <var>N</var>)". For technical articles, I also include the journal information. The idea is, if I completely lose access to my computer and papers, I can look up the source material again. Consequently, I give as much bibliographic information as possible.
</p>
<figure>
<div class="separator" style="clear: both;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEj5jZWq-rnqORStiNFF6JQwlvVDOwO-RajRAkG2oT0PowLotEBdHd-1stgFXYtEJ9FP0vWd553gpynxYEc9Wg2LlPzKvYxzECdEF1gwz673sXDhi-6EPAgVn5Kbh0K12yEUoRKYKVvVyrKKm71q0oLXEF4kx1yFB5rV-hFhzjH0NK3_m6GlY-OO7DBu/s1600/literature-notes-mac-lane-back.png" style="display: block; padding: 1em 0; text-align: center; "><img style="border: 1px solid black" alt="" border="0" data-original-height="536" data-original-width="420" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEj5jZWq-rnqORStiNFF6JQwlvVDOwO-RajRAkG2oT0PowLotEBdHd-1stgFXYtEJ9FP0vWd553gpynxYEc9Wg2LlPzKvYxzECdEF1gwz673sXDhi-6EPAgVn5Kbh0K12yEUoRKYKVvVyrKKm71q0oLXEF4kx1yFB5rV-hFhzjH0NK3_m6GlY-OO7DBu/s1600/literature-notes-mac-lane-back.png"/></a></div>
<figcaption>Figure 2. The back of the literature note from figure 1.</figcaption>
</figure>
<p>
I can refer to my literature notes when writing a permanent note, but I do not permit myself to refer to the original source when writing permanent notes. If I find I need to refer to the original source, I take that to mean my literature note-taking process was lacking somehow.
</p>
<p>
There are times when, for example, I read a source particularly from one perspective. (E.g., "How can this article about quantum hydrodynamics be used in this particular calculation I'm trying to do?") Later on, I realize there was some important aspect I neglected to take notes on (e.g., "Oh, that article about quantum hydrodynamics revived the 'particle model tradition' of Stokes, I totally missed that."). In that case, I re-read the article or book, and because I note when I read it on the back...it acts like a note to "future me" that there was some material I missed in the reading.
</p>
<p>
(And, for the record, I organize the literature notes by author-year-title.)
</p>
<h1>Permanent Notes</h1>
<section class="definition" style="border: 1px solid black">
<p><b>Definition.</b>
A <dfn>Permanent Note</dfn> is some writing which is given an ID number, a "title", and some content; it is stored in the Zettelkasten.
</p>
</section>
<p>
Most of my notes are mathematical in nature, or written in a "mathematical style". I mean to say, I write them using "mathematical registers" to classify the sort of statement (theorem, example, definition, remark, etc.) and a summary of the result. Then the body of the slip of paper contains more precise details.
</p>
<figure>
<div class="separator" style="clear: both;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgvAXdknL8tNxTY2B73BevhHvzEFdbyyaJrAboK-SMDhebWEKxVOH0fmIujOM79iwkA9kq3Q5_RGdB0lCg66QYiGEyNQhJoA_0LmMju_YKMLZoAqBCWYanMBCoODdZcRSJRjNM5Qd_nhf6lUl3yEHj8x4l9THeWTBLkSZ1ztX2ffGl_K0lPOVlhyOZv/s1600/zettel-thm-bounded-sequence.png" style="display: block; padding: 1em 0; text-align: center; "><img style="border: 1px solid black" alt="" border="0" data-original-height="354" data-original-width="531" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgvAXdknL8tNxTY2B73BevhHvzEFdbyyaJrAboK-SMDhebWEKxVOH0fmIujOM79iwkA9kq3Q5_RGdB0lCg66QYiGEyNQhJoA_0LmMju_YKMLZoAqBCWYanMBCoODdZcRSJRjNM5Qd_nhf6lUl3yEHj8x4l9THeWTBLkSZ1ztX2ffGl_K0lPOVlhyOZv/s1600/zettel-thm-bounded-sequence.png"/></a></div>
<figcaption>Figure 3. An example of a permanent note [front side].</figcaption>
</figure>
<p>
I write on printer paper cut into quarters, so this is 5.5-inches wide and 4.25 inches tall. When writing on the paper, I have a college-ruled lined paper behind the quarter slip (which is why it appears so straight and clean).
</p>
<p>
<b>ID Numbering.</b> I should mention the ID number (the "6.1.2/3b" in the upper left-hand corner) has the following BNF grammar:
</p>
<pre>
⟨<i>id</i>⟩ ::= ⟨<i>folder-part</i>⟩ "/" ⟨<i>file-part</i>⟩
⟨<i>folder-part</i>⟩ ::= ⟨<i>positive integer</i>⟩
| ⟨<i>positive integer</i>⟩ "." ⟨<i>folder-part</i>⟩
⟨<i>file-part</i>⟩ ::= ⟨<i>positive integer</i>⟩
| ⟨<i>positive integer</i>⟩ ⟨<i>lowercase letter</i>⟩
| ⟨<i>positive integer</i>⟩ ⟨<i>lowercase letter</i>⟩ ⟨<i>file-part</i>⟩
</pre>
<p>
The "folder part" encodes the generic subject of the slip. For example, "6.1.2" is the folder part for the slip given. Here "6" refers to "Mathematical analysis", "6.1" refers to "Real analysis", and "6.1.2" refers to sequences of real numbers. Observe, the folder part moves from more general ("Real analysis") to the more specific; this is characteristic of all "folders" in my Zettelkasten.
</p>
<p>
The "file part" encodes the placement of a slip "inside" a "folder". The idea is that I'm sending "telegrams" to an intelligent (but completely ignorant) colleague. My colleague has never heard of real analysis (or anything else besides arithmetic and spelling). I need to order my telegrams somehow. The first attempt is to use <dfn>Threads</dfn>, just a sequence of numbers.
</p>
<p>
But when I want to discuss further an aspect of a thread (like, I want to pause and give a "sub-thread" consisting of examples), then I need to <dfn>Branch</dfn> off a slip to talk about some specific aspect. A single slip may have zero or more branches. I indicate a branch by writing a letter. Usually "a" is reserved for examples (unless there is a critical remark necessary to clarify something), then "b" is reserved for theorems about a concept.
</p>
<p>
For the example given, there is some fibbing here. That is to say, the ID number should really be "6.1.2/3b1". Why? Because letters act like different "flavors" of decimal separations. There shouldn't be any privilege to them (e.g., "a" is not more important than "b", there is no sense of priority, etc.). I haven't added any further theorems concerning "6.1.2/3", so I lazily truncated the ID number of the example to "6.1.2/3b".
</p>
<p>
<b>Title.</b> The title is usually of the form:
</p>
<pre>
⟨<i>title</i>⟩ ::= ⟨<i>register</i>⟩ ". " ⟨<i>summary</i>⟩
</pre>
<p>
As a mathematician, I habitually write "definition", "theorem", "proof", "remark", "example", etc., in an abbreviated form ["defn", "thm", "pf", "rmk", "ex", respectively]. Then I write a human readable summary of the result, like "Convergent sequences are bounded".
</p>
<p>
I <a href="https://texnicalstuff.blogspot.com/2022/03/zettelkastens-and-literate-programs.html">previously mentioned</a> introducing a "code" register when writing literate programs, and discussed the content of such notes.
</p>
<p>
Recently, I have also been experimenting with writing notes on history, and I have found registers of little use there. So your mileage may vary.
</p>
<figure>
<div class="separator" style="clear: both;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEh2ZekkAyX0h3Xb-5g6oS-BY90rVIAHFUS62dLmxsvZ_2QcPcI32zTCJEqPtqI06X6UXBScnagMdOxmHIJ_OaLaJ5z0SvIIlTIgCWdOmCjE2uy6vQ7YOuWRAQTIh1KzJ98PXpriXEbdJho-R4tH3FD4Pip-onN8N0J9g02CqjkYH7Z4xdp0Lo7c3SBl/s1600/zettel-link.png" style="display: block; padding: 1em 0; text-align: center; "><img style="border: 1px solid black" alt="" border="0" data-original-height="388" data-original-width="534" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEh2ZekkAyX0h3Xb-5g6oS-BY90rVIAHFUS62dLmxsvZ_2QcPcI32zTCJEqPtqI06X6UXBScnagMdOxmHIJ_OaLaJ5z0SvIIlTIgCWdOmCjE2uy6vQ7YOuWRAQTIh1KzJ98PXpriXEbdJho-R4tH3FD4Pip-onN8N0J9g02CqjkYH7Z4xdp0Lo7c3SBl/s1600/zettel-link.png"/></a></div>
<figcaption>Figure 4. Another example of a permanent note [front side]. NOTE: all links are written in red ink (using non-red ink was a bad idea).</figcaption>
</figure>
<p>
Also worth mentioning, the first "folder" is about my Zettelkasten's conventions. An example slip from this "folder" is given in Figure 4.
</p>
<p>
<b>Content of a permanent note.</b> This is pretty subjective, and varies considerably. For mathematics, I have a great luxury here since every "register" is a separate slip.
</p>
<p>
I have found it useful for propositions [lemmas, theorems, corollaries, etc.] to give a "proof sketch" below the theorem statement. If there is some justification for a step, it's a branch off the slip.
</p>
<p>
Examples are just special kinds of propositions, and the emphasis of its content is the proof.
</p>
<p>
I can give some concrete "tricks" to writing permanent notes, they both boil down to relating new material to existing content already in the Zettelkasten.
</p>
<p>
<b>Example: Creating examples.</b> A useful exercise is to go back to examples existing in my Zettelkasten, and try to use it as an example of the new material. For instance, I have the "symmetries of the tetrahedron" as an example of a group. When reading figure 1, I may pose the question: can we express the symmetries of the tetrahedron as a universal arrow? (Not in any obvious way, but there are other gadgets which may be a universal arrow, so I keep looking.) When I find an example [call it a "widget"], I create a new permanent note entitled "Ex: widget (Universal Arrow)", the first sentence is "A widget [link] is a universal arrow." The "[link]" refers back to the original slip which first discussed the "widget".
</p>
<p>
Usually this process is more "subconscious" than actually flipping through every slip in my Zettelkasten. With the universal arrow example, I usually know an example would be an algebraic gadget, so I can restrict my focus to the "Abstract algebra" folder; even then, I can restrict attention to a few "subfolders".
</p>
<p>
<b>Example: Translating content.</b> Another way to approach creating permanent notes is to "translate" old material from a different domain to whatever I just read. For example, I learned the <a href="https://encyclopediaofmath.org/wiki/Krull-Remak-Schmidt_theorem">Krull-Schmidt theorem</a> for rings and modules. But currently I am studying finite group theory. Could I frame an analogous theorem for groups?
</p>
<p>
<b>Convention: formal proof sketches.</b> I try to write the mathematical proofs using Wiedijk's <a href="http://www.cs.ru.nl/F.Wiedijk/notes/mv.pdf">Mathematical Vernacular</a>, which is a synthesis of formal proof steps while leaving the terms and formulas informal. I also write "big step proofs", or what Wiedijk calls <a href="http://www.cs.ru.nl/F.Wiedijk/pubs/sketches2.pdf">formal proof sketches</a>.
</p>
<p>
<b>Back of permanent notes.</b> On the back side of a permanent note is a list of references which were used for the slip. They are lists to where one could find the same result in the literature which I've read, and refer to entries in my "bibliography apparatus".
</p>
<p>
<b>Integration into the Zettelkasten.</b> Usually, I study a book or article, write a number of permanent notes without any ID number. Only after I have extracted all the information needed from my source, I begin to think about how to integrate the new permanent notes into my Zettelkasten.
</p>
<p>
Sometimes the order of material in a book is "backwards" (it happens a lot in physics), so the corresponding permanent notes are in reverse order. Less frequently, the material needs to be partitioned to separate parts of the Zettelkasten. There has not been a time when the material is "completely disconnected" from each other, in the sense that they are added to different threads.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-54283773440524786602022-04-26T16:00:00.003-07:002022-05-26T08:16:51.663-07:00How big will the classification of finite simple groups be?<p>
Gorenstein, Lyons, and Solomon (and friends) have been writing a consolidated proof for the classification theorem for finite simple groups...since 1994. In fact, it's still a work in progress. How big will it be?
</p>
<p>
Thus far, nine volumes have been published:
</p>
<table style="margin: 0 auto; text-align: center;">
<thead>
<th>Volume Number</th><th>First page number</th><th>Bibliography Page number</th><th>Number of Pages</th>
</thead>
<tbody>
<tr><td><a href="https://bookstore.ams.org/surv-40-10s/">1</a></td><td>22</td><td>159</td><td>137</td></tr>
<tr><td><a href="https://bookstore.ams.org/surv-40-2/">2</a></td><td>14</td><td>216</td><td>202</td></tr>
<tr><td><a href="https://bookstore.ams.org/surv-40-3/">3</a></td>
<td>18</td>
<td>420</td>
<td>402</td></tr>
<tr><td><a href="https://bookstore.ams.org/surv-40-4/">4</a></td>
<td>18</td><td>350</td><td>332</td></tr>
<tr><td><a href="https://bookstore.ams.org/surv-40-5/">5</a></td>
<td>14</td><td>476</td><td>462</td></tr>
<tr><td><a href="https://bookstore.ams.org/surv-40-6/">6</a></td>
<td>14</td><td>532</td><td>518</td></tr>
<tr><td><a href="https://bookstore.ams.org/surv-40-7/">7</a></td>
<td>12</td><td>352</td><td>340</td></tr>
<tr><td><a href="https://bookstore.ams.org/surv-40-8/">8</a></td>
<td>14</td><td>498</td><td>484</td></tr>
<tr><td><a href="https://bookstore.ams.org/surv-40-9/">9</a></td>
<td>12</td><td>530</td><td>518</td></tr>
</tbody>
</table>
<p>
At present, there is an expected additional 4 volumes coming (according to David Roberts's <a href="https://mathoverflow.net/a/217397/22457">answer</a> on Mathoverflow). Performing a linear regression on the number of pages in terms of the volume number, we can make a prediction. Here's the R code doing this:
</p>
<pre>
df <- data.frame(vol = 1:9,
start=c(22,14,18,18,14,14,12,14,12),
bib=c(159,216,420,350,476,532,352,498,530));
df$pgs <- df$bib - df$start;
lm0 <- lm(pgs ~ vol, data=df);
summary(lm0);
# Call:
# lm(formula = pgs ~ vol, data = df)
#
# Residuals:
# Min 1Q Median 3Q Max
# -118.29 -53.62 -14.82 84.78 105.84
#
# Coefficients:
# Estimate Std. Error t value Pr(>|t|)
# (Intercept) 174.56 62.68 2.785 0.0271 *
# vol 40.53 11.14 3.639 0.0083 **
# ---
# Signif. codes: 0 ‘***’ 0.001 ‘**’ 0.01 ‘*’ 0.05 ‘.’ 0.1 ‘ ’ 1
#
# Residual standard error: 86.27 on 7 degrees of freedom
# Multiple R-squared: 0.6542, Adjusted R-squared: 0.6048
# F-statistic: 13.24 on 1 and 7 DF, p-value: 0.008296
predict(lm0, data.frame(vol=c(10,11,12,13)))
# 1 2 3 4
# 579.8889 620.4222 660.9556 701.4889
sum(df$pgs)
# [1] 3395
sum(predict(lm0, data.frame(vol=c(10,11,12,13)))) + sum(df$pgs)
# [1] 5957.756
</pre>
<p>
<b>Tl;dr:</b> the classification of finite simple groups is expected to be around 5957 pages, but could ostensibly reach up to 8243 pages.
</p>
<section>
<h2>Addendum</h2>
<p>
We can improve the estimate by dropping the constant term, and estimating the "additional pages" compared to the first volume:
</p>
<pre>
df <- data.frame(vol = 1:9,
start=c(22,14,18,18,14,14,12,14,12),
bib=c(159,216,420,350,476,532,352,498,530));
df$pgs <- df$bib - df$start;
df2 <- data.frame(vol = 1:9,
pgs=df$pgs - df$pgs[1]);
lm0 <- lm(pgs ~ 0 + vol, data=df2);
summary(lm0)
# Call:
# lm(formula = pgs ~ 0 + vol, data = df2)
#
# Residuals:
# Min 1Q Median 3Q Max
# -122.24 -37.17 -24.70 92.68 125.61
#
# Coefficients:
# Estimate Std. Error t value Pr(>|t|)
# vol 46.463 4.901 9.48 1.26e-05 ***
# ---
# Signif. codes: 0 ‘***’ 0.001 ‘**’ 0.01 ‘*’ 0.05 ‘.’ 0.1 ‘ ’ 1
#
# Residual standard error: 82.75 on 8 degrees of freedom
# Multiple R-squared: 0.9183, Adjusted R-squared: 0.908
# F-statistic: 89.86 on 1 and 8 DF, p-value: 1.263e-05
predict(lm0, data.frame(vol=c(10,11,12,13))) + df$pgs[1]
# 1 2 3 4
# 601.6316 648.0947 694.5579 741.0211
sum(predict(lm0, data.frame(vol=c(10,11,12,13))) + 137) + sum(df$pgs)
# [1] 6080.305
</pre>
<p>
This gives us a better fit (adjusted R-squared of 0.908) with a better error estimate (with 95% probability, it will be 6080 pages give or take 40 pages).
</p>
<p>
<b>Tl;dr2:</b> the classification of finite simple groups can be expected to be around 6080±40 pages long.
</p>
</section>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-78617040390509136392022-03-23T16:00:00.001-07:002022-03-23T16:00:00.161-07:00Zettelkastens and Literate Programs<p>
I've been re-reading John Harrison's <cite class="book">Handbook of Practical Logic and Automated Reasoning</cite> (a wonderful book), with an eye towards writing notes for my <a href="https://political-arithmetic.blogspot.com/2020/07/zettelkasten.html">Zettelkasten</a>.
</p>
<p>
What I have done, out of habit, is I've reworked the code in Standard ML (as opposed to OCaml). I've added a "register" (mathematicians would recognize them as "theorem environments" in LaTeX) for source code, and the template for writing such notes on a 5.5 inch by 4.25 inch (A6) slip of paper looks like:
</p>
<table style="border: 1px solid #333">
<tr>
<td>[<var>id number</var>]</td><td></td><td style="text-align:right;"><u>Code</u> [<var>name of chunk</var>]</td>
</tr>
<tr><td colspan="3">[<var>English summary of the code, or the algorithm, or...</var>]</td></tr>
<tr><td style="border-top: 1px solid black;">⟨[<var>name of chunk</var>]⟩≡</td><td></td><td></td></tr>
<tr><td colspan="3">[<var>Standard ML code here</var>]</td></tr>
</table>
<p>
Just replace the bracketed italicized text (including the brackets) with your own text. I do write a horizontal line separating the "code block" from the "text block", and underline the "Code" part of the title.
</p>
<p>
I follow the general heuristics Knuth suggests for literate programming, even using the names of code chunks in angled braces as if they were statements. Following some of the <a href="https://smlfamily.github.io/history/index.html">early handwritten documents on Standard ML</a>, I underline keywords like "if", "then", "else", "case", "fun", etc., in the code block.
</p>
<p>
While reading Harrison's book, I add unit tests, write up examples, etc. This isn't done "in the abstract", I actually type the code up on a computer (e.g., <a href="https://gist.github.com/pqnelson/f618dfc7cb6874baadc7d98ad00fe48b">here</a> is my implementation of most of the propositional logic code).
</p>
<p>
One advantage to this is that we can prove properties about the code snippet in branches off the code zettel. Another advantage, giving a good human-level summary of the code snippet helps greatly with Harrison's book, since the techniques from chapter 3 make another appearance in chapter 6 (i.e., 300 pages later) and I forget some of the nuances surrounding the implementation ("Is <code>skolem</code> called before or after <code>nnf</code>?"), I can just glance at the snippets for guidance.
</p>
<p>
Another useful aspect of using a Zettelkasten for studying theorem provers is that it facilitates blending notes from multiple books seamlessly. I noticed this accidentally, when I was unsatisfied with Harrison's description of Herbrand universes, then started reading Chang and Lee's <cite class="book">Symbolic Logic and Mechanical Theorem Proving</cite> (1973) description of Herbrand universes.
</p>
<p>
There are other aspects of Zettelkasten which seems uniquely suitable for studying theorem provers, but I digress.
</p>
<p>
I'm experimenting with using a Zettelkasten for literate programming "by hand" more generally, which is a bizarre but fascinating experience, especially when exploring <a href="http://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html">monads in Standard ML</a>.
</p>
<p>
Anyways, I just wanted to make note of this quirky note-taking system for literate programming.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-82307649597114567502021-12-06T15:30:00.005-08:002021-12-09T09:51:03.763-08:00On Structured Proofs and the Declarative Proof Style<section>
<p>
<b>1.</b>
Suppose we have successfully formalized the classification theorem for
finite simple groups in your favorite theorem prover (Lean, HOL, Coq,
Mizar, whatever). In a century's time (or several centuries from now),
do you think your theorem prover will still be around and backwards
compatible? If not, what good would the formalization be?
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">1.1.</span> <span class="label">Remark (Concerns have been partially realized).</span>
We stress, despite the concerns raised being hypothetical and distant,
they have been partly realized already. The Automath project's
efforts to translate Landau's <em>Foundations of Analysis</em> would have
been lost to history but for Freek Wiedijk's heroic efforts. Or, hitting
closer to home for many, Lean 3 broke compatibility with Lean 2; and, as
I understand it, there still remains a large quantity of Lean 2
libraries not yet ported. Worse, Lean 4 broke compatibility with Lean 3,
and the Xena project's library has not yet ported to Lean 4. The idea
that we would encode mathematical knowledge in one single theorem prover
seems riskier than encoding it in natural language. Why not try to have
the best of both worlds?
</p>
</section>
<section>
<p>
<b>2. Readable Proofs.</b>
One of the roles for proofs in mathematics is
<em>communication</em>. Hence we need something analogous to the notion of
"readable code" in programming: readable proofs. Consider the
following proof, tell me what it does (no cheating!):
</p>
<pre>
prove
('!p q. p * p = 2 * q * q ==> q = 0',
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM 'EVEN') THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN 'm:num' SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL ['q:num'; 'm:num']) THEN
POP_ASSUM MP_TAC THEN CONV_TAC SOS_RULE);;
</pre>
<p>
Or the following:
</p>
<pre>
Proof.
rewrite EL2 with (p_prime := p_prime) (p_odd := p_odd) by (omega || auto).
rewrite EL2 with (p_prime := q_prime) (p_odd := q_odd) by (omega || auto).
rewrite m1_pow_compatible. rewrite <- m1_pow_morphism.
f_equal. rewrite <- QR6. unfold a. unfold b. auto.
rewrite <- Zmult_0_r with (n := (p - 1) / 2).
apply Zmult_ge_compat_l. omega. omega.
Qed.
</pre>
<p>
I honestly wouldn't guess the first example had to do with proving
${\sqrt{2}\notin\mathbb{Q}}$, nor would I have imagined the second had to do with
the law of quadratic recipricocity. (The first in HOL Light, the second
in Coq.) What do you suppose mathematicians of the 25th century would
think of these proofs? Would our efforts formalizing mathematics in a
theorem prover yield fruit akin to Euclid's <em>Elements</em>, or would it
be more indecipherable than Russell and Whitehead's <em>Principia</em>?
</p>
<p>
Hence, I would like to assess the following question:
</p>
<p>
</section>
<section class="proposition Puzzle">
<p>
<span class="number">3.</span> <span class="label">Puzzle.</span>
<i>What qualities make a proof "readable"?</i>
</p>
</section>
<section>
<p>
<b>4. Sources.</b>
We're not in the wilderness on this matter. Some very smart people have
thought very hard about this question. But we haven't progressed much in
the past few decades, compared to designing programming languages. We
all seem to draw waters from the same well.
</p>
<p>
Andrzej Trybulec created Mizar <a href="#matuszewskimizar">[10]</a> specifically for
readability. Over the years, Mizar went from an abstract idea to a
concrete realization, iteratively improving its input language to make
it resemble a working mathematician's proofs. A cynical critic may
deride Mizar as merely natural deduction in Pascal syntax, but that
concedes the point: it's readable and understandable on its own, without
relying on the computer to tell us the "proof state" and remaining
goals in a proof. (Empirically, it turns out that Mizar reflects how
mathematicians write, based on a cursory glance at 40k articles;
see <a href="http://mizar.uwb.edu.pl/forum/archive/1203/msg00030.html">Josef Urban's email</a>
to the Mizar mailing list.)
</p>
<p>
(For our earlier examples, I personally think that Mizar's proof of the theorem of quadratic recipricocity, <a href="http://www.mizar.org/version/current/mml/int_5.miz">Th49 of <code>int_5.miz</code></a>, while long, is clear and readable...even if I don't fully understand Mizar. Similarly, the proof that $\sqrt{2}\notin\mathbb{Q}$ is the first theorem in <a href="http://www.mizar.org/version/current/mml/irrat_1.miz"><code>irrat_1.miz</code></a>. It's longer than I would find in a textbook, as are all formal proofs, but I have no difficulty making sense of it.)
</p>
<p>
The other major source of inspiration, I think, is Mark Wenzel's Isar
front-end for Isabelle <a href="#wenzelphd-thesis">[13]</a> (and enlightening
discussion of a prototype <a href="#wenzeltphols99">[12]</a>). Here the system
<em>emerges</em> bottom-up, as discussed in §3.2 of Wenzel's
thesis <a href="#wenzelphd-thesis">[13]</a>. Other theorem provers attempted to
simply copy/paste Isar commands, but apparently they never caught on. I
suspect this is due to copying the superficialities, rather than drawing
upon the underlying principles, produced an awkward input language.
</p>
<p>
There are other sources worth perusing, like Zammit's "Structured Proof
Language" <a href="#zammitphd-thesis">[17]</a> among others. We also mention Isar
inspired many prototypes to adapt Mizar-style proofs to other theorem
provers (Corbineau's Czar <a href="#corbineau-czar">[2]</a>, Giero and Wiedijk's MMode <a href="#giero-wiedijk-mmode">[3]</a>,
Harrison's Mizar Mode for HOL <a href="#harrison-mizar-mode">[4]</a>).
Also worth mentioning is <span class="small-caps">ForTheL</span> <a href="#paskevich-forthel">[11]</a> which
emerged from the Soviet SAD theorem prover <a href="#lyaletski-sad">[9]</a>, possibly
a future input language for Lean.
</p>
<p>
I especially want to point out <span class="small-caps">ForTheL</span> <a href="#paskevich-forthel">[11]</a> as a stand-out, partly because it was designed behind the Iron Curtain, and partly because it's more of a controlled language which resembles natural language.
</p>
</section>
<section>
<p>
<b>5. Declarative proofs.</b>
One bit of terminology, John Harrison <a href="#harrisonproof-style">[5]</a> calls
the structured proof style "declarative style proofs", which seems
fine. Some fanatics of the procedural camp dislike the term. Giero and
Wiedijk <a href="#giero-wiedijk-mmode">[3]</a> point out the
differences between procedural and declarative styles are:
</p>
<ol>
<li> a procedural proof generally run backward (from goal to the
assumptions), whereas declarative proofs run mostly forwards (from the
assumptions to the goal);
</li>
<li> a procedural proof generally does not have statements containing
the statements which occur in the proof states, whereas declarative
proofs do;
</li>
<li> a procedural proofs have few <a href="https://en.wikipedia.org/wiki/Cut_rule">proof cuts</a>, whereas declarative
proofs have nearly one cut for each proof step.
</li>
</ol>
<p>
It turns out these qualities <em>do</em> make a difference on the
readability of a proof script. But this is a bit like trying to learn an
author's writing style by examining the statistics of the author's
writing, like "Average number of words per sentence" or "Average
number of syllables per word".
</p>
</section>
<section>
<p>
<b>6. Natural deduction, vernacular.</b>
A key insight worth discussing further is that declarative/structured
proofs emerge from the natural deduction calculus. Curiously,
Jaśkowski <a href="#jaskowski-suppositions">[6]</a> (who invented natural deduction
independent of, and earlier than, Gentzen) does this in his original
paper. Wiedijk <a href="#wiedijk-mv">[15]</a> considers this avenue using a formal
grammar for the proof steps, leaving notions like "term" and
"formula" [i.e., the heart of a proposition/theorem] informal.
So far, so good; but this has been predominantly first-order logic. How
do we articulate readable proofs for type theory?
</p>
</section>
<section>
<p>
<b>7.</b>
We construct proof steps for a declarative proof style by assigning
"keywords" to rules of inference in natural deduction.
</p>
<p>
The problem with trying to find a readable proof format from natural
deduction for type theory is, well, there are a lot more inference rules
in the calculus of constructions (as opposed to, say, first-order
logic).
</p>
<p>
The Lean4 developers have unwittingly started the road to reinventing
lambda-typed lambda calculus, which has fewer rules and ostensibly could
be encoded into a declarative proof style input.
</p>
</section>
<section>
<p>
<b>8.</b>
One <em>linguistic</em> avenue may be found in de Bruijn's "mathematical
vernacular" <a href="#de-bruijn-vernacular">[1]</a>, which then evolved into
WTT <a href="#kamareddine-nederpelt-wtt">[7]</a>.
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">8.1.</span> <span class="label">Remark (Soft typing).</span>
What's worth noting is de Bruijn <a href="#de-bruijn-vernacular">[1]</a> states
in §1.17, "In particular we have a kind of meta-typing (the 'high
typing', see Section 3.6) in the language, whereas most other systems
would have such things in the metalanguage." We now call such 'high
typing' either 'soft typing' <a href="#wiedijk-soft-type">[16]</a>, or 'semi-soft
typing' <a href="#kaliszyk-rabe-language">[8]</a>.
</p>
</section>
<section>
<p>
<b>9.</b>
Another avenue would be to weaken existing structured proof formats, so
they become independent of foundations (e.g., instead of writing
"${x\in\mathbb{N}}$", we would write "${x}$ be a natural number" — type
theory provers would translate this into "${x{:}\mathbb{N}}$", and set theory
provers would translate this into "${x\in\mathbb{N}}$" as before).
</p>
<p>
If GNU Hurd's failures have taught us anything about engineering, it's
that "a bird in the hand is worth two in the bush." That is to say,
it's wiser to take an <em>existing</em> working framework, and modify it
slowly until it becomes what we want.
</p>
</section>
<section>
<p>
<b>10. Conclusion?</b>
If this post seems less-than-satisfying, that's probably because I've
only identified a problem.
No solutions have been offered. That's because this is a <em>hard problem</em>
somewhere between language design (very hard) and mathematical logic.
Since we lack a robust framework for designing languages, this is far
more of an art than science.
</p>
<p>
Although we have fewer than a half-dozen examples of declarative proof
styles (really, maybe 3?), we have some avenues of exploration. But the
design space may be much larger than we realize: we just lack the tools
to describe it adequately.
</p>
<p>
One closing thought I'd pass off, though, is that type theorists encode
logic in a rather protracted manner. It may be that structured proofs for
type theory would be forced to "compile down" into many more steps, or maybe
we just haven't adequately found a way to connect type theory to working
mathematics.
</p>
</section>
<h1>Bibliography</h1>
<ol>
<li><a name="de-bruijn-vernacular"></a> Nick de Bruijn,
"The Mathematical Vernacular".
In <em>Proceedings of the workshop on programming logic</em>
(eds. Peter Dybjer, Bengt Nordstrom, Kent Petersson, <em>et al</em>.),
1987. <a href="https://pure.tue.nl/ws/portalfiles/portal/4318923/599592.pdf">https://pure.tue.nl/ws/portalfiles/portal/4318923/599592.pdf</a>
<br /><br />
See also F.3 of <em>Selected Papers on Automath</em> for a revised
version of this manuscript.
</li>
<li><a name="corbineau-czar"></a> Pierre Corbineau,
"A Declarative Language For The Coq Proof Assistant".
In Marino Miculan, Ivan Scagnetto, and Furio Honsell, editors, <em>Types for Proofs and Programs, International Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007, Revised Selected Papers</em>,
volume 4941 of Lecture Notes in Computer Science, pages 69–84. Springer, 2007.
<a href="https://kluedo.ub.uni-kl.de/frontdoor/deliver/index/docId/2100/file/B-065.pdf">https://kluedo.ub.uni-kl.de/frontdoor/deliver/index/docId/2100/file/B-065.pdf</a>
</li>
<li><a name="giero-wiedijk-mmode"></a> Mariusz Giero and Freek Wiedijk,
"MMode: A Mizar Mode for the proof assistant Coq".
Technical report, ICIS, Radboud Universiteit Nijmegen, 2004.
<a href="https://www.cs.ru.nl/ freek/mmode/mmode.pdf">https://www.cs.ru.nl/ freek/mmode/mmode.pdf</a>
</li>
<li><a name="harrison-mizar-mode"></a> John Harrison,
"A Mizar Mode for HOL".
In <em>Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '96</em>, volume
1125 of LNCS, pages 203–220. Springer, 1996.
<a href="https://www.cl.cam.ac.uk/ jrh13/papers/mizar.html">https://www.cl.cam.ac.uk/ jrh13/papers/mizar.html</a>
</li>
<li><a name="harrisonproof-style"></a> John Harrison,
"Proof Style".
<a href="https://www.cl.cam.ac.uk/ jrh13/papers/style.html">https://www.cl.cam.ac.uk/ jrh13/papers/style.html</a>
</li>
<li><a name="jaskowski-suppositions"></a> Stanisław Jaśkowski
"On the Rules of Suppositions in Formal Logic".
<em>Studia Logica</em> <b>1</b> (1934) pp.5–32.
<a href="https://www.logik.ch/daten/jaskowski.pdf">https://www.logik.ch/daten/jaskowski.pdf</a>
</li>
<li><a name="kamareddine-nederpelt-wtt"></a> Fairouz Kamareddine and Rob Nederpelt,
"A refinement of de Bruijn's formal language of mathematics".
<em>Journal of Logic, Language, and Information</em> <b>13</b>, 3 (2004), pp.287–340
</li>
<li><a name="kaliszyk-rabe-language"></a> Cezary Kaliszyk and Florian Rabe,
"A Survey of Languages for Formalizing Mathematics".
<a href="https://arxiv.org/abs/2005.12876">https://arxiv.org/abs/2005.12876</a>
</li>
<li><a name="lyaletski-sad"></a> Alexander Lyaletski,
"Evidence Algorithm Approach to Automated Theorem Proving
and SAD Systems".
<a href="http://ceur-ws.org/Vol-2833/Paper_14.pdf">http://ceur-ws.org/Vol-2833/Paper_14.pdf</a>
</li>
<li><a name="matuszewskimizar"></a> Roman Matuszewski and Piotr Rudnicki,
"Mizar: The First 30 Years".
<em>Mechanized Mathematics and Its Applications</em> <b>4</b>, 1 (2005) pp.3–24.
<a href="http://mizar.org/people/romat/MatRud2005.pdf">http://mizar.org/people/romat/MatRud2005.pdf</a>
</li>
<li><a name="paskevich-forthel"></a> Andrei Paskevich,
"The syntax and semantics of the ForTheL language".
Manuscript dated December 2007,
<a href="http://nevidal.org/download/forthel.pdf">http://nevidal.org/download/forthel.pdf</a>
</li>
<li><a name="wenzeltphols99"></a> Markus Wenzel,
"Isar — a Generic Interpretative Approach to Readable Formal Proof
Documents".
In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, <em>Theorem Proving in Higher Order Logics, TPHOLs'99</em>, LNCS 1690, (c) Springer, 1999.
<a href="https://www21.in.tum.de/ wenzelm/papers/Isar-TPHOLs99.pdf">https://www21.in.tum.de/ wenzelm/papers/Isar-TPHOLs99.pdf</a>
</li>
<li><a name="wenzelphd-thesis"></a> Markus Wenzel,
"Isabelle/Isar — a versatile environment for human-readable formal
proof documents".
PhD thesis,
Institut für Informatik, Technische Universität München, 2002.
<a href="https://mediatum.ub.tum.de/doc/601724/601724.pdf">https://mediatum.ub.tum.de/doc/601724/601724.pdf</a>
</li>
<li> Markus Wenzel and Free Wiedijk.
"A comparison of the mathematical proof languages Mizar and Isar".
<em>Journal of Automated Reasoning</em> <b>29</b> (2002), pp.389–411.
<a href="https://www21.in.tum.de/~wenzelm/papers/romantic.pdf">https://www21.in.tum.de/~wenzelm/papers/romantic.pdf</a>
</li>
<li><a name="wiedijk-mv"></a> Freek Wiedijk,
"The Mathematical Vernacular".
Undated manuscript (available since at least 2004),
<a href="https://www.cs.ru.nl/ freek/notes/mv.pdf">https://www.cs.ru.nl/ freek/notes/mv.pdf</a>
</li>
<li><a name="wiedijk-soft-type"></a> Freek Wiedijk,
"Mizar's Soft Type System".
In: K.Schneider and J.Brandt (eds.), <em>Theorem Proving in Higher Order Logics 2007</em>, LNCS 4732, 383–399, 2007.
<a href="https://cs.ru.nl/F.Wiedijk/mizar/miztype.pdf">https://cs.ru.nl/F.Wiedijk/mizar/miztype.pdf</a>
</li>
<li><a name="zammitphd-thesis"></a> Vincent Zammit, (1999)
"On the Readability of Machine Checkable Formal Proofs".
PhD Thesis, Kent University, 1999.
<a href="https://kar.kent.ac.uk/21861/">https://kar.kent.ac.uk/21861/</a>
</li>
</ol>
pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-79064529919329318902021-12-02T16:00:00.014-08:002021-12-02T16:00:00.152-08:00Subgroups: Normal and...Abnormal...<section class="proposition Definition">
<p>
<span class="number">1.</span> <span class="label">Definition.</span> Let ${G}$ be a group; denote its group structure as the tuple ${(G,e_{G},\star_{G},\iota_{G})}$ where ${\iota_{G}}$ is the inverse operator, ${e_{G}}$ is the identity element, ${\star_{G}}$ is the binary composition operator. </p>
<p>
We define a <dfn>Subgroup</dfn> of ${G}$ to consist of a subset ${H\subseteq G}$ equipped with ${G}$'s group structure, i.e.,
<ol>
<li> the binary operation restricted to ${H}$, ${\star|_{H}\colon H\times H\to G}$ </li>
<li> the inverse operator ${\iota|_{H}\colon H\to H}$ </li>
<li> the identity element from ${G}$, ${e_{G}\in H}$ </li>
</ol>
such that
<ol>
<li> the group composition is closed on ${H}$, i.e., ${\{h_{1}\star|_{H}h_{2}|h_{1},h_{2}\in H\}\subseteq H}$ </li>
<li> group inversion is closed in ${H}$, i.e., ${\iota|_{H}(H)\subseteq H}$ </li>
<li> the usual group properties holds for this group structure induced on ${H}$. </li>
</ol>
If further ${H\neq G}$, we call ${H}$ a <dfn>Proper Subgroup</dfn> of ${G}$.
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">1.1.</span> <span class="label">Remark.</span> We denote ${H<G}$ if ${H}$ is a proper subgroup of ${G}$, and ${H\leq G}$ if ${H}$ is a generic subgroup of ${G}$.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">2.</span> <span class="label">Example (Trivial subgroups).</span> For any group ${G}$, there are always two subgroups available: ${G}$ itself, and the trivial subgroup ${\mathbf{1}}$ consisting of only the identity element. Since these subgroups come "for free", we call them <dfn>Trivial Subgroups</dfn>.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">3.</span> <span class="label">Example (Subgroups of dihedral group).</span> Let ${n\in\mathbb{N}}$ be greater than 2. Recall the dihedral group ${D_{n}}$ consists of rotations by ${2\pi/n}$ radians and reflections. We have two subgroups (at least): one generated by rotations alone, the other generated by reflections alone. </p>
<p>
The subgroup of rotations is a finite group consisting of ${n}$ elements. It's a cyclic group, isomorphic to ${\mathbb{Z}/n\mathbb{Z}}$. </p>
<p>
The subgroup of reflections is less exciting. There are two elements in it: reflection about the ${x}$-axis, and the identity transformation. This is a cyclic subgroup of order 2, isomorphic to ${\mathbb{Z}/2\mathbb{Z}}$.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">4.</span> <span class="label">Example (NON-Example: subset alone insufficient).</span> Consider modular arithmetic ${\mathbb{Z}/p\mathbb{Z}}$ for some prime ${p}$. This is a group consisting of a set ${\{0,1,\dots,p-1\}}$ equipped with addition modulo ${p}$, inversion maps ${m}$ to ${-m\equiv p-m\bmod{p}}$. </p>
<p>
Although the underlying set is a subset of the additive group ${\mathbb{Z}}$, the addition operation is a different function. Consequently, the group structure on ${\mathbb{Z}/p\mathbb{Z}}$ is <em>not equal</em> to the group structure on ${\mathbb{Z}}$. The moral: being a subset alone is insufficient.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">5.</span> <span class="label">Example (Symmetric group).</span> Let ${n\in\mathbb{N}}$. The symmetric group ${S_{n}}$ consists of permutations of the set ${\Omega_{n}=\{1,2,\dots,n\}}$. We can consider ${k\leq n}$, and then we have ${S_{k}\leq S_{n}}$ by restricting to permutations of the subset ${\Omega_{k}\subseteq\Omega_{n}}$.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">6.</span> <span class="label">Example.</span> Recall the general linear group ${\mathrm{GL}(n,\mathbb{R})}$ is the group of ${n\times n}$ invertible matrices over the real numbers, using matrix multiplication as its binary operator, and matrix inversion for its group inverse. Also recall the determinant
$$ \det\colon\mathrm{GL}(n,\mathbb{R})\to\mathbb{R}^{\times} \tag{1}$$
is a group morphism. Its kernel is a subgroup, called the <dfn>Special Linear Group</dfn>, denoted
$$ \mathrm{SL}(n,\mathbb{R})=\{M\in\mathrm{GL}(n,\mathbb{R})|\det(M)=1\}. \tag{2}$$
The reader can check it is closed under matrix multiplication and matrix inversion.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">7.</span> <span class="label">Example.</span> <a name="ex004-subgroupscommutator-subgroup"></a> Let ${G}$ be any group. If ${g_{1},g_{2}\in G}$, then their commutator is the element ${[g_{1},g_{2}]=g_{1}g_{2}g_{1}^{-1}g_{2}^{-1}\in G}$. We can construct the <dfn>Commutator Subgroup</dfn> of ${G}$, denoted ${[G,G]}$ or (more commonly but more confusingly) by ${G'}$ in the literature, by considering the subgroup generated by commutators of elements of ${G}$. Then an arbitrary element of the commutator subgroup looks like
$$ {} [g_{1},g_{2}][g_{3},g_{4}](\dots)[g_{2n-1},g_{2n}]\in[G,G] \tag{3}$$
and we use multiplication from ${G}$.
</p>
</section>
<h1>1. Exercises</h1>
</p>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">1.</span> Let ${H_{1}}$, ${H_{2}\leq G}$. Is ${H_{1}\cap H_{2}}$ a subgroup of ${G}$?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">2.</span> Let ${H_{1}}$, ${H_{2}\leq G}$. Is ${H_{1}\cup H_{2}}$ a subgroup of ${G}$?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">3.</span> Let ${\varphi\colon G\to K}$ be a group morphism. Is the image of ${\varphi}$ a subgroup of ${K}$? </p>
<p>
If ${H<K}$, is its preimage under ${\varphi}$ a subgroup of ${G}$?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">4.</span> Prove or find a counter-example: if ${G}$ is a cyclic group, then every subgroup is cyclic.
</p>
</section>
<h1>2. Normal Subgroups</h1>
</p>
<section>
<p>
<b>8.</b> <a name="chunk004-subgroupsmotivation-for-normal-subgroup"></a> The special linear group is a rather special situation (no pun intended). We can prove that, for any ${M\in\mathrm{SL}(n,\mathbb{R})}$ and for any ${T\in\mathrm{GL}(n,\mathbb{R})}$, we have ${XMX^{-1}\in\mathrm{SL}(n,\mathbb{R})}$. Really? Look, take its determinant:
$$ \begin{split} \det(XMX^{-1})&=\det(X)\det(M)\det(X)^{-1}\\ &=\det(M)=1. \end{split} \tag{4}$$
Its a property shared by the kernel of any group morphism ${\varphi\colon G\to H}$, we'd have ${k\in\ker(\varphi)}$ and ${g\in G}$ satisfy ${\varphi(gkg^{-1})=\varphi(g)\varphi(k)\varphi(g)^{-1}=\varphi(k)=e_{H}}$. This gives us a particular kind of subgroups. </p>
<p>
</section>
<section class="proposition Definition">
<p>
<span class="number">9.</span> <span class="label">Definition.</span> <a name="defn004-subgroupsnormal-subgroup"></a> Let ${G}$ be a group. A <dfn>Normal Subgroup</dfn> of ${G}$ consists of a subgroup ${H\leq G}$ such that
<ol>
<li> Closed under conjugation by group elements: for any ${h\in H}$ and for any ${g\in G}$, we have ${ghg^{-1}\in H}$. </li>
</ol>
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">9.1.</span> <span class="label">Remark.</span> Care must be taken for the normality property: all we ask is for ${ghg^{-1}\in H}$, <b>not</b> that ${ghg^{-1}=h}$.
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">9.2.</span> <span class="label">Remark (Notation).</span> We denote a normal subgroup ${N}$ of ${G}$ by ${N \triangleleft G}$, and ${N \trianglelefteq G}$ if ${N}$ is a proper normal subgroup of ${G}$. There are a couple ways of remembering which way the triangle points: one is that we just turn the subgroup notation ${N\leq G}$ into a triangle, the other is that it "snitches" on (i.e., points to) the normal subgroup.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">10.</span> <span class="label">Example.</span> The trivial subgroups are trivially normal.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">11.</span> <span class="label">Example.</span> For the Dihedral group ${D_{n}}$, we have a couple subgroups (one generated by rotations, the other generated by reflections). Is one of them normal? </p>
<p>
The rotation subgroup is generated by ${r}$ and satisfies ${r^{n}=1}$. The reflection subgroup is generated by ${s}$ and satisfies ${s^{2}=1}$. Together, they have ${s\circ r^{k}\circ s=r^{-k}}$. This implies the rotation subgroup is normal. </p>
<p>
Is the reflection subgroup normal?
</p>
</section>
<section class="proposition Theorem">
<p>
<span class="number">12.</span> <span class="label">Theorem.</span> <em><a name="thm004-subgroupsabelian-implies-subgroups-are-normal"></a> Let ${G}$ be a group. If ${G}$ is Abelian, then every subgroup ${H\leq G}$ is normal. </em>
</p>
</section>
<section class="proof">
<p>
<em>Proof:</em> Assume ${G}$ is Abelian. Let ${H\leq G}$ be an arbitrary subgroup of ${G}$, let ${g\in G}$ and ${h\in H}$ be arbitrary group elements. Then conjugation looks like ${g+h-g=h}$. Hence ${H}$ is a normal subgroup of ${G}$ by Definition <a href="#defn004-subgroupsnormal-subgroup">9</a>. ∎
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">13.</span> <span class="label">Example (Converse to Theorem 12 is false).</span> Consider the quaternion group ${Q_{8}}$ generated by ${i^{4}=j^{4}=k^{4}=(ijk)^{2}=1}$ and so ${ij=k}$, ${jk=i}$, ${j=ki}$. We really have only 8 elements in ${Q_{8}}$: ${1}$, ${-1}$, ${i}$, ${-i}$, ${j}$, ${-j}$, ${k}$, ${-k}$. But we only need two of the "purely imaginary" elements (${i}$, ${j}$, ${k}$) to generate the entire group. </p>
<p>
The proper subgroups would be generated from one complex generator, or from ${-1}$. We claim they are all normal. The case of ${\{\pm1\}<Q_{8}}$ is obviously normal, since ${x(-1)x^{-1}=-1}$ for any ${x\in Q_{8}}$. </p>
<p>
The reasoning for proper subgroups generated by one imaginary element resembles one another, so let's consider the subgroup generated by ${i}$. Then we see
$$ jij^{-1}=-jk=-i \tag{5}$$
and
$$ j^{3}ij^{-3}=(-j)i(j)=i. \tag{6}$$
Similarly we'd find, from ${i^{3}=-i}$, that
$$ ji^{3}j^{-1}=i \tag{7}$$
and
$$ j^{3}i^{3}j^{-3}=-i. \tag{8}$$
Thus the subgroup generated by ${i}$ is closed under conjugation from all elements from ${Q_{8}}$. </p>
<p>
Really? Well, any generic element in ${Q_{8}}$ looks like ${i^{m}j^{n}}$. Its inverse would be ${(i^{m}j^{n})^{-1}=j^{-n}i^{-m}}$. So conjugation by these elements would amount to multiplying the element ${i^{\ell}}$ from the subgroup by some ${i^{q}}$. But that's okay: elements of the form ${i^{q}}$ belong to the subgroup anyways.
</p>
</section>
<section class="proposition Theorem">
<p>
<span class="number">14.</span> <span class="label">Theorem.</span> <em> If ${\varphi\colon G\to H}$ is a group morphism, then ${\ker(\varphi)}$ is a normal subgroup of ${G}$. </em>
</p>
</section>
<p>
The proof was sketched earlier in <a href="#chunk004-subgroupsmotivation-for-normal-subgroup">§8</a>. </p>
<section class="proposition Theorem">
<p>
<span class="number">15.</span> <span class="label">Theorem.</span> <em> Let ${G}$ be a group. Every normal subgroup ${N\triangleleft G}$ is the kernel of some group morphism. </em>
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">15.1.</span> <span class="label">Remark.</span> We do not yet have the technology to prove this, yet, but it is true. Basically, we construct a morphism by taking ${g\in G}$ and mapping it to cosets ${gN=\{gn\in G|n\in N\}}$. The difficulty we have is that the image of this mapping is the collection of left cosets of ${N}$, which may or may not be a group. Further, it was rather arbitrary mapping it to <em>left</em> cosets of ${N}$: why not map ${g}$ to ${Ng=\{ng\in G|n\in N\}}$? Wouldn't these be distinct (i.e., not equal) mappings?
</p>
</section>
<h1>3. Exercises</h1>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">5.</span> Find the normal subgroups of the symmetric group ${S_{n}}$.
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">6.</span> Let ${G}$ be a group, ${H\triangleleft G}$ be a normal subgroup, and ${N\triangleleft H}$ be a normal subgroup of ${H}$. Is ${N}$ a normal subgroup of ${G}$?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">7.</span> Let ${G}$ be a group, recall the commutator subgroup from Example <a href="#ex004-subgroupscommutator-subgroup">7</a> that ${[G,G]}$ is a subgroup of ${G}$. Prove or find a counter-example: the commutator subgroup is a normal subgroup of ${G}$.
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">8.</span> Let ${\varphi\colon G\to H}$ be a group morphism, ${N\triangleleft G}$ be a normal subgroup. Is ${\varphi(N)}$ a normal subgroup of ${G}$? Consider the cases when ${\varphi}$ is injective, and when ${\varphi}$ is surjective.
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">9.</span> Let ${\varphi\colon G\to H}$ be a group morphism, and ${N_{H}\triangleleft G}$ be a normal subgroup. Is the preimage ${\varphi^{-1}(N_{H}) = \{g\in G|\varphi(g)\in N_{H}\}}$ a normal subgroup of ${G}$? Is it even a subgroup?
</p>
</section>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-80643487038635945882021-11-27T13:37:00.001-08:002023-12-28T11:36:07.000-08:00ISO-2145 numbering in Plain TeX<p>
I've been writing terse notes using something like the <a href="https://en.wikipedia.org/wiki/ISO_2145">ISO-2145</a> standard. Could some TeX macros be written to support writing such notes? Of course!
</p>
<p>
Like <code>amsart</code>'s subsections and subsubsections, I wanted my sections to be "runin style" (i.e., an unindented paragraph with a leading number, possibly with some label in bold, which is separated by vertical space from the previous paragraph). Following Knuth's WEB macros, I use <code>\M</code> to create a new unlabeled "section", and <code>\N{label}</code> to create a new labeled "section". These macros increment the section number, makes the section number (and label, if present) in bold, and does not indent the section's first paragraph.
</p>
<p>
But I wanted to allow arbitrary depths for "section numbers". What I did was treat the section number like a <a href="https://en.wikipedia.org/wiki/Stack_(abstract_data_type)">stack</a>. When I wanted to work on a new subsection level, I call <code>\M[1]</code> (or, for labeled subsections, <code>\N[1]{My label for the new subsection.}</code>).
</p>
<p>
If I want to "ascend" back to the parent section, I call <code>\M[-1]</code> (and <code>\N[-1]{...}</code>) which will pop the section stack, then increment the top of the stack.
</p>
<p>
Should I want to move more than one level up or down, I simply call <code>\M[n]</code> (or <code>\N[n]{...}</code>) for any nonzero integer <code>n</code>. If called with <code>n=0</code>, then it's treated as <code>\M</code> (and <code>\N{...}</code>, resp.).
</p>
<h1>Retrospective</h1>
<p>
If I were to do this all over again, I would probably use different variable names (for example, I would probably use <code>\chunkctr</code> instead of <code>\section</code> for the counter name). But I just wanted to see if it was possible.
</p>
<p>
Also, this code could work in LaTeX, but needs some small modifications. (Well, mostly dealing with making <code>\chunkctr</code> a bona fide counter, so <code>\refstepcounter</code> could use its magic for referencing things properly.)
</p>
<p>
I guess if I wanted to be fully general, I would have some additional parameters to allow customizing the vertical spacing for separating the sections, the horizontal space between the section number and the next symbol, etc.
</p>
<h1>Code and Worked Example</h1>
<pre>
\newcount\section
\section=0
% technically, sectionDepth is not needed, but it's to avoid popping off
% "too many sections"
\newcount\sectionDepth \sectionDepth=0
% \secprefix will be redefined to append the current section number
% followed by a period
\def\secprefix{}
% \pushSection simply appends "\the\section." to \secprefix's current value
\def\pushSection{
\global\advance\sectionDepth by1
\let\sectmp\secprefix
\xdef\secprefix{\sectmp\the\section.}
}
% update \secprefix from "a.b.(...).c.d" to "a.b.(...).c"
% and set \section to "d" (as a number)
\def\popSection{
\def\newPrefix{}
\global\advance\sectionDepth by-1
\def\updatePrefix##1.##2\endUpdate{
\ifx\relax##2 % if we are at the last number
% globally set \secprefix to be the leading (n-1) section numbers
\xdef\secprefix{\newPrefix}
% globally set \section to be the last section number from \secprefix
\global\section=\number##1
\else
\xdef\newPrefix{\newPrefix##1.}
\updatePrefix##2\endUpdate
\fi}
\ifx\secprefix\relax % if \secprefix is empty
\else
\expandafter\updatePrefix\secprefix\relax\endUpdate
\fi
}
\def\thesection{\secprefix\the\section.}
\def\stepSec{\global\advance\section by1}
\def\downOne{
\pushSection
\global\section=0
}
\def\upOne{
\popSection
}
\newcount\secIter \secIter=0
% \up ascends back to one of the parent sections, ascending #1 levels
\def\up#1{ % #1 is a negative integer
\ifnum\sectionDepth>0%
\secIter=#1%
\multiply\secIter by-1
% but \sectionDepth is a non-negative integer, so transform it
\ifnum\secIter>\sectionDepth%
\global\secIter=\sectionDepth
\fi%
\loop
\ifnum\secIter>0
\upOne
\advance\secIter by-1
\repeat%
\fi%
}
% down appends #1 subsections to the given section number
\def\down#1{ % #1 is a positive integer
\global\secIter=#1%
\loop
\ifnum\secIter>0
\downOne
\advance\secIter by-1
\repeat%
}
% move up or down #1 layers, does nothing if #1 is zero
\def\adjustSection#1{\ifnum#1<0\up{#1}\else{\ifnum#1>0\down{#1}\fi}\fi}
% \M is used for unlabeled paragraphs
\def\Mlabel{\medbreak\noindent\ignorespaces%
{\bf\thesection\ignorespaces}\enspace\ignorespaces}
\def\Mnone{\stepSec\Mlabel}
\def\Mmany[#1]{\adjustSection{#1}\Mnone}
\def\xM{\ifx\tmp[\expandafter\Mmany\else\Mnone\fi}
\def\M{\futurelet\tmp\xM}
% \N is used for labeled paragraphs
\def\Nlabel#1{\medbreak\noindent\ignorespaces%
{\bf\thesection\ignorespaces\enspace#1\ignorespaces}\enspace\ignorespaces}
\def\Nnone#1{\stepSec\Nlabel{#1}}
\def\Nmany[#1]#2{\adjustSection{#1}\Nnone{#2}}
\def\xN{\ifx\tmp[\expandafter\Nmany\else\Nnone\fi}
\def\N{\futurelet\tmp\xN}
\M
This is a test to see if this works.
\M I hope it works.
\M[1]
And this should be \S{2.1}, I hope.
\N[1]{Claim:} This should be \S{2.1.1}.
\M[-1]
This should be \S{2.2}.
\M[3]
This should be \S{2.2.0.0.1}, I hope?
\N[-3]{Theorem.}%
This is \S3, yes?
\M[-1]
No, this is \S3.
\bye
</pre>
<h1>Addendum: in LaTeX</h1>
<p>
It turns out to be a straightforward generalization to LaTeX:
</p>
<pre>
\documentclass{article}
\usepackage{fullpage}
\newcounter{chunk}
\def\setSection#1{\setcounter{chunk}{#1}}
\def\stepSec{\refstepcounter{chunk}}
% technically, sectionDepth is not needed, but it's to avoid popping off
% "too many sections"
\newcount\sectionDepth \sectionDepth=0
% \secprefix will be redefined to append the current section number
% followed by a period
\def\secprefix{}
\renewcommand\thechunk{\secprefix\arabic{chunk}.}
% \pushSection simply appends "\arabic{chunk}." to \secprefix's current value
\def\pushSection{
\global\advance\sectionDepth by1
\let\sectmp\secprefix
\xdef\secprefix{\sectmp\arabic{chunk}.}
}
% update \secprefix from "a.b.(...).c.d" to "a.b.(...).c"
% and set \chunk counter to "d" (as a number)
\def\popSection{
\def\newPrefix{}
\global\advance\sectionDepth by-1
\def\updatePrefix##1.##2\endUpdate{
\ifx\relax##2 % if we are at the last number
% globally set \secprefix to be the leading (n-1) section numbers
\xdef\secprefix{\newPrefix}
% globally set \chunk to be the last section number from \secprefix
\setSection{\number##1}
\else
\xdef\newPrefix{\newPrefix##1.}
\updatePrefix##2\endUpdate
\fi}
\ifx\secprefix\relax % if \secprefix is empty
\else
\expandafter\updatePrefix\secprefix\relax\endUpdate
\fi
}
\def\downOne{\pushSection\setSection{0}}
\def\upOne{\popSection}
\newcount\secIter \secIter=0
% \up ascends back to one of the parent sections, ascending #1 levels
\def\up#1{ % #1 is a negative integer
\ifnum\sectionDepth>0%
\secIter=#1%
% but \sectionDepth is a non-negative integer, so transform it
\multiply\secIter by-1
\ifnum\secIter>\sectionDepth%
\global\secIter=\sectionDepth
\fi%
\loop
\ifnum\secIter>0
\upOne
\advance\secIter by-1
\repeat%
\fi%
}
% down appends #1 subsections to the given section number
\def\down#1{ % #1 is a positive integer
\global\secIter=#1%
\loop
\ifnum\secIter>0
\downOne
\advance\secIter by-1
\repeat%
}
\def\adjustSection#1{\ifnum#1<0\up{#1}\else{\ifnum#1>0\down{#1}\fi}\fi}
%% \M is used for unlabeled paragraphs
\newcommand\M[1][0]{\adjustSection{#1}\medbreak%
\stepSec\noindent\ignorespaces%
\textbf{\thechunk\ignorespaces}\enspace\ignorespaces}
%% \N is used for labeled paragraphs
\newcommand\N[2][0]{\adjustSection{#1}\medbreak%
\stepSec\noindent\ignorespaces%
\textbf{\thechunk\ignorespaces\enspace#2\ignorespaces}\enspace\ignorespaces}
\begin{document}
\M
This is a test to see if this works.
\M I hope it works.
\M[1]
And this should be \S{2.1}, I hope.
\N[1]{Claim:} This should be \S{2.1.1}.
\M[-1]
This should be \S{2.2}.
\M[3]
This should be \S{2.2.0.0.1}, I hope?
\N[-3]{Theorem.}%
This is \S3, yes?
\M[-1]
No, this is \S3.
\M[0] This should be \S4.
\N[0]{Corollary.} This is \S5?
\end{document}
</pre>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-33679950464857135612021-11-24T15:00:00.002-08:002021-11-24T15:00:00.142-08:00Mathematical Language and Soft Type Systems<p>
<b>1.</b> After writing some <a href="https://texnicalstuff.blogspot.com/2021/11/the-next-generation-of-theorem-provers.html">thoughts about the next generation of provers</a>, I'd like to draw your attention to a couple papers:
</p>
<ol>
<li>F. Wiedijk, <br/>"Mizar's Soft Type System." <br/>In: K. Schneider & J. Brandt (eds.), <cite class="book">Theorem Proving in Higher Order Logics 2007</cite>, LNCS 4732, 383-399, 2007; <a href="http://cs.ru.nl/F.Wiedijk/mizar/miztype.pdf">pdf</a></li>
<li>Cezary Kaliszyk, Florian Rabe, <br/>"A Survey of Languages for Formalizing Mathematics". <br/><a href="https://arxiv.org/abs/2005.12876">arXiv:2005.12876</a>, 19 pages</li>
</ol>
<p>
I mention these papers as worth reading, for a couple reasons: first, they discuss an example of what a "higher level of abstraction" actually looks like; second, Kaliszyk and Rabe's paper complements Avigad's paper quite well.
</p>
<p>
<b>2. Definition.</b> Recall that type theory works by making typing judgements part of the metalanguage. A <dfn>Soft Type System</dfn> introduces typing judgements as propositions (and types as predicates) in the object language.
</p>
<p>
<b>2.1. Example.</b> For a concrete example of soft types in predicate logic, a dependent type with $n$ parameters is represented as an $n+1$-ary predicate $T(x, c_{1}, \dots, c_{n})$ interpreted as $x : T~c_{1}\dots c_{n}$. Subtyping is interpreted as $\forall x, S(x)\implies T(x)$ to assert $S$ is a subtype of $T$, and so on.
</p>
<p>
<b>2.2.</b> <i>Remark</i> (Soft Types in Type Theory)<b>.</b> This is not limited to "non-type theoretic foundations". For example <a href="https://corn.cs.ru.nl/">C-Corn</a> in Coq uses a version of a soft type system, as a means to increase the level of abstraction.
</p>
<p>
<b>2.3.</b> I bring this up because soft types increase the level of abstraction for formalizing mathematics. It's a non-obvious step, which approximates mathematical practice, and demonstrates the sort of "extensibility" I think the next generation of provers may need. Amazingly enough, it can encode the axiom of choice (see, e.g., <a href="http://alioth.uwb.edu.pl/~adamn/types2016_slides.pdf">slides</a> about <code>the [type]</code> usage in Mizar for encoding choice).
</p>
<p>
<b>3. Mathematical Language.</b> The only addendum I have to add from my last post is just a reference to Kaliszyk and Rabe's paper. It works in a "dual" manner to Avigad's paper, trying to think about a "pseudocode" for formalizing mathematics by surveying what different provers do.
</p>
<p>
The only qualm I have with their paper is precisely addressed by Avigad's paper: it's useful to give a lot of "small snippets" when trying to think about designing a language. Working in the abstract is, well, abstract. And hard.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-9445241768621408882021-11-23T20:00:00.002-08:002021-12-09T09:50:53.760-08:00The Next Generation of Theorem Provers<p>
<b>1. A parable.</b>
Back in the 1980s and '90s, there was a Cambrian explosion of CPU architectures: <a href="https://en.wikipedia.org/wiki/SPARC">SPARC</a>, <a href="https://en.wikipedia.org/wiki/IBM_POWER_microprocessors">POWER</a>, <a href="https://en.wikipedia.org/wiki/PA-RISC">PA-RISC</a>, <a href="https://en.wikipedia.org/wiki/MIPS_architecture">MIPS</a>, and presumably many others. Each processor architecture had its own customized UNIX-like operating system (SPARC had Solaris <i>née</i> <a href="https://en.wikipedia.org/wiki/SunOS">SunOS</a>, POWER had <a href="https://en.wikipedia.org/wiki/IBM_AIX">AIX</a>, PA-RISC had <a href="https://en.wikipedia.org/wiki/HP-UX">HP-UX</a>, MIPS had <a href="https://en.wikipedia.org/wiki/IRIX">IRIX</a>, etc.).
</p>
<p>
If you wrote a program and compiled it for one architecture, but I worked on a computer with a different architecture, then you couldn't share your program with me: you had to send me your source code, and hopefully I had a compiler for the language you used, then I could compile your program for my computer.
</p>
<p>
Of course, this was a nuisance. Some compilers had special features which hindered porting programs. Thus motivated the <a href="https://en.wikipedia.org/wiki/Java_(programming_language)">Java programming language</a> with the motto, <a href="https://en.wikipedia.org/wiki/Write_once,_run_anywhere">"Write once, run anywhere"</a>.
</p>
<p>
<b>2. Theorem Provers.</b> The situation with theorem provers reminds me of the situation with competing CPU architectures in the '80s and '90s. If you wrote a proof in Lean (or Coq or HOL or...), and I work with Coq (or HOL or anything else), then I can't verify your proof in my system. Worse: I can't even "compile it" to my theorem prover. <em>I would have to rewrite it from scratch.</em>
</p>
<p>
<b>2.1. Terminology.</b> I'm going to generically refer to proof checkers, interactive theorem provers, and automatic theorem provers under the umbrella term <dfn>Prover</dfn>. This is non-standard, but the field is so small that <em>any choice would be non-standard.</em>
</p>
<p>
<b>3. "Generations" of Provers.</b> For the sake of clarity, I think it's useful to introduce a notion of "Generations of Provers", analogous to <a href="https://en.wikipedia.org/wiki/Programming_language_generations">generations of programming languages</a>.
</p>
<p>
"First generation provers" include: Automath, Metamath, possibly Twelf, and others lacking automation (or auto-generation of infrastructure, like inductive types which [when defined] introduce an induction principle). First generation provers require <b>you</b> do this manually.
</p>
<p>
"Second generation provers" range from LCF to HOL, Coq, and Lean (and, I would argue, Mizar). There is some degree of automation, the proof assistant does some of the heavy lifting for you, but you may be required to explicitly state some proof steps.
</p>
<p>
And that's where we are today: after about 70 years, we've got two "generations" of provers. (This isn't too bad, considering how few people have worked on theorem provers and proof assistants.) We emphasize that "generation" is used metaphorically for the "level of <a href="https://en.wikipedia.org/wiki/Abstraction_(computer_science)">abstraction</a>" afforded by the prover.
</p>
<p>
<b>4. Hitting a moving target.</b> Unlike the situation facing CPU architects or programming language designers, we who think about theorem provers are trying to formalize an evolving language (mathematics).
</p>
<p>
We could berate mathematicians for not using theorem provers. But then we have our "tower of Babel" problem, where your prover can't talk to mine. (<del>Fanatics</del> Evangelists resolve this problem by insisting on using their "one true Prover", but that's unrealistic and unmerited.)
</p>
<p>
A better alternative would be to try to come up with the "next generation" of provers. This is easy to say, hard to accomplish. And mathematicians would just say, "Well, can't we make it like LaTeX with custom macros for proving results?" Again: easier said than done.
</p>
<p>
Designing a language is very hard, even with simple requirements. But a step towards the next generation would be (I believe <a href="http://www.cs.ru.nl/F.Wiedijk/">Freek Wiedijk</a> pointed this out in some article) analogous to how compilers "eat in" a high level language, process it, and then "spit out" assembly. What's the "assembly language" of mathematics? Some first generation prover, like Metamath or Automath.
</p>
<p>
<b>5. Designing a mathematical language.</b> The way we have learned to design a programming language (from many years of trial and error): write many small programs in the proposed language, and in comments specify the intended outcome. This strategy applies to provers, as well: write down many examples of mathematics [definitions, theorems, proofs or proof sketches] in the hypothetical prover's vernacular, and comment on what it should be doing.
</p>
<p>
There is much freedom when designing a new prover's vernacular, and it's easy to "cheat". Simply say, "...and somehow the prover will magically do the following: ...".
</p>
<p>
Perhaps we can turn this on its head, and begin thinking about how to do mathematics as a <a href="https://en.wikipedia.org/wiki/Controlled_natural_language">controlled natural language</a>? This is how I stumbled into theorem proving, running across Freek Wiedijk's note <a href="http://www.cs.ru.nl/F.Wiedijk/notes/mv.pdf">"The Mathematical Vernacular"</a>.
</p>
<p>
<b>6. Semiformal mathematics: controlling the vernacular.</b>
I just started jotting these ideas down when I came across Jeremy Avigad's interesting recent paper, <a href="http://philsci-archive.pitt.edu/19508/">"The design of mathematical language"</a>. Although I agree with much of the paper, and I especially praise the use of "many small examples from mathematical literature" to guide the discussion, I thought it was limited in exploring the "design space" and eager to accept Lean's design decisions.
</p>
<p>
For example, consider the definition of a "normal subgroup". Are we defining an adjective ("normal") or a type modifier (since "subgroup" is a type, a "normal subgroup" would be a subtype of "subgroup") or a new type with implicit coercions (any "normal subgroup" is automatically a "subgroup", and satisfy the properties that a subgroup would have)?
</p>
<p>
Another undiscussed dimension to mathematical definitions (as a <a href="https://en.wikipedia.org/wiki/Domain-specific_language">domain specific language</a>) would be examining the <a href="https://texnicalstuff.blogspot.com/2009/08/object-oriented-math-category-theory-as.html">"stuff, structure, and properties"</a> idea of Baez and Dolan. This template gives us a lot "for free", and can be made somewhat "independent of foundations" by using objects in toposes. It's a small thing, but seldom discussed among provers.
</p>
<p>
The discussion also lacked adequate examples from applied mathematics (which, for me, would be things like weak solutions to PDEs, or theorems about regularity of PDEs, or something like that...my mind is focused on the Navier-Stokes equations). Granted, this <em>is</em> a domain where many mathematicians flinch and say, "Ouch, this is an unpleasant field." I do not intend it as a criticism, but an observation.
</p>
<p>
<b>6.1. Analysis, Synthesis.</b> The next natural step in Avigad's paper would be to move from <em>analyzing examples</em> to <em>synthesizing</em> some semi-formal "vernacular".
</p>
<p>
I honestly don't have a "semi-formal vernacular" at hand to present, but I have been using something similar to Wiedijk's vernacular for the past year. Since April or so of 2021, I have been transcribing my notes into a Zettelkasten (i.e., onto A6 size slips of paper). Proofs and proof sketches have been written using a slight variant of Wiedijk's vernacular.
</p>
<p>
It works fine for proofs, and forces me to fill in missing steps (or at least, make note of them). But I think proofs as a domain-specific language don't require much thought: we've had very smart people think about it for a century, and they came up with pretty good ideas (natural deduction, judgements, etc.). Now my task boils down to coming up with the right "reserved keywords" corresponding to the proof steps found in mathematical logic.
</p>
<p>
For definitions, in Field theory and Galois theory, most definitions don't neatly fit the "stuff, structure, properties" mould. This is great! Now I have some ready-to-present examples where it fails, namely whenever a definition looks like: "We call a gadget $G$ <dfn>Hairy</dfn> if [hairy property] holds." This occurs a lot in field theory and Galois theory. It also forces me to think deeply about what "species" of definition this is, and what's "really being defined" here.
</p>
<p>
<b>6.2. Future of Provers?</b> The short answer is, I don't know. The next steps may be to think about the "next generation" of provers, and try to move towards a "foundation independent framework" which resembles how working mathematicians actually operate.
</p>
<p>
But I think it's wrong-headed to say, as Leslie Lamport put it, mathematicians are "doing proofs wrong" because it resembles Euclid (and Euclid is old, thus bad). It's probably equally as misguided as suggesting that the design of the input language for provers is irrelevant, as any compiler designer will tell you, since this alienates the user-base and hinders adoptation.
</p>
<p>
Taken together, this suggests we need to make provers resemble "ordinary mathematics" as published and practiced by working mathematicians. Thus investigations along the lines of Avigad's article is well worth pursuing.
</p>
<p>
My intuition tells me that the third or fourth generation of Provers will resemble compilers, accepting more human intelligible input, producing "assembly code"-like output for a particular foundations of mathematics. Changing foundations would be a "one liner", if that. <em>But what does the input language look like?</em> That's hard to say.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-7157398372287186042021-11-23T19:00:00.001-08:002021-11-23T19:00:00.154-08:00Group Morphisms<section>
<p>
<b>1.</b> There is some "Kabuki theater" whenever introducing a new mathematical gadget, thanks to <a href="https://texnicalstuff.blogspot.com/2009/08/object-oriented-math-category-theory-as.html">category theory</a>: we have our new gadget, then we could ask about morphisms (very important), "subgadgets", and universal constructions (products, quotients, etc.). The exciting thing, as in Kabuki theater, is the order and manner of presentation. </p>
<p>
</section>
<section class="proposition Definition">
<p>
<span class="number">2.</span> <span class="label">Definition.</span> Let ${G}$ and ${H}$ be groups. We define a <dfn>Group Morphism</dfn> to consist of a function ${\varphi\colon G\to H}$ of the underlying sets such that
<ol>
<li> group operation is preserved: for any ${g_{1}}$, ${g_{2}\in G}$, we have ${\varphi(g_{1}g_{2})=\varphi(g_{1})\varphi(g_{2})}$; </li>
<li> identity element is preserved: if ${e_{G}\in G}$ is the identity element of ${G}$ and ${e_{H}\in H}$ is the identity element of ${H}$, then ${\varphi(e_{G})=e_{H}}$; </li>
<li> inverse is preserved: for any ${g\in G}$, ${\varphi(g^{-1})=\varphi(g)^{-1}}$. </li>
</ol>
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">2.1.</span> <span class="label">Remark.</span> Older texts refer to group morphisms as "group <em>homomorphisms</em>". After category theory became popular and part of the standard curriculum, the "homo-" prefix was dropped because group morphisms live in the same category, so it was redundant.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">3.</span> <span class="label">Example.</span> One "low hanging fruit" for morphism examples is the identity morphism. We should check, for any group ${G}$, the identity function ${\mathrm{id}\colon G\to G}$ is a <em>bona fide</em> group morphism. </p>
<p>
We see it preserves the group operation. For any ${g_{1}}$, ${g_{2}\in G}$, we have ${\mathrm{id}(g_{1}g_{2})=g_{1}g_{2}}$ by definition of the identity function. But this is also equal to ${\mathrm{id}(g_{1})\mathrm{id}(g_{2})}$. Thus the group operation is preserved. </p>
<p>
The identity element is preserved ${\mathrm{id}(e_{G})=e_{G}}$. </p>
<p>
Inversion is also preserved ${\mathrm{id}(g^{-1})=g^{-1}=\mathrm{id}(g)^{-1}}$ for any ${g\in G}$. </p>
<p>
Thus taken together, it follows the identity mapping satisfies the axioms of a group morphism.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">4.</span> <span class="label">Example.</span> Let ${G}$ be any group, and consider ${\mathbb{Z}}$ equipped with addition as a group. For each ${g\in G}$, we have a group morphism ${\varphi\colon\mathbb{Z}\to G}$ sending ${1\in\mathbb{Z}}$ to ${g\in G}$. Is this <em>really</em> a group morphism? </p>
<p>
We can check that the properties are (or, ought to be) satisfied. If the group operation is preserved, then ${\varphi(1+1)=\varphi(1)\varphi(1)=g^{2}}$ and more generally, for any ${m\in\mathbb{Z}}$, we have ${\varphi(m+1)=\varphi(1)^{m}=g^{m}}$. </p>
<p>
For the identity element being preserved, that means ${\varphi(0)=e_{G}}$, which is fine: it corresponds to ${g^{0}=e_{G}}$. </p>
<p>
Group inverses would be ${\varphi(-m)=\varphi(m)^{-1}=(g^{m})^{-1}}$. And we know this is precisely the same as ${g^{-m}}$.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">5.</span> <span class="label">Example.</span> Consider the group ${\mathrm{GL}(2,\mathbb{R})}$ and the multiplicative group ${\mathbb{R}^{\times}}$ of nonzero real numbers. Then the determinant
$$ \det\colon\mathrm{GL}(2,\mathbb{R})\to\mathbb{R}^{\times} \tag{1}$$
is a group morphism. Let us prove it! </p>
<p>
We see, for any matrices ${M}$, ${N\in\mathrm{GL}(2,\mathbb{R})}$ we have
$$ \det(MN)=\det(M)\det(N). \tag{2}$$
This is a familiar fact in linear algebra. But for us, it tells us the group operation is preserved. </p>
<p>
The identity element must be mapped to the identity element. We see the identity matrix ${I\in\mathrm{GL}(2,\mathbb{R})}$ has ${\det(I)=1}$. Thus the determinant preserves the group identity element. </p>
<p>
As far as the group inverse, well, this follows from previous results, right? After all, if ${M\in\mathrm{GL}(2,\mathbb{R})}$, then ${M^{-1}\in\mathrm{GL}(2,\mathbb{R})}$, and
$$ I = M^{-1}M \tag{3}$$
so
$$ \det(M^{-1}M)=\det(M^{-1})\det(M)=1 \tag{4}$$
and thus by division
$$ \det(M^{-1})=\det(M)^{-1}. \tag{5}$$
Thus the group inverse operator is preserved.
</p>
</section>
<section class="proposition Definition">
<p>
<span class="number">6.</span> <span class="label">Definition.</span> Let ${\varphi\colon G\to H}$ be a group morphism. We define the <dfn>Kernel</dfn> of ${\varphi}$ to be the pre-image of the identity element of ${H}$: \begin{equation*} \ker(\varphi)=\{g\in G|\varphi(g)=e_{H}\}. \end{equation*}
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">7.</span> <span class="label">Example.</span> For the group morphism ${\det\colon\mathrm{GL}(2,\mathbb{R})\to\mathbb{R}^{\times}}$, the kernel would be
$$ \ker(\det)=\{M\in\mathrm{GL}(2,\mathbb{R})|\det(M)=1\}. \tag{6}$$
That is to say, it consists of matrices with unit determinant. Observe, this is a group under matrix multiplication: if two matrices have unit determinant, their product has unit determinant; the identity matrix is in the kernel; and it's closed under inverses. This is an important group called the <dfn>Special Linear Group</dfn>, denoted ${\mathrm{SL}(2,\mathbb{R})}$.
</p>
</section>
<h1>1. Properties of Morphisms</h1>
</p><section class="proposition Proposition">
<p>
<span class="number">8.</span> <span class="label">Proposition.</span> <em> Let ${\varphi\colon G\to H}$ be a group morphism. If ${g\in G}$ is any element, then ${\varphi(g^{-1})=\varphi(g)^{-1}}$. </em>
</p>
</section>
<section class="proof"><p>
<em>Proof:</em> Let ${g\in G}$ (so ${\varphi(g)\in H}$). We find ${\varphi(g\cdot g^{-1})=\varphi(g)\varphi(g^{-1})=e_{H}}$, thus multiplying on the left by ${\varphi(g)^{-1}}$ gives the result. ∎
</p>
</section>
<section class="proposition Proposition">
<p>
<span class="number">9.</span> <span class="label">Proposition.</span> <em> Let ${\varphi\colon G\to H}$ be a group morphism. If ${g\in G}$ is any element and ${n\in\mathbb{Z}}$ is any integer, then ${\varphi(g^{n})=\varphi(g)^{n}}$. </em>
</p>
</section>
<section class="proof">
<em>Proof:</em> Per cases since ${n<0}$ or ${n=0}$ or ${n>0}$. The ${n=0}$ case is obvious. </p>
<p>
For ${n>0}$, by induction. The base case ${n=1}$ gives ${\varphi(g^{1})=\varphi(g)^{1}}$, which is obvious. Assume this holds for arbitrary ${n}$. Then the inductive case ${n+1}$ is
$$ \varphi(g^{n+1})=\varphi(g^{n}g)=\varphi(g)^{n}\varphi(g)=\varphi(g)^{n+1}. \tag{7}$$
Thus we have proven the result for non-negative ${n}$. </p>
<p>
For negative ${n\in\mathbb{Z}}$, the proof is analogous. ∎
</p>
</section>
<section class="proposition Theorem">
<p>
<span class="number">10.</span> <span class="label">Theorem.</span> <em> The composition of group morphisms is a group morphism. More explicitly, if ${\varphi\colon G\to H}$ and ${\psi\colon H\to K}$ are group morphisms, then ${\psi\circ\varphi\colon G\to K}$ is a group morphism. </em>
</p>
</section>
<section class="proposition Theorem">
<p>
<span class="number">11.</span> <span class="label">Theorem.</span> <em> Let ${\varphi\colon G\to H}$ be a group morphism. If ${\ker(\varphi)=\{e_{G}\}}$, then ${\varphi}$ is injective. </em>
</p>
</section>
<section class="proof">
<p>
<em>Proof:</em> Assume ${\ker(\varphi)=\{e_{G}\}}$. Let ${g_{1}}$, ${g_{2}\in G}$ be completely arbitrary. (We want to show if ${\varphi(g_{1})=\varphi(g_{2})}$, then ${g_{1}=g_{2}}$.) Assume ${\varphi(g_{1})=\varphi(g_{2})}$. Then ${\varphi(g_{1})\varphi(g_{2})^{-1}=e_{H}}$ by multiplying both sides on the right by ${\varphi(g_{2})^{-1}}$. And ${\varphi(g_{1})\varphi(g_{2}^{-1})=\varphi(g_{1}\cdot g_{2}^{-1})=e_{H}}$. Thus ${g_{1}\cdot g_{2}^{-1}\in\ker(\varphi)}$ by definition of the kernel. But we assumed the only member of the kernel was identity element. Thus ${g_{1}\cdot g_{2}^{-1}=e_{G}}$, and moreover ${g_{1}=g_{2}}$. Hence ${\varphi}$ is injective. ∎
</p>
</section>
<h1>2. Exercises</h1>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">1.</span> Let ${G}$ be a group, ${n\in\mathbb{N}}$ be a fixed positive integer. Prove or find a counter-example: ${\varphi\colon G\to G}$, sending ${g}$ to ${\varphi(g)=g^{n}}$ is a group morphism.
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">2.</span> Prove or find a counter-example: the matrix trace ${\mathop{\rm tr}\nolimits\colon\mathrm{GL}(2,\mathbb{R})\to\mathbb{R}}$ is a group morphism.
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">3.</span> Is the exponential function on the real numbers a group morphism ${\exp\colon\mathbb{R}\to\mathbb{R}^{\times}}$?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise</span> <span class="number">4.</span> Is the matrix exponential a group morphism ${\exp\colon\mathrm{Mat}_{2}(\mathbb{R})\to\mathrm{GL}(2,\mathbb{R})}$? [Hint: $\mathrm{Mat}_{2}(\mathbb{R})$ has its group operation be matrix addition. Is this preserved?]
</p>
</section>
pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com1tag:blogger.com,1999:blog-3776650590176552530.post-14884665374127071892021-11-15T16:00:00.002-08:002021-11-17T08:19:59.225-08:00Typography of Lie groups, Lie algebras<p>
This is a note for myself as I review my notes on finite groups, Lie groups (both the classic infinite ones and the finite simple groups of Lie type), Lie algebras, and specifically the typography for them.
</p>
<p>
First, no one agrees completely, and everyone's conventions is slightly different. What I mean by this: although everyone agrees, e.g., that the A<sub><var>n</var></sub> family of Lie algebras refers to the same thing, some people use serif font for the "A", others use bold, some italicize, others do not, etc. Each field uses its own notation with good reason, but I think we can standardize notation a bit better in group theory.
</p>
<p>
I'm inclined to follow Robert Wilson's conventions from his book <cite class="book">The Finite Simple Groups</cite> (2009).
</p>
<h2>Families of Groups</h2>
<p>
<b>Families of Simple Lie groups:</b> use upright, teletype font for the family and "math italics" for the subscript if it's a variable, e.g., $\mathtt{A}_{n}$, $\mathtt{B}_{5}$, $\mathtt{C}_{m}$, $\mathtt{D}_{n^{2}}$, $\mathtt{E}_{8}$
</p>
<p>
<b>Exceptional Finite Simple Groups of Lie Type:</b> don't treat the formatting as special, so, e.g., the Steinberg groups would be ${}^{2}A_{n}(q^{2})$, ${}^{2}D_{n}(q^{2})$, ${}^{2}E_{6}(q^{2})$, ${}^{3}D_{4}(q^{3})$.
</p>
<p>
<b>Sporadic simple group:</b> these should be made upright, e.g., the Suzuki group is $\mathrm{Suz}$, the Matthieu groups look like $\mathrm{M}_{11}$, the Conway groups $\mathrm{Co}_{1}$ and $\mathrm{Co}_{2}$, and so on. <b>BUT</b> the exception to this rule is that the Monster group is written $\mathbb{M}$ and the Baby Monster $\mathbb{B}$.
</p>
<p>
<b>Alternating, Cyclic, Symmetric group.</b> These are just written as $A_{n}$, $C_{n}$, or $S_{n}$. The dihedral group, too, is $D_{n}$.
</p>
<p>
<b>Classical Lie Groups:</b> Here there is a double standard. For classical Lie groups over the reals or complex numbers, we write something of the form $\mathrm{GL}(n, \mathbb{F})$, $\mathrm{SL}(n, \mathbb{F})$, $\mathrm{U}(n, \mathbb{F})$, $\mathrm{SU}(n, \mathbb{F})$, $\mathrm{O}(n, \mathbb{F})$, $\mathrm{SO}(n, \mathbb{F})$, $\mathrm{Sp}(n)=\mathrm{USp}(n)$ for the compact Symplectic group, $\mathrm{Sp}(2n,\mathbb{F})$ for the generic Symplectic group.
</p>
<p>
The finite groups corresponding to these guys are written a little differently in my notes: the $n$ parameter is pulled out as a subscript, because frequently we write $q$ instead of $\mathbb{F}_{q}$ for finite fields...and then looking at $\mathrm{SL}(8,9)$ is far more confusing than $\mathrm{SL}_{8}(9)$. Thus we have $\mathrm{GL}_{n}(q)$, and so on.
</p>
<p>
<b>Projective classical groups:</b> the projective classical groups are prefixed by a "P", not a blackboard bold $\mathbb{P}$. E.g., $\mathrm{PSL}_{2}(7)$. At present, the <a href="https://en.wikipedia.org/w/index.php?title=Projective_orthogonal_group&oldid=1034230012">projective orthogonal group</a> wikipedia page seems to agree with this convention.
</p>
<h2>Operations</h2>
<p>
<b>For finite groups:</b> the Atlas of finite groups seems to have set the standard conventions for finite groups, Wilson changes them slightly. We'll find $G = N{:}H$ for the semidirect product $G = N \rtimes H = H\ltimes N$. Also $A\mathop{{}^{\textstyle .}}\nolimits B = A{\,}^{\textstyle .} B$ for a non-split extension with quotient $B$ and normal subgroup $A$, but no subgroup $B$. And $A{.}B$ is an unspecified extension.
</p>
<aside>
<p>
Just a quick remark concerning $A^{\textstyle{.}}B$, I was unsatisfied with this, and <a href="https://tex.stackexchange.com/q/622639/14751">asked TeX.stackexchange</a> for help. The answers were fantastic! I'll quote the two solutions submitted:
</p>
<pre>
<b>% solution one</b>
\makeatletter
\newcommand*{\udot}{{\mathpalette\ud@t\relax}} % or \mathrel/\mathbin/etc?
\newcommand*{\ud@t}[2]{%
\sbox\z@{\m@th$#1.$}%
\sbox\tw@{$#1:$}%
\raise\dimexpr\ht\tw@-\ht\z@\relax\box\z@
}
% Example usage:
%
% $A . A {:} A \udot A$\par
% $\scriptstyle A . A {:} A \udot A$\par
% $\scriptscriptstyle A . A {:} A \udot A$
\makeatother
<b>% solution two</b>
\makeatletter
\newcommand{\udot}{\mathpalette\udot@\relax}
\newcommand{\udot@}[2]{%
\begingroup
\sbox\z@{$#1{:}$}%
\sbox\tw@{$#1{.}$}%
\raisebox{\dimexpr\ht\z@-\ht\tw@}{$\m@th#1.$}%
\endgroup
}
\makeatother
\newcommand{\genericextension}[1]{%
\mathbin{%
\nonscript\mkern-0.75\medmuskip
{#1}%
\nonscript\mkern-0.75\medmuskip
}%
}
\DeclareRobustCommand{\gext}{\genericextension{.}}
\DeclareRobustCommand{\sdp}{\genericextension{:}}
\DeclareRobustCommand{\nsext}{\genericextension{\udot}}
% Example usage:
%
% $A\gext B$ is a group extension
%
% $A\sdp B$ is a semidirect product
%
% $A\nsext B$ is a nonsplit group extension
%
% ${:}{\udot}$ for checking the alignment
%
% $X_{A\gext B} \quad X_{A\sdp B} \quad X_{A\nsext B}$
</pre>
</aside>
<p>
<b>Lie algebras.</b> Writing notes on paper, for a given Lie group $G$, I write $\mathrm{Lie}(G)$ as its Lie algebra. (It turns out to be a functor...neat!) If I have to write Fraktur by hand, I approximate it using <a href="https://loopspace.mathforge.org/CountingOnMyFingers/Calligraphy/">Pappus's caligraphy tutorial</a>.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-87560556542302591072021-11-12T00:00:00.008-08:002021-11-12T06:52:02.973-08:00Charts and Atlases, Manifolds and Smooth Structures
<h1>1. Manifolds</h1>
<p>
We will introduce the machinery necessary for defining a smooth manifold.
</p>
<h2>1.1. Charts</h2>
<section class="proposition Definition">
<p>
<span class="number">1.</span> <span class="label">Definition.</span> Let ${X\subset M}$ be some set. An ${n}$-dimensional <dfn>Chart</dfn> consists of
<ol>
<li> an open subset ${U\subset\mathbb{R}^{n}}$ </li>
<li> a map ${\varphi\colon U\to X}$ </li>
</ol>
such that ${\varphi}$ is an appropriate isomorphism (for topological manifolds, it is a homeomorphism; smooth manifolds require a diffeomorphism; and so on).
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">2.</span> <span class="label">Remark.</span> We call ${\varphi\colon U\to X}$ a <dfn>Parametrization</dfn> of ${X}$, and ${\varphi^{-1}\colon X\to U}$ a <dfn>Local System of Coordinates</dfn>.
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">3.</span> <span class="label">Remark.</span> Since ${\varphi}$ is an isomorphism, the literature mixes up using ${U\to X}$ and ${X\to U}$. Milner uses ${\varphi\colon U\to X}$, but John Lee uses the opposite convention.
</p>
</section>
<section class="proposition Definition">
<p>
<span class="number">4.</span> <span class="label">Definition.</span> Let ${(U,\varphi)}$, ${(V,\psi)}$ be two charts. We say they are <dfn>Compatible</dfn> if
</p>
<ol>
<li> the set ${(\varphi^{-1}\circ\psi)(V)\subset U}$ is an open set; </li>
<li> the set ${(\psi^{-1}\circ\varphi)(U)\subset V}$ is an open set; </li>
<li> the map ${\psi^{-1}\circ\varphi\colon\varphi^{-1}(\psi(V))\to\psi^{-1}(\varphi(U))}$ is smooth; and </li>
<li> the map ${\varphi^{-1}\circ\psi\colon\psi^{-1}(\varphi(U))\to\varphi^{-1}(\psi(V))}$ is smooth. </li>
</ol>
<p>
In particular, the charts are compatible if ${\varphi(U)\cap\psi(V)=\emptyset}$ is disjoint.
</p>
</section>
<div class="separator" style="clear: both;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEg-G7aWGG8zHYP3-E_e-kUb5mxekKwwRjcykcnOyQyt1eGHTLoSfMBdr6T-UIGxQfglDav3P6_sx0Qmg1wM3YFVgdWQN4qIbNrtnb3ID5Z-bPs-6y1E2ciuM1ux7e4ThZvZy3W_OOcTEcA/s0/img-0.png" style="display: block; padding: 1em 0; text-align: center; "><img alt="" border="0" data-original-height="321" data-original-width="491" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEg-G7aWGG8zHYP3-E_e-kUb5mxekKwwRjcykcnOyQyt1eGHTLoSfMBdr6T-UIGxQfglDav3P6_sx0Qmg1wM3YFVgdWQN4qIbNrtnb3ID5Z-bPs-6y1E2ciuM1ux7e4ThZvZy3W_OOcTEcA/s0/img-0.png"/></a></div>
<section class="proposition Remark">
<p>
<span class="number">5.</span> <span class="label">Remark.</span> We refer to the maps ${\psi^{-1}\circ\varphi}$ as <dfn>Transition Functions</dfn>. The condition of smooth is ${C^{\infty}(\mathbb{R}^{n})}$, but different manifolds have different conditions (we could have ${C^{k}}$ charts, or ${C^{0}}$ charts, or analytic ${C^{\omega}}$ charts, or...). </p>
<p>
In the older literature (e.g., Kobayashi and Nomizu's <em>Foundations of Differential Geometry</em>), the collection of transition functions form a gadget called a <dfn>Pseudogroup</dfn>.
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">6.</span> <span class="label">Remark.</span> We abuse notation, and could be more explicit by writing
$$ \psi^{-1}\circ\varphi\colon\varphi^{-1}(\varphi(U)\cap\psi(V))\to\psi^{-1}(\varphi(U)\cap\psi(V)) \tag{1}$$
</p>
</section>
<section class="proposition Exercise">
<p>
▸ <span class="label">Exercise</span> <span class="number">1.</span> Prove chart compatibility is an equivalence relation.
</p>
</section>
<h2>1.2. Atlases</h2>
<section class="proposition Definition">
<span class="number">7.</span> <span class="label">Definition.</span> Let ${M}$ be a set. An (${n}$-dimensional) <dfn>Atlas</dfn> consists of a collection ${\{(U_{\alpha},\varphi_{\alpha})\mid\alpha\in A\}}$ of ${n}$-dimensional charts on ${M}$ such that
<ol>
<li> Covers ${M}$: $\displaystyle{\bigcup_{\alpha\in A}\varphi_{\alpha}(U_{\alpha})=M}$ </li>
<li> Pairwise compatible: for any ${\alpha}$, ${\beta\in A}$ the charts ${(U_{\alpha},\varphi_{\alpha})}$ and ${(U_{\beta},\varphi_{\beta})}$ are compatible. </li>
</ol>
</section>
<section class="proposition Definition">
<p>
<span class="number">8.</span> <span class="label">Definition.</span> Two ${n}$-dimensional atlases on ${M}$, ${\mathcal{A}}$ and ${\mathcal{B}}$, are called <dfn>Equivalent</dfn> if their union ${\mathcal{A}\cup\mathcal{B}}$ is also an atlas. That is to say, if any chart of ${\mathcal{A}}$ is compatible with any chart of ${\mathcal{B}}$.
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">9.</span> <span class="label">Remark.</span> Remember: charts are <em>compatible</em>, but atlases are <em>equivalent</em>.
</p>
</section>
<section class="proposition Lemma">
<p>
<span class="number">10.</span> <span class="label">Lemma.</span> <em><a name="lemma002-diff-geomtransitivity-of-atlas-equivalence"></a> Let ${\mathcal{B}}$ be an atlas, let ${(U,\varphi)}$ and ${(V,\psi)}$ be two charts not contained in ${\mathcal{B}}$. If ${(U,\varphi)}$ is compatible with every chart of ${\mathcal{B}}$, and if ${(V,\psi)}$ is compatible with every chart of ${\mathcal{B}}$, then ${(U,\varphi)}$ is compatible with ${(V,\psi)}$. </em>
</p>
</section>
<section class="proposition Theorem">
<p>
<span class="number">11.</span> <span class="label">Theorem.</span> <em> Equivalence of atlases is an equivalence relation. </em>
</p>
</section>
<section class="proof">
<p>
<em>Proof:</em> Let ${\mathcal{A}}$, ${\mathcal{B}}$, ${\mathcal{C}}$ be arbitrary atlases on ${M}$.
</p>
<ol>
<li> Reflexivity: ${\mathcal{A}}$ is equivalent to itself, since by definition any pair of charts in ${\mathcal{A}}$ are compatible. </li>
<li> Symmetry: let ${\mathcal{A}}$ and ${\mathcal{B}}$ be equivalent atlases, then ${\mathcal{B}}$ and ${\mathcal{A}}$ are equivalent atlases. </li>
<li> Transitivity: this is the nontrivial part. Let ${\mathcal{A}}$ and ${\mathcal{B}}$ be equivalent atlases, and ${\mathcal{B}}$ be equivalent to ${\mathcal{C}}$. Then transitivity follows by considering arbitrary charts ${(U,\varphi)\in\mathcal{A}}$ and ${(V,\psi)\in\mathcal{C}}$, then applying <a href="#lemma002-diff-geomtransitivity-of-atlas-equivalence">Lemma 10</a>. </li>
</ol>
<p>
Thus "equivalence of atlases" forms an equivalence relation. ∎
</p>
</section>
<section class="proposition Proposition">
<p>
<span class="number">12.</span> <span class="label">Proposition.</span> <em> The collection of atlases on a given set ${M}$ is a <em>set</em>, not a proper class. </em>
</p>
</section>
<section class="proof">
<p>
<em>Proof:</em> The class of atlases is a subcollection of
$$ \mathcal{X}=\mathcal{P}\left(\bigcup_{U\in\mathcal{P}(\mathbb{R}^{n})}\mathop{\rm Hom}\nolimits(U,M)\right) \tag{2}$$
where ${\mathop{\rm Hom}\nolimits(U,\mathbb{R}^{n})}$ is the collection of (appropriately smooth, or continuous, or holomorphic, or...) functions from ${U}$ to ${M}$. By ZF axioms, ${\mathcal{X}}$ is a set. ∎
</p>
</section>
<h2>1.3. Manifolds</h2>
<section class="proposition Definition">
<p>
<span class="number">13.</span> <span class="label">Definition.</span> Let ${M}$ be a set, let ${\mathcal{A}}$ be an ${n}$-dimensional atlas on ${M}$. We call a subset ${B\subset M}$ <dfn>Open</dfn> (with respect to ${\mathcal{A}}$) if for any chart ${(U,\varphi)\in\mathcal{A}}$ the preimage ${\varphi^{-1}(B)}$ is open (in ${U}$, and thus open in ${\mathbb{R}^{n}}$). In particular, the images ${\varphi(U)}$ are open.
</p>
</section>
<section class="proposition Theorem">
<p>
<span class="number">14.</span> <span class="label">Theorem.</span> <em> If two atlases ${\mathcal{A}_{1}}$ and ${\mathcal{A}_{2}}$ on ${M}$ are equivalent, then a subset ${B\subset M}$ is open with respect to ${\mathcal{A}_{1}}$ if and only it is open with respect ${\mathcal{A}_{2}}$. </em>
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">15.</span> <span class="label">Remark.</span> This theorem shows an equivalence class of atlases on ${M}$ makes ${M}$ a topological space. We may therefore meaningfully speak about topological properties of ${M}$ (like compactness, connectedness, and so forth).
</p>
</section>
<section class="proposition Corollary">
<p>
<span class="number">16.</span> <span class="label">Corollary.</span> <em> Let ${\mathcal{A}}$ be an ${n}$-dimensional atlas for ${M}$. Then the collection of open sets with respect to ${\mathcal{A}}$ form a topology on ${M}$. </em>
</p>
</section>
<section class="proposition Definition">
<p>
<span class="number">17.</span> <span class="label">Definition.</span> Let ${M}$ be a fixed set. A <dfn>${n}$-Dimensional Differential Structure</dfn> (or <em>${n}$-Dimensional Smooth Structure</em>) on ${M}$ consists of an equivalence class ${\mathfrak{D}}$ of ${n}$-dimensional atlases on ${M}$ such that
<ol>
<li>Second-Countable: ${\mathfrak{D}}$ contains an at most countable atlas; </li>
<li>Hausdorff: for any distinct ${p,q\in M}$, there exists disjoint open neighborhoods ${U,V\subset M}$ such that ${p\in U}$ and ${q\in V}$. </li>
</ol>
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">18.</span> <span class="label">Remark (Smooth Structure using a Maximal Atlas).</span> Equivalence classes are awkward to work with, and so it is more popular to consider <em>maximal atlases</em>. An atlas ${\mathcal{A}}$ is maximal if it contains all charts compatible with every chart in ${\mathcal{A}}$. Given an equivalence class ${\mathfrak{A}}$ of atlases, we may obtain a maximal atlas by considering
$$ \mathcal{A}_{\text{max}} = \bigcup_{\mathcal{A}\in\mathfrak{A}}\mathcal{A}. \tag{3}$$
This may be used instead of an equivalence class of atlases in defining a differential structure, provided the second-countable axiom is reworded as: ${\mathcal{A}_{\text{max}}}$ contains an at most countable subatlas.
</p>
</section>
<section class="proposition Remark">
<p>
<span class="number">19.</span> <span class="label">Remark (Convenient Fiction).</span> No one actually constructs either a maximal atlas or a differential structure. We typically construct a smooth atlas on ${M}$, then announce we are working with the differential structure containing our atlas. Thus maximal atlases and, to some degree, differential structures are a convenient fiction.
</p>
</section>
<section class="proposition Definition">
<p>
<span class="number">20.</span> <span class="label">Definition.</span> A <dfn>(Smooth) ${n}$-Dimensional Manifold</dfn> consists of a set ${M}$ equipped with an ${n}$-dimensional differential structure.
</p>
</section>
<section class="proposition Puzzle">
<p>
<span class="number">21.</span> <span class="label">Puzzle.</span> Is this definition correct? By this, I mean: is an "${n}$-Dimensional Differential Structure" <em>actually</em> structure (in the sense of <a href="https://texnicalstuff.blogspot.com/2009/08/object-oriented-math-category-theory-as.html">"stuff, structure, and properties"</a>)?
</p>
</section>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-78088902823615683082021-11-08T12:30:00.002-08:002021-11-08T12:30:00.155-08:00Introducing Groups to Beginners<p>[This is an experiment to see if some software to translate LaTeX to html works.]</p>
<section>
<p>
<b>1. Introduction.</b> We will do some group theory. Here "group" refers to a "group of symmetry transformations", and we should think of elements of the group as functions mapping an object to itself in some particularly <em>symmetric</em> way. </p>
<p>
</section>
<section class="proposition Definition">
<p>
<span class="number">2.</span> <span class="label">Definition.</span> A <dfn>Group</dfn> consists of a set ${G}$ equipped with
<ol>
<li> a law of composition ${\circ\colon G\times G\to G}$, </li>
<li> an identity element ${e\in G}$, and </li>
<li> an inverse operator ${(-)^{-1}\colon G\to G}$ </li>
</ol>
such that
<ol>
<li> Associativity: For any ${g_{1}}$, ${g_{2}}$, ${g_{3}\in G}$, ${(g_{1}\circ g_{2})\circ g_{3}=g_{1}\circ(g_{2}\circ g_{3})}$ </li>
<li> Unit law: For any ${g\in G}$, ${g\circ e=e\circ g=g}$ </li>
<li> Inverse law: For any ${g\in G}$, ${g^{-1}\circ g=g\circ g^{-1}=e}$. </li>
</ol>
</p>
</section>
<section>
<p>
<b>3. Effective Thinking Principle: Create Examples.</b> Whenever encountering a new definition, it's useful to construct examples. Plus, it's fun. Now let us consider a bunch of examples! </p>
</section>
<section class="proposition Example">
<p>
<span class="number">4.</span> <span class="label">Example (Trivial).</span> One strategy is to find the most boring example possible. We can't use ${G=\emptyset}$ since a group must contain at least one element: the identity element ${e\in G}$. Thus the next most boring candidate is the group containing <em>only</em> the identity element ${G=\{e\}}$. This is the <dfn>Trivial Group</dfn>.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">5.</span> <span class="label">Example (Dihedral).</span> Consider the regular ${n}$-gon in the plane ${X\subset\mathbb{R}^{2}}$ with vertices located at ${(\cos(k2\pi/n), \sin(k2\pi/n))}$ for ${k=0,1,\dots,n-1}$. We also require ${n\geq3}$ to form a non-degenerate polygon (${n=2}$ is just a line segment, and ${n=1}$ is one dot). </p>
<p>
We can rotate the polygon by multiples of ${2\pi/n}$ radians. There are several ways to visualize this, I suppose we could consider rotations of the plane by ${2\pi/n}$ radians:
$$ r\colon\mathbb{R}^{2}\to\mathbb{R}^{2} \tag{1}$$
which acts like the linear transformation
$$ r \begin{pmatrix} x\\ y \end{pmatrix} := \begin{pmatrix} \cos(2\pi/n) & -\sin(2\pi/n)\\ \sin(2\pi/n) & \cos(2\pi/n) \end{pmatrix} \begin{pmatrix} x\\ y \end{pmatrix}. \tag{2}$$
We see that the image of our ${n}$-gon under this transformation ${r(X)=X}$ remains invariant. </p>
<p>
The other transformation worth exploring is reflecting about the ${x}$-axis, ${s\colon\mathbb{R}^{2}\to\mathbb{R}^{2}}$ which may be defined by
$$ s \begin{pmatrix} x\\ y \end{pmatrix} := \begin{pmatrix} 1 & 0\\ 0 & -1 \end{pmatrix} \begin{pmatrix} x\\ y \end{pmatrix}. \tag{3}$$
This transformation also leaves our polygon invariant ${s(X)=X}$. </p>
<p>
We can compose these two types of transformations. Observe that ${s\circ s=\mathrm{id}}$ and the ${n}$-fold composition ${r^{n}=r\circ\dots\circ r=\mathrm{id}}$ both yield the identity transformation ${\mathrm{id}(x)=x}$ for all ${x\in\mathbb{R}^{2}}$. Then we have ${2n}$ symmetry transformations: ${\mathrm{id}}$, ${r}$, ..., ${r^{n-1}}$; and ${s}$, ${s\circ r}$, ..., ${s\circ r^{n-1}}$. What about, say, ${r\circ s}$? We find ${s\circ r^{k}\circ s=r^{-k}}$, so ${r^{k}\circ s = s\circ r^{-k}}$. Thus it's contained in our list of symmetry transformations. </p>
<p>
The symmetry group thus constructed is called the <dfn>Dihedral Group</dfn>. Geometers denote it by ${D_{n}}$, algebraists denote it by ${D_{2n}}$, and we denote it by ${D_{n}}$.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">6.</span> <span class="label">Example (Rotations of regular polygon).</span> We can restrict our attention, working with the previous example further, to only <em>rotations</em> of the regular ${n}$-gon by multiples of ${2\pi/n}$ radians. We can describe this group as "generated by a single element", i.e., symmetries are of the form ${r^{k}}$ for ${k\in\mathbb{Z}}$. This is an example of a <dfn>Cyclic Group</dfn>. In particular, it is commutative: any symmetries ${r_{1}}$ and ${r_{2}}$ satisfy ${r_{1}\circ r_{2}=r_{2}\circ r_{1}}$. These are special situations, let us carve out space to define these concepts explicitly.
</p>
</section>
<section class="proposition Definition">
<p>
<span class="number">7.</span> <span class="label">Definition.</span> We call a group ${G}$ <dfn>Abelian</dfn> if it is commutative, i.e., for any transformations ${f}$, ${g\in G}$ we have ${f\circ g = g\circ f}$. In this case, we write ${f\circ g}$ as ${f+g}$, using the plus sign to stress commutativity.
</p>
</section>
<section class="proposition Definition">
<p>
<span class="number">8.</span> <span class="label">Definition.</span> We call a group ${G}$ <dfn>Cyclic</dfn> if there is at least one element ${g\in G}$ such that ${\{g^{n}\mid n\in\mathbb{Z}\}=G}$ the entire group consists of iterates of ${g}$ and ${g^{-1}}$.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">9.</span> <span class="label">Example (Number Systems).</span> Another few examples the reader may know are the familiar number systems under addition: the integers ${\mathbb{Z}}$, the rational numbers ${\mathbb{Q}}$, the real numbers ${\mathbb{R}}$, and the complex numbers ${\mathbb{C}}$. They are commutative groups.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">10.</span> <span class="label">Example (Infinite dihedral).</span> We can take the infinite limit of the dihedral group to get the infinite dihedral group ${D_{\infty}}$. We formally describe it as consisting of "rotations" ${r}$ and "reflections" ${s}$ such that
<ol>
<li> ${r^{m}\circ r^{n} = r^{m+n}}$ for any ${m}$, ${n\in\mathbb{Z}}$; </li>
<li> ${s\circ r^{m}\circ s = r^{-m}}$ for any ${m\in\mathbb{Z}}$; </li>
<li> ${s\circ s = e}$; </li>
<li> ${r^{n}\circ r^{-n} = r^{-n}\circ r^{n} = e}$ for any ${n\in\mathbb{Z}}$, in particular ${r^{0}=e}$. </li>
</ol>
In this sense, the "infinite limit" turns rotations into something like the integers.
</p>
</section>
<section class="proposition Example">
<p>
<span class="number">11.</span> <span class="label">Example (Circular dihedral).</span> A more intuitive "infinite limit" of the dihedral group is the symmetries of the unit circle ${S^{1}}$ in the plane ${\mathbb{R}^{2}}$. These are anti-clockwise rotations and reflection about the ${x}$-axis, but rotations are parametrized by a real parameter (the "angle"):
$$ r_{\theta}~``=\!\!\mbox{"} \begin{pmatrix}\cos(\theta) & -\sin(\theta)\\ \sin(\theta) & \cos(\theta) \end{pmatrix}. \tag{4}$$
Here we write an "equals" sign in quotes because this is the intuition. A group is <em>abstract</em>, whereas the matrix is a concrete realization of the symmetry. </p>
<p>
The reader should verify the axioms for a group are satisfied, with the hint that ${r_{\theta}\circ r_{\phi} = r_{\theta+\phi}}$ and the usual relation between reflection and rotation holds. </p>
<p>
This group is called the <dfn>Orthogonal Group</dfn> in 2-dimensions.
</p>
</section>
<h1>Exercises</h1>
<section class="proposition Exercise">
<p>
<span class="label">Exercise 1.</span> Is ${\mathbb{Z}}$ a cyclic group? Is ${\mathbb{C}}$ a cyclic group?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise 2.</span> Is the non-negative integers ${\mathbb{N}_{0}}$ a group under addition? Under multiplication?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise 3.</span> Are the positive real numbers ${\mathbb{R}_{\text{pos}}}$ a group under multiplication?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise 4.</span> Pick your favorite polyhedron in 3-dimensions. Determine its symmetry group.
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise 5.</span> Complex conjugation acts on ${\mathbb{C}}$ by sending ${x+i\cdot y}$ to ${x-i\cdot y}$. Does this give us a symmetry group?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise 6 (challenging).</span> If we consider polynomials with coefficients in, say, rational numbers (denoted ${\mathbb{Q}[x]}$ for polynomials with the unknown ${x}$), then how can we form a symmetry group of ${\mathbb{Q}[x]}$?
</p>
</section>
<section class="proposition Exercise">
<p>
<span class="label">Exercise 7 (General Linear Group).</span> Take ${n\in\mathbb{N}}$ to be a fixed positive integer, preferably ${n\geq2}$. Consider the collection of invertible ${n}$-by-${n}$ matrices with entries which are rational numbers
$${\mathrm{GL}(n, \mathbb{Q}) = \{ M\in\mathrm{Mat}(n\times n, \mathbb{Q}) \mid \det(M)\neq0\}.}$$
Prove this is a group under matrix multiplication.
</p>
</section>
pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com1tag:blogger.com,1999:blog-3776650590176552530.post-64262497676847862312012-12-16T09:33:00.000-08:002012-12-16T09:33:37.747-08:00TeX macro for normal operator ordering<p>I've always been bothered with normal operator ordering, writing <code>$:O(a)O(b):$</code> always produces bad results. <br />
</p><p>The quick fix I've been using is the following:<br />
</p><pre>\def\normOrd#1{\mathop{:}\nolimits\!#1\!\mathop{:}\nolimits}
%%
% example:
% \begin{equation}
% \normOrd{a(z)b(\omega)} = a(z)_{+}b(\omega)+(-1)^{\alpha\beta}b(\omega)a(z)_{-}
% \end{equation}
%%
</pre>Which in practice looks like:<br />
<br />
<div class="separator" style="clear: both; text-align: center;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgPDQiueiVMDrxfzmkFY_TMYWQ41ARLX5ZhRY7j-RS8OOJ8e9Vr1DMnb7poj4ChDXL0GLzkmVEnc-Q51mVvwhm2m6pmBXAHkwBs2tZAXY_hAeNP7graj7MIs7wS8ISUN_B_w2Egp6l0EoE/s1600/foo.png" imageanchor="1" style="margin-left:1em; margin-right:1em"><img border="0" height="25" width="400" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgPDQiueiVMDrxfzmkFY_TMYWQ41ARLX5ZhRY7j-RS8OOJ8e9Vr1DMnb7poj4ChDXL0GLzkmVEnc-Q51mVvwhm2m6pmBXAHkwBs2tZAXY_hAeNP7graj7MIs7wS8ISUN_B_w2Egp6l0EoE/s400/foo.png" /></a></div><h2>How I got this solution</h2>I determined this solution iteratively after many different attempts, which I shall enumerate along with the problems they each had.<br />
<br />
However, using mere colons <code>:a(z)b(\omega): = ...</code> produces the following:<br />
<div class="separator" style="clear: both; text-align: center;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhbNrjzcP_XTICLxGms6SxuECKLBuvnhe4c0Kmqk2Gb03L4Oqkcd26ovlok482paE2U27peRjPLfC3Qn8UIfUqancyEBj6Ppmde8N2WW7mOYzYUx-A67jbRqoVfyT3f3fvQ3SR8oDXSQUM/s1600/bad1.png" imageanchor="1" style="margin-left:1em; margin-right:1em"><img border="0" height="24" width="400" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhbNrjzcP_XTICLxGms6SxuECKLBuvnhe4c0Kmqk2Gb03L4Oqkcd26ovlok482paE2U27peRjPLfC3Qn8UIfUqancyEBj6Ppmde8N2WW7mOYzYUx-A67jbRqoVfyT3f3fvQ3SR8oDXSQUM/s400/bad1.png" /></a></div>Being clever, I asked myself "Hey, why not write <code>:x\colon</code> for the normal ordering?" This was clever, but wrong. Consider the following example:<br />
<pre>g = :x\colon
</pre>Producing:<br />
<div class="separator" style="clear: both; text-align: center;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjVkPnjWCi-vwEme5YWXkT3_p6tIJcrXQKwSwdCnHnRLaqbyteZzppWknquidScG77nCjKmd-uOBjPOuPhs8IzZdF7M4_To6zIGDGWcEHn41BzFiDrIMZuxfS22S0bRkdmAiN4t-JMVc68/s1600/bad2.png" imageanchor="1" style="margin-left:1em; margin-right:1em"><img border="0" height="30" width="166" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjVkPnjWCi-vwEme5YWXkT3_p6tIJcrXQKwSwdCnHnRLaqbyteZzppWknquidScG77nCjKmd-uOBjPOuPhs8IzZdF7M4_To6zIGDGWcEHn41BzFiDrIMZuxfS22S0bRkdmAiN4t-JMVc68/s400/bad2.png" /></a></div>Not one to give up easily, I found a <code>\cocolon</code> definition on <a href="http://tex.stackexchange.com/q/2300">tex.stackexchange</a>. Trying that instead:<br />
<pre>g = \cocolon x\colon = y
</pre>Produces strange extra whitespace on the right:<br />
<div class="separator" style="clear: both; text-align: center;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEj1rHLdXGfKDtstA2K4jLJhoe6IWcZzgcR9b9tMJ199kHG_TZPAui6qveEa7CSgvmVYfbzlB9mQ4KQ9uQPha3wy31NxZU2qrA3oo-rys2Gc2YyFCr4nVvY2IzLWfB4ir7fbwqhhJP9UvW8/s1600/bad3.png" imageanchor="1" style="margin-left:1em; margin-right:1em"><img border="0" height="30" width="264" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEj1rHLdXGfKDtstA2K4jLJhoe6IWcZzgcR9b9tMJ199kHG_TZPAui6qveEa7CSgvmVYfbzlB9mQ4KQ9uQPha3wy31NxZU2qrA3oo-rys2Gc2YyFCr4nVvY2IzLWfB4ir7fbwqhhJP9UvW8/s400/bad3.png" /></a></div>After examining the co-colon code, I just determined that something along the lines of<br />
<pre>% rough draft definition #1
\def\normOrd#1{\mathrel{:}\!#1\!\mathrel{:}}
</pre>would work. This didn't quite work, the whitespacing was strange. So instead I just use <code>\mathop{:}\nolimits...</code>, which produces the desired result.pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com5tag:blogger.com,1999:blog-3776650590176552530.post-81940705587074861242012-08-12T09:00:00.000-07:002012-08-12T09:00:03.035-07:00Revising my Notes on General Relativity<p>So I've been revising my notes on general relativity, and I've found several things worth mentioning.<br />
</p><p><b>1. Equivalence Principle.</b> The equivalence principle gives us geometry. This is often poorly described (I too committed this error in my drafts). <br />
</p><p>The equivalence principle tells us neither the composition of a body nor its mass determines its trajectory in a gravitational field. So gravity determines <em>paths</em>, and this gives us geometry.<br />
</p><p>Moreover, there are <em>different</em> equivalence principles which should be mentioned. I yielded to this, and became incoherent (alas!). The trick is to stick this into a box, for the interested reader to find out more about it, but not obstruct the writing.<br />
</p><p><b>2. Coordinates for Black Hole.</b> Different coordinates for the Schwarzschild solution are described beautifully in Hans Stephani, Dietrich Kramer, Malcolm MacCallum, Cornelius Hoenselaers, and Eduard Herlt's <em>Exact Solutions of Einstein’s Field Equations</em> (Cambridge University Press, 2d edition, 2009).<br />
</p><p><b>3. Manifolds, Mathematics.</b> I think I ought to examine Christopher Isham's <em>Modern Differential Geometry for Physicists</em> for a Physicist's differential geometry.<br />
</p><p>I should like to discuss the exponential map, which relates paths to geometry (as alluded in the equivalence principle discussion). <br />
</p><p>Most readers probably will agree that "Part II" of my notes (which specifically discuss differential geometry) are the toughest part of the notes. <br />
</p><p>Probably, I should mention a few examples of manifolds and explicitly study their coordinates in lecture 5.<br />
</p><p><b>3.1. Functions.</b> I never discussed what it means for a function on a manifold (a) to exist, (b) to be smooth.<br />
</p><p>Really, this let us discuss curves too. Why? A curve is just a function γ:<em>I</em>→<em>M</em> where <em>I</em> is just a closed interval, and <em>M</em> is the manifold.<br />
</p><p><b>3.2. Diffeomorphisms.</b> This word is thrown around a lot, but never defined rigorously (or at all!). So I should re-investigate this a bit.<br />
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-57696427649104426632012-05-25T17:34:00.001-07:002012-05-28T19:45:55.011-07:00Vertex algebras<p>Think about your favorite Lie algebra Lie(G). We have a mapping on it, namely, the <a href="http://en.wikipedia.org/wiki/Adjoint_representation_of_a_Lie_algebra">adjoint representation</a>:<br />
</p><p style="padding-left:1cm;">ad:Lie(G) → End[Lie(G)]<br />
</p><p>where "End[Lie(G)]" are the endomorphisms of the Lie algebra Lie(G).<br />
</p><p>Normally this is of the form "ad(u)v∈Lie(G)" and is shorthand for "ad(u)=[u,-]".<br />
</p><p>The Jacobi identity looks like:<br />
</p><p style="padding-left:1cm;">ad(u)ad(v)-ad(v)ad(u)=ad(ad(u)v).<br />
</p><p>This is the most important identity. Vertex operator algebras are an algebra with a similar property.<br />
</p><p>A vertex operator algebra consists of a vector space V equipped with a mapping usually denoted<br />
</p><p style="padding-left:1cm;">Y:V→(End V)[[x,x<sup>-1</sup>]].<br />
</p><p>In this form, it looks like left-multiplication operator...or that's the intuition anyways. So if "v∈V", we should think Y(v,x) belongs to "(End V)[[x,x<sup>-1</sup>]]" and acts on the left.<br />
</p><p>Really through <a href="http://en.wikipedia.org/wiki/Currying">currying</a> this should be thought of as "V⊗V→V[[x,x<sup>-1</sup>]]", i.e., a sort of multiplication operator with a parameter "x". (This is related to the "state-operator correspondence" physicists speak of with conformal field theories.)<br />
</p><p>Just like a Lie algebra, the Vertex Operator algebra satisfies a Jacobi identity and it is the most important defining property for the VOA.<br />
</p><p>Lets stop and look at this structure again:<br />
</p></p><p style="padding-left:1cm;">Y:V→(End V)[[x,x<sup>-1</sup>]].<br />
</p><p>What's the codomain exactly? Well, it's a formal <em>distribution</em> (<b>not</b> a mere formal power series!).<br />
</p><p>So what does one look like? Consider δ(z-1) = Σ z<sup>n</sup> where the summation ranges over n∈ℤ. This series representation is a formal distribution, and behaves in the obvious way. Lets prove this!<br />
</p><p><b>Desired Property:</b> δ(z-1) vanishes almost everywhere. <br />
</p><p>Consider the geometric series f(z) = Σz<sup>n</sup> where n is any non-negative integer (n=0,1,...).<br />
</p><p>Observe that δ(z-1) = f(z) + z<sup>-1</sup>f(z<sup>-1</sup>). Lets now substitute in the resulting geometric series:<br />
</p><p style="padding-left:1cm;">δ(z-1) = [1/(1-z)] + z<sup>-1</sup>[1/(1-z<sup>-1</sup>)]<br />
</p><p>and after some simple arithmetic we see for z≠1 we have δ(z-1)=0. <br />
</p><p><b>Desired Property:</b> for any Laurent polynomial f(z) we have δ(z-1)f(z)=δ(z-1)f(1).<br />
</p><p>This turns out to be true, thanks to the magic of infinite series; but due to html formatting, I omit the proof. The proof is left as an exercise to the reader (the basic sketch is consider δ(z-1)z<sup>n</sup>, then prove linearity, and you're done).<br />
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-65335284522256622422012-05-18T12:36:00.001-07:002012-05-18T12:36:54.428-07:00Finite Field with Four Elements<p>Small note to myself on notational problems when facing finite groups.<br />
</p><p>Recall the finite field with four elements is ℤ<sub>2</sub>[x]/(1+x+x<sup>2</sup>). <br />
</p><p>People often write ω = 1+x and <span style="text-decoration:overline;">ω</span>=x. Observe then that <span style="text-decoration:overline;">ω</span><sup>2</sup> = ω, and ω<sup>2</sup> = <span style="text-decoration:overline;">ω</span>. Moreover ω<span style="text-decoration:overline;">ω</span>=1 and 1+ω+<span style="text-decoration:overline;">ω</span>=0.<br />
</p><p>I have only seen this ω notation specified in Pless' <em>Error Correcting Codes</em>, Third ed., page 102 et seq.<br />
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-75632390247699909652012-03-16T12:03:00.000-07:002012-03-16T12:03:22.491-07:00End notes and Foot notes in LaTeX<p>
So I was writing up notes for a reading group on Afghanistan, and it has apparently become fashionable to use endnotes in the humanities. Being fond of Edward Gibbon, I use footnotes excessively. Irritating everyone, I use both while making it indistinguishable whether I refer to a footnote or endnote by a superscripted number.
</p>
<p>
How to do this in LaTeX? Quite simple:
</p>
<pre>
\documentclass{article}
\usepackage{endnotes}
\makeatletter
\newcommand*{\dupcntr}[2]{%
\expandafter\let\csname c@#1\expandafter\endcsname\csname c@#2\endcsname
}
\dupcntr{endnote}{footnote}
\renewcommand\theendnote{\thefootnote}
\makeatother
\begin{document}
Blah blah blah.
\end{document}
</pre>
<p>
It turns out to work quite well.
</p>
<p>
I modified some macros from a <a href="http://tex.stackexchange.com/questions/33898/slave-duplicate-counter">TeX Stackexchange</a> discussion on "slave counters"...so I get only partial credit.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-73850860216013854982012-02-21T10:54:00.000-08:002012-02-21T10:55:29.284-08:00Metapost and Labels<p>
This is just a quick note to myself. When I want to write a label with a smaller font, I should use <code>\scriptstyle</code>...but it is tricky since it requires <b>math mode!</b>
</p>
<p>
So an example, consider this diagram describing an experiment for gravitational redshift:
</p>
<pre>
numeric u;
u = 1pc;
beginfig(0)
path earth;
pair clock[];
earth = fullcircle scaled u;
clock[0] = (0,2u);
clock[1] = (0,4u);
draw (0,0)--(0,5u) dashed evenly;
for i=0 upto 1:
label(btex $\bullet$ etex, clock[i]);
endfor;
fill earth withcolor 0.75white;
draw earth;
label.rt(btex ${\scriptstyle\rm Earth}$ etex, (.5u,0));
label.rt(btex ${\scriptstyle\rm Satellite\ 1}$ etex, clock[0]);
label.rt(btex ${\scriptstyle\rm Satellite\ 2}$ etex, clock[1]);
endfig;
end;
</pre>
<p>
Just remember to use "<code>\ </code>" for spaces. Otherwise it will all run together horribly!
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-59300782745271084822012-02-14T13:21:00.000-08:002012-02-14T13:26:55.862-08:00Feynman Diagrams and Motives<p>
I have been re-reading the following book:
</p>
<p style="margin-left:3em;">
Alain Connes and Matilde Marcolli, <br />
<i>Noncommutative Geometry, Quantum Fields, and Motives</i>, <br />
Colloquium Publications, Vol.55, American Mathematical Society, 2008.
</p>
<p>
It turns out that Dr Marcolli has taught a <a href="http://www.its.caltech.edu/~matilde/course2008.html">course</a> on related material back in 2008! It is mostly dealing with the first chapter of the book.
</p>
<h2>Hopf Algebras and Feynman Calculations</h2>
<p>
There is a nice review of Hopf algebras used in Feynman diagram calculations:
</p>
<p style="margin-left:3em;">
Kurusch Ebrahimi-Fard, Dirk Kreimer, <br />
"Hopf algebra approach to Feynman diagram calculations". <br />
Eprint <a href="http://arxiv.org/abs/hep-th/0510202v2">arXiv:hep-th/0510202v2</a>, 30 pages.
</p>
<p>
For another specifically reviewing the noncommutative approach discussed in Connes and Matilde's book, see:
</p>
<p style="margin-left:3em;">
Herintsitohaina Ratsimbarison, <br />
"Feynman diagrams, Hopf algebras and renormalization."<br />
Eprint <a href="http://arxiv.org/abs/math-ph/0512012v2">arXiv:math-ph/0512012v2</a>, 12 pages.
</p>
<p>
What is a "Hopf algebra", anyways?
</p>
<p style="margin-left:3em;">
Pierre Cartier, <br />
"A primer of Hopf algebras." <br />
<a href="http://www.math.osu.edu/~kerler.2/VIGRE/InvResPres-Sp07/Cartier-IHES.pdf">Eprint <tt>[math.osu.edu]</tt></a>, 81 pages.
</p>
<h3>Hopf Algebras</h3>
<p>
What the deuce is a "Hopf algebra"? That's a very good question, and I'm very glad you asked it.
Wikipedia has its <a href="">definition</a>, which may or may not be enlightening.
</p>
<p>
Lets consider a concrete example. Consider a finite group G, and the field of complex number ℂ. We assert the collection Hom(G,ℂ) is a Hopf algebra.
</p>
<p>
Recall we have multiplication of group elements. This is a mapping G×G→G.
</p>
<p>
Now, observe we have functoriality to give us a mapping Hom(G×G→G,ℂ) = ℂ<sup>G</sup>→ℂ<sup>G</sup>×ℂ<sup>G</sup>. Lets call this thing Δ
</p>
<p>
Great, but what does it do? Good question!
</p>
<p>
Take some f∈Hom(G,ℂ) then what is Δ(f)?
</p>
<p>
It is a function of two variables, [Δ(f)](x,y). Functoriality demands, if we fix one of the arguments to be the identity element e∈G of the group, then [Δ(f)](e,y)=f(y) and [Δ(f)](x,e)=f(x).
</p>
<p>
It follows logically that [Δ(f)](x,y)=f(xy).
</p>
<p>
We also need to consider the antipode map S:ℂ<sup>G</sup>→ℂ<sup>G</sup>. We have [S(f)](x) be determined by the Hopf property, and a long story short [S(f)](x)=f(x<sup>-1</sup>).
</p>
<p>
Note that the antipode map is a <b>generalization</b> of the "group inverse" notion.
</p>
<p>
The other algebraic structure is a triviality, lets consider other interesting applications!
</p>
<h3>Feynman Diagrams</h3>
<p>
Now, I have written <a href="http://notebk.googlecode.com/files/feynman.pdf">some notes <tt>[pdf]</tt></a> on the basic algorithm evaluating Feynman diagrams and producing a number (the "probability amplitude").
</p>
<p>
As I understand it (and I don't!!) Ebrahimi-Fard and Kreimer suggest considering the Hopf algebra of "Feynman graphs" (which are just considered as colored graphs representing physical processes).
</p>
<p>
The basic algorithm to evaluating Feynman diagrams are based on the "Feynman rules" (what we assign to each edge, vertex, etc.). So Feynman rules are linear and multiplicative maps, associating to each Feynman graph (again, seen as a collection of vertices and edges) its corresponding <b>Feynman integral</b>.
</p>
<p>
So these maps are the important things, which enable us to algorithmically do stuff.
</p>
<p>
Lets stop! I said "Feynman integrals" are assigned to each graph...am I drunk, or is that correct?
</p>
<p>
Yes yes, the answer is "yes" ;)
</p>
<p>
What a horrible joke...but what I mean is: the scattering process of electrons, for example, is the infinite sum taking into account all the virtual processes.
</p>
<p>
Usually we only care up to a few orders.
</p>
<p>
Of course, this is my understanding of the Hopf algebra treatment of Feynman diagrams...and I openly admit: <b>I could be completely wrong!</b>
</p>
<p>
So to figure it out, I'll stop rambling, and continue reading.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-39626704031083745202012-02-06T10:13:00.000-08:002012-02-06T10:13:26.704-08:00(Ramblings on) Writing Notes on Quantum Field Theory<p>
So, in the long run, my aim is to write great notes on quantum field theory and quantum gravity. Since quantum gravity <em>depends</em> on quantum field theory, it makes sense to begin there!
</p>
<p>
For those uninterested in my rambling thought process, here's the punch line: just as integrals and derivatives are first covered symbolically in calculus, then rigorously in analysis...we likewise believe that a naive and symbolic approach first ought to be covered, then a rigorous and axiomatic approach second.
</p>
<p>
Greiner and Reinhardt's <em>Field Quantization</em> provides a good level for detail, at least for the naive/symbolic treatment of field theory.
</p>
<h2>What Other People Do</h2>
<p>
The basic approach other books take is "Well, here's Feynman diagrams. Quantum Field Theory just plays with these...here's how you get Feynman rules...and here's renormalization, the end."
</p>
<p>
This is not terrible. But it is lacking a certain <em>je ne sais quoi</em>.
</p>
<p>
So instead, perhaps I should look at it from the mathematical perspective. This has its own problems.
</p>
<h2>Depends on...</h2>
<p>
The problem I have is with <b>dependencies!</b> It doesn't make sense to write about quantum field theory without first writing about classical field theory, quantum mechanics, and a bit about functional analysis.
</p>
<p>
I have written a note about <a href="http://notebk.googlecode.com/files/rqm.pdf">Relativistic Quantum Mechanics <tt>[pdf]</tt></a> (which may make more sense after reading my notes on <a href="http://notebk.googlecode.com/files/lieGroups.lieAlgebras.Representations.gamma.pdf">Lie Groups, Lie Algebras, and their Representations <tt>[pdf]</tt></a>).
</p>
<p>
However, there is still more to do with quantum mechanics. Particularly, the subject of <b>scattering theory</b> is lacking. (Erik Koelink has some great <a href="http://fa.its.tudelft.nl/~koelink/dictaat-scattering.pdf">Lecture Notes <tt>[tudelft.nl]</tt></a> too)
</p>
<p>
Despite my notes on <a href="http://notebk.googlecode.com/files/functionalQFT.pdf">Functional Techniques in Path Integral Quantization <tt>[pdf]</tt></a>, I still feel lacking in the "path integral" department.
</p>
<p>
Perhaps I should write notes on measure theory, functional analysis, then tackle Glimm and Jaffe's <em>Quantum physics: a functional integral point of view</em>?
</p>
<p>
With classical field theory, the subject quickly becomes a can of worms (sadly enough).
</p>
<p>
Gauge theory, as Derek Wise notes in his blog post <a href="http://dkwise.wordpress.com/2012/01/30/the-geometric-role-of-symmetry-breaking-in-gravity/">"The geometric role of symmetry breaking in gravity"</a>, is intimately connected to Cartan Geometry.
</p>
<p>
There are dozens of exercises/examples to consider in gauge theory: Yang-Mills Theory, Born-Infield Action, Non-linear Sigma-Model, Non-linear Electrodynamics, Chern-Simons Theory, etc.
</p>
<h2>What Outline</h2>
<p>
So far, I've been considering my obstacles...but what about an outline?
</p>
<p>
The model I am following is the treatment of integration and differentiation in mathematics. First we have the <b>naive</b> symbolic manipulations (as done in calculus), then later we have the <b>formal and rigorous</b> proof based approach (as done in analysis).
</p>
<p>
Perhaps we should begin with <b>naive field theory</b>, where we obtain classical field theory "naively" from a "many body" problem.
</p>
<p>
This has merit from modelling fields as densities on the intuitive level.
</p>
<p>
Canonical quantization of this scheme becomes a triviality.
</p>
<p>
The problem with this approach is: what about the treatment of gauge theories, and their quantization?
</p>
<p>
After a few miracles, I expect to end up working with path integral quantization and formal calculus.
</p>
<p>
Naive treatment on quantizing gauge systems ought to be considered a bit more closely...
</p>
<p>
So that concludes the "naive" approach, and we begin the <b>Axiomatic Approach</b>. We should clarify the term "Axiom" means <b>specification</b> (not "God given truth", as dictionaries insist!).
</p>
<p>
The axiomatic approach would be done in a "guess-and-check" manner, modifying the axioms as necessary.
</p>
<p>
We naturally begin with Wightman axioms for the canonical approach, and the Osterwalder-Schrader axioms for the path integral approach. (Quickly, we ought to prove these two are equivalent!)
</p>
<p>
Kac's <em>Vertex Algebras for Beginners</em> takes the Wightman axioms, then extends them to conformal field theory through some magic. Perhaps this would be a worth-while example to consider?
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-14218549286783092812012-01-20T08:55:00.000-08:002012-01-20T09:02:50.304-08:00Studying Tactics<p>
My friend asked me for help on military tactics. "Where'd you get the idea I know anything about that?" I asked.
</p>
<p>
"I thought game theory was known to all mathematicians," my friend sheepishly replied.
</p>
<p>
Well, he's wrong about that. But I later found Clausewitz's suggestion <a href="http://www.gutenberg.org/files/1946/1946-h/1946-h.htm#2HCH0014">on examples</a>:
</p>
<blockquote>
<p>
EXAMPLES from history make everything clear, and furnish the best description of proof in the empirical sciences. This applies with more force to the Art of War than to any other. General Scharnhorst, whose handbook is the best ever written on actual War, pronounces historical examples to be of the first importance, and makes an admirable use of them himself. Had he survived the War in which he fell, the fourth part of his revised treatise on artillery would have given a still greater proof of the observing and enlightened spirit in which he sifted matters of experience.
</p>
<p>
But such use of historical examples is rarely made by theoretical writers; the way in which they more commonly make use of them is rather calculated to leave the mind unsatisfied, as well as to offend the understanding. We therefore think it important to bring specially into view the use and abuse of historical examples.
</p>
<p>
[...]
</p>
<p>
Now, if we consider closely the use of historical proofs, four points of view readily present themselves for the purpose.
</p>
<p>
First, they may be used merely as an EXPLANATION of an idea. In every abstract consideration it is very easy to be misunderstood, or not to be intelligible at all: when an author is afraid of this, an exemplification from history serves to throw the light which is wanted on his idea, and to ensure his being intelligible to his reader.
</p>
<p>
Secondly, it may serve as an APPLICATION of an idea, because by means of an example there is an opportunity of showing the action of those minor circumstances which cannot all be comprehended and explained in any general expression of an idea; for in that consists, indeed, the difference between theory and experience. Both these cases belong to examples properly speaking, the two following belong to historical proofs.
</p>
<p>
Thirdly, a historical fact may be referred to particularly, in order to support what one has advanced. This is in all cases sufficient, if we have ONLY to prove the POSSIBILITY of a fact or effect.
</p>
<p>
Lastly, in the fourth place, from the circumstantial detail of a historical event, and by collecting together several of them, we may deduce some theory, which therefore has its true PROOF in this testimony itself.
</p>
<p>
For the first of these purposes all that is generally required is a cursory notice of the case, as it is only used partially. Historical correctness is a secondary consideration; a case invented might also serve the purpose as well, only historical ones are always to be preferred, because they bring the idea which they illustrate nearer to practical life.
</p>
<p>
The second use supposes a more circumstantial relation of events, but historical authenticity is again of secondary importance, and in respect to this point the same is to be said as in the first case.
</p>
<p>
For the third purpose the mere quotation of an undoubted fact is generally sufficient. If it is asserted that fortified positions may fulfil their object under certain conditions, it is only necessary to mention the position of Bunzelwitz [Frederick the Great's celebrated entrenched camp in 1761] in support of the assertion.
</p>
<p>
But if, through the narrative of a case in history, an abstract truth is to be demonstrated, then everything in the case bearing on the demonstration must be analysed in the most searching and complete manner; it must, to a certain extent, develop itself carefully before the eyes of the reader. The less effectually this is done the weaker will be the proof, and the more necessary it will be to supply the demonstrative proof which is wanting in the single case by a number of cases, because we have a right to suppose that the more minute details which we are unable to give neutralise each other in their effects in a certain number of cases.
</p>
<p>
If we want to show by example derived from experience that cavalry are better placed behind than in a line with infantry; that it is very hazardous without a decided preponderance of numbers to attempt an enveloping movement, with widely separated columns, either on a field of battle or in the theatre of war—that is, either tactically or strategically—then in the first of these cases it would not be sufficient to specify some lost battles in which the cavalry was on the flanks and some gained in which the cavalry was in rear of the infantry; and in the tatter of these cases it is not sufficient to refer to the battles of Rivoli and Wagram, to the attack of the Austrians on the theatre of war in Italy, in 1796, or of the French upon the German theatre of war in the same year. The way in which these orders of battle or plans of attack essentially contributed to disastrous issues in those particular cases must be shown by closely tracing out circumstances and occurrences. Then it will appear how far such forms or measures are to be condemned, a point which it is very necessary to show, for a total condemnation would be inconsistent with truth.
</p>
<p>
It has been already said that when a circumstantial detail of facts is impossible, the demonstrative power which is deficient may to a certain extent be supplied by the number of cases quoted; but this is a very dangerous method of getting out of the difficulty, and one which has been much abused. Instead of one well-explained example, three or four are just touched upon, and thus a show is made of strong evidence. But there are matters where a whole dozen of cases brought forward would prove nothing, if, for instance, they are facts of frequent occurrence, and therefore a dozen other cases with an opposite result might just as easily be brought forward. If any one will instance a dozen lost battles in which the side beaten attacked in separate converging columns, we can instance a dozen that have been gained in which the same order was adopted. It is evident that in this way no result is to be obtained.
</p>
<p>
Upon carefully considering these different points, it will be seen how easily examples may be misapplied.
</p>
<p>
An occurrence which, instead of being carefully analysed in all its parts, is superficially noticed, is like an object seen at a great distance, presenting the same appearance on each side, and in which the details of its parts cannot be distinguished. Such examples have, in reality, served to support the most contradictory opinions. To some Daun's campaigns are models of prudence and skill. To others, they are nothing but examples of timidity and want of resolution. Buonaparte's passage across the Noric Alps in 1797 may be made to appear the noblest resolution, but also as an act of sheer temerity. His strategic defeat in 1812 may be represented as the consequence either of an excess, or of a deficiency, of energy. All these opinions have been broached, and it is easy to see that they might very well arise, because each person takes a different view of the connection of events. At the same time these antagonistic opinions cannot be reconciled with each other, and therefore one of the two must be wrong.
</p>
<p>
Much as we are obliged to the worthy Feuquieres for the numerous examples introduced in his memoirs—partly because a number of historical incidents have thus been preserved which might otherwise have been lost, and partly because he was one of the first to bring theoretical, that is, abstract, ideas into connection with the practical in war, in so far that the cases brought forward may be regarded as intended to exemplify and confirm what is theoretically asserted—yet, in the opinion of an impartial reader, he will hardly be allowed to have attained the object he proposed to himself, that of proving theoretical principles by historical examples. For although he sometimes relates occurrences with great minuteness, still he falls short very often of showing that the deductions drawn necessarily proceed from the inner relations of these events.
</p>
<p>
Another evil which comes from the superficial notice of historical events, is that some readers are either wholly ignorant of the events, or cannot call them to remembrance sufficiently to be able to grasp the author's meaning, so that there is no alternative between either accepting blindly what is said, or remaining unconvinced.
</p>
<p>
It is extremely difficult to put together or unfold historical events before the eyes of a reader in such a way as is necessary, in order to be able to use them as proofs; for the writer very often wants the means, and can neither afford the time nor the requisite space; but we maintain that, when the object is to establish a new or doubtful opinion, one single example, thoroughly analysed, is far more instructive than ten which are superficially treated. The great mischief of these superficial representations is not that the writer puts his story forward as a proof when it has only a false title, but that he has not made himself properly acquainted with the subject, and that from this sort of slovenly, shallow treatment of history, a hundred false views and attempts at the construction of theories arise, which would never have made their appearance if the writer had looked upon it as his duty to deduce from the strict connection of events everything new which he brought to market, and sought to prove from history.
</p>
<p>
When we are convinced of these difficulties in the use of historical examples, and at the same time of the necessity (of making use of such examples), then we shall also come to the conclusion that the latest military history is naturally the best field from which to draw them, inasmuch as it alone is sufficiently authentic and detailed.
</p>
<p>
In ancient times, circumstances connected with War, as well as the method of carrying it on, were different; therefore its events are of less use to us either theoretically or practically; in addition to which, military history, like every other, naturally loses in the course of time a number of small traits and lineaments originally to be seen, loses in colour and life, like a worn-out or darkened picture; so that perhaps at last only the large masses and leading features remain, which thus acquire undue proportions.
</p>
<p>
If we look at the present state of warfare, we should say that the Wars since that of the Austrian succession are almost the only ones which, at least as far as armament, have still a considerable similarity to the present, and which, notwithstanding the many important changes which have taken place both great and small, are still capable of affording much instruction. It is quite otherwise with the War of the Spanish succession, as the use of fire-arms had not then so far advanced towards perfection, and cavalry still continued the most important arm. The farther we go back, the less useful becomes military history, as it gets so much the more meagre and barren of detail. The most useless of all is that of the old world.
</p>
<p>
But this uselessness is not altogether absolute, it relates only to those subjects which depend on a knowledge of minute details, or on those things in which the method of conducting war has changed. Although we know very little about the tactics in the battles between the Swiss and the Austrians, the Burgundians and French, still we find in them unmistakable evidence that they were the first in which the superiority of a good infantry over the best cavalry was, displayed. A general glance at the time of the Condottieri teaches us how the whole method of conducting War is dependent on the instrument used; for at no period have the forces used in War had so much the characteristics of a special instrument, and been a class so totally distinct from the rest of the national community. The memorable way in which the Romans in the second Punic War attacked the Carthaginan possessions in Spain and Africa, while Hannibal still maintained himself in Italy, is a most instructive subject to study, as the general relations of the States and Armies concerned in this indirect act of defence are sufficiently well known.
</p>
<p>
But the more things descend into particulars and deviate in character from the most general relations, the less we can look for examples and lessons of experience from very remote periods, for we have neither the means of judging properly of corresponding events, nor can we apply them to our completely different method of War.
</p>
<p>
Unfortunately, however, it has always been the fashion with historical writers to talk about ancient times. We shall not say how far vanity and charlatanism may have had a share in this, but in general we fail to discover any honest intention and earnest endeavour to instruct and convince, and we can therefore only look upon such quotations and references as embellishments to fill up gaps and hide defects.
</p>
<p>
It would be an immense service to teach the Art of War entirely by historical examples, as Feuquieres proposed to do; but it would be full work for the whole life of a man, if we reflect that he who undertakes it must first qualify himself for the task by a long personal experience in actual War.
</p>
<p>
Whoever, stirred by ambition, undertakes such a task, let him prepare himself for his pious undertaking as for a long pilgrimage; let him give up his time, spare no sacrifice, fear no temporal rank or power, and rise above all feelings of personal vanity, of false shame, in order, according to the French code, to speak THE TRUTH, THE WHOLE TRUTH, AND NOTHING BUT THE TRUTH.
</p>
</blockquote>
<p>
<b>Addendum:</b> one may be interested in <a href="http://www.napoleonic-literature.com/Book_8/MaximsOfNapoleon.html">Napoleon's Maxims</a>, <a href="http://regimentalrogue.com/library/library-patton.htm">Patton's Reading List</a>, and Roosevelt's <a href="http://trevorhuxham.wordpress.com/2009/10/24/teddy-roosevelt%E2%80%99s-pigskin-library/">Pigskin Library</a>.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-35805855691167651822012-01-11T13:28:00.000-08:002012-01-11T13:28:54.385-08:00Puzzles<p>
Recently I've been more interested in puzzles.
</p>
<p>
<a href="http://projecteuler.net/">Project Euler</a> is the classic example of puzzles which require either higher math or computational skill (or both!).
</p>
<p>
Facebook has a <a href="http://www.facebook.com/careers/puzzles.php">collection of puzzles</a> too, motivated from the engineering perspective.
</p>
<p>
But note: Facebook uses these puzzles for hiring people. Plus, the puzzles are not always mathematically oriented.
</p>
<p>
I suppose a good mathematician should always set up puzzles for themselves. As Socrates remarked:
</p>
<blockquote>
<p>
SOCRATES: Indeed, Lysimachus, I should be very wrong in refusing to aid
in the improvement of anybody. And if I had shown in this conversation
that I had a knowledge which Nicias and Laches have not, then I admit
that you would be right in inviting me to perform this duty; but as we
are all in the same perplexity, why should one of us be preferred
to another? I certainly think that no one should; and under these
circumstances, let me offer you a piece of advice (and this need not go
further than ourselves). <b>I maintain, my friends, that every one of us
should seek out the best teacher whom he can find, first for ourselves,
who are greatly in need of one, and then for the youth, regardless of
expense or anything. But I cannot advise that we remain as we are. And
if any one laughs at us for going to school at our age, I would quote to
them the authority of Homer, who says, that
</p>
<p>
'Modesty is not good for a needy man.'
</p>
<p>
Let us then, regardless of what may be said of us, make the education of
the youths our own education.</b> (Emphasis added, from Plato's <a href="http://www.gutenberg.org/dirs/1/5/8/1584/1584.txt">Laches</a>)
</p>
</blockquote>
<p>
For example, I know a little bit about representations of Lie groups and Lie algebras (one can always learn more!)...but what about the representation of the quaternion group induced from the irreducible representations of SU(2)? How does it decompose into irreps? Etc.
</p>
<p>
Knuth remarked somewhere what helped him understand the representation theory for the symmetric group was writing a program which generated the permutation matrix representations.
</p>
<p>
I suspect writing a program which does these sorts of computations is a great puzzle for any mathematician that's savvy with programming.
</p>
<h2>Reading Material</h2>
<p>
And now, for something completely different.
</p>
<p>
A few papers I want to read: <br />
<a href="http://arxiv.org/abs/1201.1975">When physics helps mathematics: calculation of the sophisticated multiple integral</a>, 13 pages; <br />
<a href="http://arxiv.org/abs/1201.1992">Some algebraic properties of differential operators</a>, 15 pages; <br />
<a href="http://arxiv.org/abs/1112.3502">Introduction to supergravity</a>, 152 pages; <br />
<a href="http://arxiv.org/abs/1112.4669">Fermionic impurities in Chern-Simons-matter theories</a>, 31 pages; <br />
<a href="http://arxiv.org/abs/1201.2120">Spinors and Twistors in Loop Gravity and Spin Foams</a>, 16 pages; <br />
<a href="http://arxiv.org/abs/0711.2699">Quaternionic Analysis, Representation Theory and Physics</a>, 60 pages.
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com1tag:blogger.com,1999:blog-3776650590176552530.post-18405458805435117392012-01-06T08:55:00.000-08:002012-01-06T08:55:58.569-08:00Problem Notebooks<p>
I've been looking for the infamous Kourovka notebook, but there are apparently others.
</p>
<p>
Recall the Kourovka notebook is a collection of open problems in group theory. There are other notebooks with open problems in other fields.
</p>
<p>
For example, the <a href="http://math.usask.ca/~bremner/research/translations/dniester.pdf">Dniester Notebook <tt>[usask.ca]</tt></a> (pdf, 56 pages) has problems in ring theory.
</p>
<p>
The notebook stopped being published years ago. Now it's been open sourced.
</p>
<p>
The Sverdlovsk notebook stopped publishing back in 1989; it was a collection of open problems for semigroups, but it cannot be found.
</p>
<p>
Other problem notebooks might exist too, but I am unaware of them...
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0tag:blogger.com,1999:blog-3776650590176552530.post-67397326066397165402012-01-06T08:37:00.000-08:002012-01-06T08:38:37.172-08:00People don't read anymore :(<p>
I have been wandering around book stores recently, and stumbled upon the <em>Landmark Herodotus</em>. If you recall, I wrote a <a href="http://texnicalstuff.blogspot.com/search/label/Herodotus">few posts</a> on Herodotus.
</p>
<p>
People ought to be reading the text, and produce their own notes, producing a similar result (as <em>Landmark</em>) which is personalized.
</p>
<p>
Don't mistake me: I think <em>Landmark</em> is a wonderful resource! It has helped with maps, and so on...but people should be doing this on their own.
</p>
<p>
The problem <em>Landmark</em> posed (to me) parallels <em>Cliff Notes</em>. The books are produced as an example of how to take notes while reading books<b>...not a replacement for reading!</b>
</p>
<p>
Extemporaneously producing maps is an invaluable skill. The map doesn't have to be precise, e.g. drawing Asia minor as a rectangle, or Greece as three rectangles.
</p>
<p>
There are some elements to, e.g., the <em>Landmark Herodotus</em> that are pleasant, and makes it a great resource <b>to borrow from.</b> For example: what did Herodotus get wrong?
</p>
<p>
It appears that he got a lot of Egyptian history wrong, for example.
</p>
<p>
But my point is: <b>reading is studying!</b> You have to make a book <em>your own</em> through notes, maps, references to other books, etc.
</p>
<p>
<b>How</b> you study is entirely up to you; <b>how</b> you take notes, well, that is entirely up to you. But reading without taking notes is like dancing: nobody does it unless drunk or insane.
</p>
<p>
People just confuse <em>the mechanics of reading</em> (parsing letters into words) with <em>the procedure called "reading"</em> (obtaining information from books, and evaluating it). *sigh*
</p>
<p>
P.S. Happy New Year!
</p>pqnelsonhttp://www.blogger.com/profile/12779680952736168655noreply@blogger.com0