Add def for Spin group and even subalgebra of CA

tex/forest.bib

@@ -1354,3 +1354,30 @@ @article{riccardo2024towards
   year={2024}
 }
 
+@article{pepe2024staresnet,
+  title={STAResNet: a Network in Spacetime Algebra to solve Maxwell's PDEs},
+  author={Pepe, Alberto and Buchholz, Sven and Lasenby, Joan},
+  journal={arXiv preprint arXiv:2408.13619},
+  year={2024}
+}
+
+@article{filimoshina2024note,
+  title={A Note on Centralizers and Twisted Centralizers in Clifford Algebras},
+  author={Filimoshina, Ekaterina and Shirokov, Dmitry},
+  journal={Advances in Applied Clifford Algebras},
+  volume={34},
+  number={5},
+  pages={50},
+  year={2024},
+  publisher={Springer}
+}
+
+@inproceedings{wieser2022computing,
+  title={Computing with the Universal Properties of the Clifford Algebra and the Even Subalgebra},
+  author={Wieser, Eric and Lasenby, Joan},
+  booktitle={International Conference on Advanced Computational Applications of Geometric Algebra},
+  pages={199--211},
+  year={2022},
+  organization={Springer}
+}
+

trees/ca-001J.tree

@@ -0,0 +1,27 @@
+\import{spin-macros}
+% clifford hopf spin draft
+\tag{clifford}
+\tag{draft}
+
+% definition theorem lemma construction observation
+% convention corollary axiom example exercise proof
+% discussion remark notation
+% \taxon{}
+% \refcardt{lemma}{}{}{}{
+
+% james2001representations woit2017quantum lux2010representations sims1994computation wilson2024discrete hamilton2023supergeometric hamilton2023unification
+
+\refdef{even subalgebra of Clifford algebra}{wieser2022computing}{
+\lean{CliffordAlgebra.even}
+
+\p{
+The even subalgebra of the Clifford algebra is defined as the submodule of the Clifford algebra
+
+##{
+\Cl^{+}(Q) \equiv \left\{ x_1 \cdots x_k \in \Cl \mid x \in V, k \text{ is even} \right\}
+}
+
+which also forms a subalgebra. Its elements are called even elements, as they can be expressed as the geometric product of an even number of 1-vectors.
+
+}
+}

trees/refs/filimoshina2024note.tree

@@ -0,0 +1,18 @@
+% ["forest"]
+\title{A note on centralizers and twisted centralizers in clifford algebras}
+\date{2024}
+\author{Ekaterina Filimoshina}\author{Dmitry Shirokov}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{filimoshina2024note,
+ title = {A Note on Centralizers and Twisted Centralizers in Clifford Algebras},
+ author = {Filimoshina, Ekaterina and Shirokov, Dmitry},
+ year = {2024},
+ journal = {Advances in Applied Clifford Algebras},
+ volume = {34},
+ number = {5},
+ pages = {50},
+ publisher = {Springer}
+}
+\stopverb}

trees/refs/pepe2024staresnet.tree

@@ -0,0 +1,14 @@
+% ["forest"]
+\title{STAResNet: A network in spacetime algebra to solve maxwell’s PDEs}
+\date{2024}
+\author{Alberto Pepe}\author{Sven Buchholz}\author{Joan Lasenby}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{pepe2024staresnet,
+ title = {STAResNet: a Network in Spacetime Algebra to solve Maxwell's PDEs},
+ author = {Pepe, Alberto and Buchholz, Sven and Lasenby, Joan},
+ year = {2024},
+ journal = {arXiv preprint arXiv:2408.13619}
+}
+\stopverb}

trees/refs/wieser2022computing.tree

@@ -0,0 +1,16 @@
+% ["forest"]
+\title{Computing with the universal properties of the clifford algebra and the even subalgebra}
+\date{2022}
+\author{Eric Wieser}\author{Joan Lasenby}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@inproceedings{wieser2022computing,
+ title = {Computing with the Universal Properties of the Clifford Algebra and the Even Subalgebra},
+ author = {Wieser, Eric and Lasenby, Joan},
+ year = {2022},
+ booktitle = {International Conference on Advanced Computational Applications of Geometric Algebra},
+ pages = {199--211},
+ organization = {Springer}
+}
+\stopverb}

trees/spin-000X.tree

@@ -6,4 +6,6 @@
 
 \transclude{spin-000W}
 
-\transclude{spin-000Y}
+\transclude{spin-000Y}
+
+\transclude{spin-0012}

trees/spin-000Y.tree

@@ -1,7 +1,9 @@
 \import{spin-macros}
 
 \refdef{Pin group}{pr-spin}{
-\p{The Pin group is defined as.
+\lean{pinGroup}
+
+\p{The Pin group is defined as
 
 ##{
 \Pin(Q) \equiv \Gamma \sqcap \unitary{\Cl(Q)}
@@ -13,7 +15,7 @@ where #{\sqcap} is the [infimum (or greatest lower bound, or meet)](https://en.w
 \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}}.
+are the unitary elements of the Clifford algebra as a #{*}-monid, and we have defined the star operation of Clifford algebra as [[ca-000K]], denoted #{\conj{x}}.
 }
 
 \p{
@@ -30,4 +32,4 @@ where
 }
 
 }
-}
+}

trees/spin-0012.tree

@@ -0,0 +1,17 @@
+\import{spin-macros}
+% clifford hopf spin draft
+\tag{spin}
+
+\refdef{Spin group}{pr-spin}{
+\lean{spinGroup}
+
+\p{The Spin group is defined as
+
+##{
+\Spin(Q) \equiv \Pin(Q) \sqcap \Cl^{+}(Q)
+}
+
+where #{\Cl^{+}(Q)} is the [even subalgebra of the Clifford algebra](ca-001J).
+}
+
+}

trees/uts-0018.tree

@@ -15,6 +15,10 @@
 \subtree[2024-11]{
 \title{November, 2024}
 
+\mdblock{11-20}{
+- skimmed \citek{pepe2024staresnet} and \citek{filimoshina2024note}
+}
+
 \mdblock{11-12~11-19}{
 - experiments on using [aider](https://aider.chat/) for LLM assisted project-level pair programming
     - [this PR](https://github.com/utensil/lean4_jupyter/pull/2) is a most extensive onehttps://github.com/pygae/galgebra/pull/528