Add Clifford algebra, Lipschitz-Clifford group, Pin group, Kronecker …

…delta, and reorganize things a bit

assets/uts-style.css

@@ -34,4 +34,19 @@ body {
     /* content: "\21A0"; */
     /* content: "\2192"; */
     /* content: "⧉"; */
-}
+}
+
+nav#toc a.link.local,
+nav#toc .link.local a,
+nav#toc a.slug {
+    font-size: 80%;
+    box-shadow: none;
+    text-decoration-line: underline;
+    text-decoration-style: dotted;
+    color: rgb(132, 132, 132);
+}
+
+/* article {
+    line-break: strict;
+    word-break: keep-all;
+} */

build.sh

@@ -2,8 +2,6 @@
 
 echo
 echo "Rebuilding forest"
-rm -rf build
-rm -rf output
 time opam exec -- forester build # --dev
 echo
 # if return code is zero, then echo "Done" else echo "Failed"

fize.sh

@@ -7,7 +7,9 @@ TREE="trees/$1.tree"
 # for the file $TREE, replace all string matching regrex \$([^$]+)\$ to #{$1} where $1 is the first match using sed inplace
 sed -i '' -E 's/\$([^$]+)\$/#{\1}/g' $TREE
 # for the file $TREE, replace all string matching regrex \$\$\n([^$]+)\$\$ to ##{$1} where $1 is the first match using sed inplace
-cat $TREE | tr '\n' '\r' | sed -E 's/\$\$(\r[^$]+)\$\$/##{\1}/g' > $TREE.tmp
+cat $TREE | tr '\n' '\r' | sed -E 's/\$\$([^$]+)\$\$/##{\1}/g' > $TREE.tmp
+# for the file $TREE.tmp, replace all string matching \r(.*)\r\r to \r\p{\1}\r\r where $1 is the first match using sed inplace
+# sed -i '' -E 's/\r(.*)\r\r/\p{\r\1\r}\r\r/g' $TREE.tmp
 cat $TREE.tmp | tr '\r' '\n' > $TREE
 rm $TREE.tmp
 # for the file $TREE, replace all string \( to #{ using sed inplace

trees/ca-0002.tree

@@ -0,0 +1,20 @@
+% clifford hopf spin
+\tag{clifford}
+
+\import{spin-macros}
+
+\refdef{Clifford algebra}{pr-spin}{
+\p{Let #{M} be a module over a commutative ring #{R}, equipped with a quadratic form #{Q: M \to R}.}
+
+\p{A Clifford algebra over #{Q} is
+##{
+\Cl(Q)  \equiv T(M)/I_Q
+}
+where #{T(M)} is the tensor algebra of #{M}, #{I_Q} is the two-sided ideal generated from the set
+##{
+\{ m \otimes m - Q(m) \mid m \in M \}.
+}}
+
+\p{We denote the canonical linear map #{M \to \Cl(Q)} as #{\iota_Q}.}
+}
+

trees/ca-X001.tree

@@ -0,0 +1,25 @@
+\import{macros}
+% clifford hopf spin
+\tag{clifford}
+
+% definition theorem lemma construction observation
+% convention corollary axiom example exercise proof
+% discussion remark
+\taxon{definition}
+\refnote{Kronecker delta}{wiki-dirac-matrices}{
+\p{
+Kronecker delta
+##{\delta_{i j}= \begin{cases}0 & \text { if } i \neq j \\ 1 & \text { if } i=j\end{cases}}
+or with use of [Iverson bracket](https://en.wikipedia.org/wiki/Iverson_bracket):
+##{
+\delta_{i j}=[i=j] .
+}
+where #{[P]} is defined as:
+##{
+[P]=\begin{cases}1 & \text { if } P \text { is true } \\ 0 & \text { if } P \text { is false }\end{cases}
+}
+}
+
+\p{In Lean 4, the Kronecker delta [could be defined as](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/kronecker.20symbol):}
+\code{def δ (i j : I) : R := (Pi.single i 1 : _ → R) j}
+}

