diff --git a/assets/uts-style.css b/assets/uts-style.css index 2fcc0ff..244347e 100644 --- a/assets/uts-style.css +++ b/assets/uts-style.css @@ -34,4 +34,19 @@ body { /* content: "\21A0"; */ /* content: "\2192"; */ /* content: "⧉"; */ -} \ No newline at end of file +} + +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; +} */ \ No newline at end of file diff --git a/build.sh b/build.sh index d217e00..c71980f 100755 --- a/build.sh +++ b/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" diff --git a/fize.sh b/fize.sh index 3b7a768..6f20115 100755 --- a/fize.sh +++ b/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 diff --git a/trees/ca-0002.tree b/trees/ca-0002.tree new file mode 100644 index 0000000..739fd34 --- /dev/null +++ b/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}.} +} + diff --git a/trees/ca-X001.tree b/trees/ca-X001.tree new file mode 100644 index 0000000..6099828 --- /dev/null +++ b/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} +} diff --git a/trees/macros.tree b/trees/macros.tree index 7ccbcb9..a392bc9 100644 --- a/trees/macros.tree +++ b/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 diff --git a/trees/refs/joot2016exploring2.tree b/trees/refs/joot2016exploring2.tree new file mode 100644 index 0000000..e2a40ba --- /dev/null +++ b/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} \ No newline at end of file diff --git a/trees/refs/wiki-dirac-matrices.tree b/trees/refs/wiki-dirac-matrices.tree new file mode 100644 index 0000000..86afaef --- /dev/null +++ b/trees/refs/wiki-dirac-matrices.tree @@ -0,0 +1,3 @@ +\import{macros} + +\wikiref{Dirac matrices}{dirac-matrices}{Gamma_matrices} \ No newline at end of file diff --git a/trees/spin-0001.tree b/trees/spin-0001.tree index c391c81..63bddd9 100644 --- a/trees/spin-0001.tree +++ b/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} - -} \ No newline at end of file +\transclude{spin-000Z} \ No newline at end of file diff --git a/trees/spin-000R.tree b/trees/spin-000R.tree index 394aef1..ab451d1 100644 --- a/trees/spin-000R.tree +++ b/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).} diff --git a/trees/spin-000V.tree b/trees/spin-000V.tree deleted file mode 100644 index c9b25ef..0000000 --- a/trees/spin-000V.tree +++ /dev/null @@ -1,40 +0,0 @@ -\import{macros} - -\texdef{Spin group}{pr-spin}{ - -% TODO -\def\Cl{\mathcal{C}\kern-2pt\ell} - -Let $M$ be a module over a commutative ring $R$, equipped with a quadratic form $Q: M \to R$. - -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 \}. -$$ - -We then have the group of units (i.e. invertible elements) of $\Cl(Q)$, - -$$ -\Cl^{\times}(Q) \equiv \left\{ x \in \Cl(Q) \mid \exists x^{-1} \in \Cl(Q), x^{-1} x = x x^{-1}=1\right\} -$$ - -and the subset $V$ of $\Cl(Q)$ in the form of $\iota_Q(m)$, - -$$ -V \equiv \left\{ \iota_Q(m) \in \Cl(Q) \mid m \in M \right\} -$$ - -where $\iota_Q$ is the canonical linear map $M \to \Cl(Q)$. - -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\} -$$ - -} - diff --git a/trees/spin-000W.tree b/trees/spin-000W.tree new file mode 100644 index 0000000..0b8a995 --- /dev/null +++ b/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)}. +} + +} diff --git a/trees/spin-000X.tree b/trees/spin-000X.tree new file mode 100644 index 0000000..00a5cf4 --- /dev/null +++ b/trees/spin-000X.tree @@ -0,0 +1,9 @@ +\import{macros} + +\title{Our definition} + +\transclude{ca-0002} + +\transclude{spin-000W} + +\transclude{spin-000Y} \ No newline at end of file diff --git a/trees/spin-000Y.tree b/trees/spin-000Y.tree new file mode 100644 index 0000000..1695c88 --- /dev/null +++ b/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}. +} + +} +} \ No newline at end of file diff --git a/trees/spin-000Z.tree b/trees/spin-000Z.tree new file mode 100644 index 0000000..23b3891 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/trees/spin-macros.tree b/trees/spin-macros.tree new file mode 100644 index 0000000..2f2eb0d --- /dev/null +++ b/trees/spin-macros.tree @@ -0,0 +1,22 @@ +\export{macros} +% clifford hopf spin +% \tag{} + +% definition theorem lemma construction observation +% convention corollary axiom example exercise proof +% discussion remark +% \taxon{} + +\def\Cl{\mathcal{C}\kern-2pt\ell} + +\def\Pin{\operatorname{Pin}} + +\def\Spin{\operatorname{Spin}} + +\def\unitary[x]{\operatorname{U}(\x)} + +\def\star[x]{\x^{*}} + +\def\norm[x]{\operatorname{N}(\x)} + +\def\conj[x]{\bar{\x}} diff --git a/watch.sh b/watch.sh index 5b8e6f9..adc11a9 100755 --- a/watch.sh +++ b/watch.sh @@ -1,8 +1,10 @@ #!/bin/bash +rm -rf build +rm -rf output ./build.sh -fswatch -o trees/ assets/ | while read num ; \ +fswatch -l 200 -o trees/ assets/ | while read num ; \ do \ ./build.sh done