More defs

trees/base-macros.tree

@@ -12,10 +12,14 @@
    \latex-preamble/common
   }
   \tex{\get\base/tex-preamble}{
+
     \begin{minipage}{5.8in}
 
+    \vspace{0.5ex}
+
     % \setlength{\parindent}{10pt}
     \setlength{\parskip}{3ex plus 0.5ex minus 0.2ex}
+
     \body
 
     \end{minipage}

trees/uts-0002.tree

@@ -4,27 +4,10 @@
 
 \date{2024-04-26}
 
-\import{base-macros}
-
 \p{This survey is built on my notes in the process of figuring out Eric Wiesser's MathOverflow question [Definition of a spin group](https://mathoverflow.net/questions/427881/definition-of-a-spin-group) for [our PR to Mathlib4 about Spin groups](https://github.com/leanprover-community/mathlib4/pull/9111/).}
 
 \p{This is also my first [Forester experiment](uts-0003).}
 
-\minitex{
-
-\begin{definition*}[Spin group]
-
-The Pin group of $(V, q)$ is the subgroup $\operatorname{Pin}(V, q)$ of $P(V, q)$ generated by the elements $v \in V$ with $q(v) = \pm 1$.
-
-The associated spin group of $(V, q)$ is then defined by
-
-$$
-\operatorname{Spin}(V, q)=\operatorname{Pin}(V, q) \cap \mathrm{Cl}^0(V, q)
-$$
-
-\end{definition*}
-
-}
-
-\p{See [[lawson2016spin]].}
+\transclude{uts-0004}
 
+\transclude{uts-0005}

trees/uts-0003.tree

@@ -2,7 +2,7 @@
 
 \date{2024-04-27}
 
-\p{I'm experimenting using [Forester](https://www.jonmsterling.com/jms-005P.xml) for building [forests of evergreen notes](https://www.jonmsterling.com/tfmt-000V.xml).}
+\p{I'm experimenting using [Forester](https://www.jonmsterling.com/jms-005P.xml) for building [forests of evergreen notes](https://www.jonmsterling.com/tfmt-000V.xml) like [Notes on duploid theory](https://www.jonmsterling.com/jms-0047.xml).}
 
 \p{I wish to use it to organize many definitions, proofs and discussions about the same mathematical concepts/topics. This is a spiritual successor to my "Many faces of Clifford algebras" writeup.}
 

trees/uts-0004.tree

@@ -0,0 +1,18 @@
+\title{Spin group ([[lawson2016spin]])}
+\date{2024-04-27}
+
+\taxon{definition}
+
+\import{base-macros}
+
+\minitex{
+
+The Pin group of $(V, q)$ is the subgroup $\operatorname{Pin}(V, q)$ of $P(V, q)$ generated by the elements $v \in V$ with $q(v) = \pm 1$.
+
+The associated spin group of $(V, q)$ is then defined by
+
+$$
+\operatorname{Spin}(V, q)=\operatorname{Pin}(V, q) \cap \mathrm{Cl}^0(V, q)
+$$
+
+}

trees/uts-0005.tree

@@ -0,0 +1,12 @@
+\title{Spin group (The wikipedia page on Clifford Algebras)}
+\date{2024-04-27}
+
+\taxon{definition}
+
+\import{base-macros}
+
+\minitex{
+
+The pin group $\operatorname{Pin}_V(K)$ is the subgroup of the Lipschitz group $\Gamma$ of elements of spinor norm 1, and similarly the spin group $\operatorname{Spin}_V(K)$ is the subgroup of elements of Dickson invariant 0 in $\operatorname{Pin}_V(K)$.
+
+}