trees/macros.tree

@@ -173,7 +173,7 @@ so the text size almost matches the size output by native forester code. This do
   \tex{\get\base/tex-preamble}{
     % \begin{minipage}{5.8in}\texstrip
     \begin{minipage}{0.97\textwidth}\texstrip
-    \vspace{0.5ex}\texstrip
+    \vspace{4ex}\texstrip
     \setlength{\parskip}{3ex plus 0.5ex minus 0.2ex}\texstrip
     \body
     \end{minipage}\texstrip

trees/refs/joot2016exploring2.tree

@@ -0,0 +1,11 @@
+\title{Exploring physics with Geometric Algebra, book II}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@misc{joot2016exploring2,
+  title={Exploring physics with Geometric Algebra, book II},
+  author={Joot, Peeter},
+  year={2016},
+  url={https://peeterjoot.com/archives/math2015/gabookII.pdf}
+}
+\stopverb}

trees/refs/wiki-dirac-matrices.tree

@@ -0,0 +1,3 @@
+\import{macros}
+
+\wikiref{Dirac matrices}{dirac-matrices}{Gamma_matrices}

trees/spin-0001.tree

@@ -12,80 +12,18 @@
 
 \transclude{spin-000R}
 
-\transclude{spin-000S}
+% \transclude{spin-000S}
 
-\block{Classifying existing definitions}{
+% \block{Classifying existing definitions}{
 
-\p{TODO:}
+% \p{TODO:}
 
-\ul{
-    \li{classify them by the prerequisites, style, and similarity}
-}
+% \ul{
+%     \li{classify them by the prerequisites, style, and similarity}
+% }
 
-}
+% }
 
-\block{Our definition}{
+\transclude{spin-000X}
 
-\transclude{spin-000V}
-
-}
-
-\block{Appendix: Various definitions of Spin group}{
-
-\p{Definitions coming from different sources are simply quoted here with minimal modifications, to include immediate prerequisites, and omit some discussions or theorems. Definitions that are too similar are not pruned. The order is quite arbitrary.}
-
-\transclude{spin-0002}
-
-\transclude{spin-0003}
-
-\transclude{spin-0004}
-
-\transclude{spin-0005}
-
-\transclude{spin-0006}
-
-\transclude{spin-0007}
-
-\transclude{spin-0008}
-
-\transclude{spin-0009}
-
-\transclude{spin-000A}
-
-\transclude{spin-000B}
-
-\transclude{spin-000C}
-
-\transclude{spin-000D}
-
-\transclude{spin-000E}
-
-\transclude{spin-000F}
-
-\transclude{spin-000G}
-
-\transclude{spin-000H}
-
-\transclude{spin-000I}
-
-\transclude{spin-000J}
-
-\transclude{spin-000K}
-
-\transclude{spin-000L}
-
-\transclude{spin-000M}
-
-\transclude{spin-000N}
-
-\transclude{spin-000O}
-
-\transclude{spin-000P}
-
-\transclude{spin-000Q}
-
-\transclude{spin-000T}
-
-\transclude{spin-000U}
-
-}
+\transclude{spin-000Z}

trees/spin-000R.tree

@@ -4,4 +4,4 @@
 
 \p{This survey is built on my notes in the process of figuring out [[ericwieser]]'s MathOverflow question [Definition of a spin group](https://mathoverflow.net/questions/427881/definition-of-a-spin-group) for [our PR](https://github.com/leanprover-community/mathlib4/pull/9111/) to Lean 4's Mathlib about Spin groups.}
 
-\p{This is my first [[uts-0001]], also a spiritual successor to my [The Many Faces of Geometric Algebra](https://github.com/pygae/lean-ga/blob/master/docs/misc/many_faces.md) writeup.}
+\p{This is my first [[uts-0001]], also a spiritual successor to my writeup [The Many Faces of Geometric Algebra](https://github.com/pygae/lean-ga/blob/master/docs/misc/many_faces.md).}

trees/spin-000W.tree

@@ -0,0 +1,26 @@
+\import{spin-macros}
+
+\refdef{Lipschitz-Clifford group}{pr-spin}{
+
+\p{The Lipschitz-Clifford group is defined as the subgroup closure of all the invertible elements in the form of #{\iota_Q(m)},
+
+##{
+\Gamma \equiv \left\{ x_1 \ldots x_k \in \Cl^{\times}(Q) \mid x_i \in V \right\}
+}
+
+where
+
+##{
+\Cl^{\times}(Q) \equiv \left\{ x \in \Cl(Q) \mid \exists x^{-1} \in \Cl(Q), x^{-1} x = x x^{-1}=1\right\}
+}
+
+is the group of units (i.e. invertible elements) of #{\Cl(Q)},
+
+##{
+V \equiv \left\{ \iota_Q(m) \in \Cl(Q) \mid m \in M \right\}
+}
+
+is the subset #{V} of #{\Cl(Q)} in the form of #{\iota_Q(m)}.
+}
+
+}

trees/spin-000X.tree

@@ -0,0 +1,9 @@
+\import{macros}
+
+\title{Our definition}
+
+\transclude{ca-0002}
+
+\transclude{spin-000W}
+
+\transclude{spin-000Y}

trees/spin-000Y.tree

@@ -0,0 +1,33 @@
+\import{spin-macros}
+
+\refdef{Pin group}{pr-spin}{
+\p{The Pin group is defined as.
+
+##{
+\Pin(Q) \equiv \Gamma \sqcap \unitary{\Cl(Q)}
+}
+
+where #{\sqcap} is the [infimum (or greatest lower bound, or meet)](https://en.wikipedia.org/wiki/Infimum_and_supremum), and the infimum of two submonoids is just their intersection #{\cap},
+
+##{
+\unitary{S} \equiv \left\{ x \in S \mid \star{x} * x = x * \star{x} = 1 \right\}
+}
+
+are the unitary elements of the Clifford algebra as a #{*}-monid, and we have defined the star operation of Clifford algebra as the [Clifford conjugate](https://utensil.github.io/lean-ga/blueprint/sec-ops.html#conjugate), denoted #{\conj{x}}.
+}
+
+\p{
+This definition is equivalent to the following:
+
+##{
+\Pin(Q)  \equiv \left\{ x \in \Gamma \mid \norm{x} = 1 \right\}
+}
+
+where
+
+##{
+\norm{x} \equiv x \conj{x}.
+}
+
+}
+}

trees/spin-000Z.tree

@@ -0,0 +1,60 @@
+\import{spin-macros}
+\title{Appendix: Many faces of Spin group}
+
+\p{Definitions coming from different sources are simply quoted here with minimal modifications, to include immediate prerequisites, and omit some discussions or theorems.}
+
+\p{They are not classified, ordered, or pruned by similarity.}
+
+\transclude{spin-0002}
+
+\transclude{spin-0003}
+
+\transclude{spin-0004}
+
+\transclude{spin-0005}
+
+\transclude{spin-0006}
+
+\transclude{spin-0007}
+
+\transclude{spin-0008}
+
+\transclude{spin-0009}
+
+\transclude{spin-000A}
+
+\transclude{spin-000B}
+
+\transclude{spin-000C}
+
+\transclude{spin-000D}
+
+\transclude{spin-000E}
+
+\transclude{spin-000F}
+
+\transclude{spin-000G}
+
+\transclude{spin-000H}
+
+\transclude{spin-000I}
+
+\transclude{spin-000J}
+
+\transclude{spin-000K}
+
+\transclude{spin-000L}
+
+\transclude{spin-000M}
+
+\transclude{spin-000N}
+
+\transclude{spin-000O}
+
+\transclude{spin-000P}
+
+\transclude{spin-000Q}
+
+\transclude{spin-000T}
+
+\transclude{spin-000U}