Add dutailly2018clifford, hitzer2012introduction, hahn2004clifford, p…

…orteous1995clifford, rosen2019geometric, ruhe2024clifford, gallier2014clifford, fulton2013representation, and revise lawson2016spin

new.sh

@@ -1,3 +1,5 @@
 #!/bin/bash
 TREE_PREFIX=${1:-uts}
-opam exec -- forester new --dest=trees --prefix=$TREE_PREFIX
+FILENAME=$(opam exec -- forester new --dest=trees --prefix=$TREE_PREFIX)
+echo $FILENAME
+cat templates/texdef.tree > $FILENAME

trees/refs/atiyah1964clifford.tree

@@ -0,0 +1,14 @@
+\title{Clifford modules}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{atiyah1964clifford,
+  title={Clifford modules},
+  author={Atiyah, Michael F and Bott, Raoul and Shapiro, Arnold},
+  journal={Topology},
+  volume={3},
+  pages={3--38},
+  year={1964},
+  publisher={Pergamon}
+}
+\stopverb}

trees/refs/dutailly2018clifford.tree

@@ -0,0 +1,10 @@
+\title{CLIFFORD ALGEBRAS-NEW RESULTS}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{dutailly2018clifford,
+  title={CLIFFORD ALGEBRAS-NEW RESULTS},
+  author={Dutailly, Jean Claude},
+  year={2018}
+}
+\stopverb}

trees/refs/fulton2013representation.tree

@@ -0,0 +1,12 @@
+\title{Representation theory: a first course}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@book{fulton2013representation,
+  title={Representation theory: a first course},
+  author={Fulton, William and Harris, Joe},
+  volume={129},
+  year={2013},
+  publisher={Springer Science \& Business Media}
+}
+\stopverb}

trees/refs/gallier2014clifford.tree

@@ -0,0 +1,11 @@
+\title{Clifford algebras, clifford groups, and a generalization of the quaternions}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{gallier2014clifford,
+  title={Clifford algebras, clifford groups, and a generalization of the quaternions},
+  author={Gallier, Jean},
+  journal={arXiv preprint arXiv:0805.0311},
+  year={2014}
+}
+\stopverb}

trees/refs/hahn2004clifford.tree

@@ -0,0 +1,13 @@
+\title{The Clifford Algebra in the Theory of Algebras, Quadratic Forms, and Classical Groups}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{hahn2004clifford,
+  title={The Clifford Algebra in the Theory of Algebras, Quadratic Forms, and Classical Groups},
+  author={Hahn, Alexander J},
+  journal={Clifford Algebras: Applications to Mathematics, Physics, and Engineering},
+  pages={305--322},
+  year={2004},
+  publisher={Springer}
+}
+\stopverb}

trees/refs/hitzer2012introduction.tree

@@ -0,0 +1,15 @@
+\title{Introduction to Clifford's geometric algebra}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{hitzer2012introduction,
+  title={Introduction to Clifford's geometric algebra},
+  author={Hitzer, Eckhard},
+  journal={Journal of the Society of Instrument and Control Engineers},
+  volume={51},
+  number={4},
+  pages={338--350},
+  year={2012},
+  publisher={The Society of Instrument and Control Engineers}
+}
+\stopverb}

trees/refs/porteous1995clifford.tree

@@ -0,0 +1,12 @@
+\title{Clifford algebras and the classical groups}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@book{porteous1995clifford,
+  title={Clifford algebras and the classical groups},
+  author={Porteous, Ian R},
+  number={50},
+  year={1995},
+  publisher={Cambridge University Press}
+}
+\stopverb}

trees/refs/rosen2019geometric.tree

@@ -0,0 +1,11 @@
+\title{Geometric multivector analysis}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@book{rosen2019geometric,
+  title={Geometric multivector analysis},
+  author={Ros{\'e}n, Andreas},
+  year={2019},
+  publisher={Springer}
+}
+\stopverb}

trees/refs/ruhe2024clifford.tree

@@ -0,0 +1,12 @@
+\title{Clifford group equivariant neural networks}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@article{ruhe2024clifford,
+  title={Clifford group equivariant neural networks},
+  author={Ruhe, David and Brandstetter, Johannes and Forr{\'e}, Patrick},
+  journal={Advances in Neural Information Processing Systems},
+  volume={36},
+  year={2024}
+}
+\stopverb}

trees/spin-0001.tree

@@ -4,10 +4,12 @@
 
 \date{2024-04-26}
 
-\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/). It's a work-in-progress.}
+\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 [[uts-0002]].}
 
+\p{Now it's a work-in-progress. Definitions coming from different sources simply quoted here with minimal modifications, to include immediate prerequisites, and omit some discussions or theorems. Definitions that are too similar are not yet pruned. And the order is quite arbitrary at the moment.}
+
 \transclude{spin-0002}
 
 \transclude{spin-0003}
@@ -36,4 +38,20 @@
 
 \transclude{spin-000F}
 
-\transclude{spin-000G}
+\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}

trees/spin-0002.tree

@@ -1,11 +1,29 @@
 \import{base-macros}
 
 \texdef{Spin group}{lawson2016spin}{
-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
+Let $V$ be a vector space over the commutative field $k$ and suppose $q$ is a quadratic form on $V$.
 
+We now consider the multiplicative group of units in the Clifford algebra $C \ell(V, q)$ associated to $V$, which is defined to be the subset
 $$
-\operatorname{Spin}(V, q)=\operatorname{Pin}(V, q) \cap \mathrm{Cl}^0(V, q)
+C \ell^{\times}(V, q) \equiv\left\{\varphi \in C \ell(V, q): \exists \varphi^{-1} \text { with } \varphi^{-1} \varphi=\varphi \varphi^{-1}=1\right\}
+$$
+
+This group contains all elements $v \in V$ with $q(v) \neq 0$.
+
+The group of units always acts naturally as automorphisms of the algebra. That is, there is a homomorphism
+$$
+\mathrm{Ad}: \mathrm{C} \ell^{\times}(V, q) \longrightarrow \operatorname{Aut}(\mathrm{C} \ell(V, q))
+$$
+called the adjoint representation, which is given by
+$$
+\operatorname{Ad}_{\varphi}(x) \equiv \varphi \times \varphi^{-1}
+$$
+
+The Pin group of $(V, q)$ is the subgroup $\operatorname{Pin}(V, q)$ of $\mathrm{P}(V, q)$ generated by the elements $v \in V$ with $q(v)= \pm 1$.
+
+The associated Spin group of $(V, q)$ is defined by
+$$
+\operatorname{Spin}(V, q)=\operatorname{Pin}(V, q) \cap C \ell^0(V, q) .
 $$
 }

trees/spin-000H.tree

@@ -0,0 +1,9 @@
+\import{base-macros}
+
+\texdef{Spin group}{dutailly2018clifford}{
+The Spin group $\operatorname{Spin}(F, \rho)$ of $C l(F, \rho)$ is the subset of $C l(F, \rho)$ whose elements can be written as the product $g=u_1 \cdot \ldots \cdot u_{2 p}$ of an even number of vectors of $F$ of norm $\left\langle u_k, u_k\right\rangle=1$.
+
+As a consequence : $\langle g, g\rangle=1, g^t \cdot g=1$ and $\operatorname{Spin}(F, \rho) \subset O(C l)$.
+
+The scalars $\pm 1$ belong to the Spin group. The identity is $+1 . \operatorname{Spin}(F, \rho)$ is a connected Lie group.
+}

trees/spin-000I.tree

@@ -0,0 +1,39 @@
+\import{base-macros}
+
+\texdef{Spin group}{hitzer2012introduction}{
+
+A versor refers to a Clifford monomial (product expression) composed of invertible vectors. It is called a rotor, or spinor, if the number of vectors is even. It is called a unit versor if its magnitude is 1.
+
+Every versor $A=a_1 \ldots a_r, \quad a_1, \ldots, a_r \in \mathbb{R}^2, r \in \mathbb{N}$ has an inverse
+$$
+A^{-1}=a_r^{-1} \ldots a_1^{-1}=a_r \ldots a_1 /\left(a_1^2 \ldots a_r^2\right),
+$$
+such that
+$$
+A A^{-1}=A^{-1} A=1 .
+$$
+
+This makes the set of all versors in $C l(2,0)$ a group, the so called Lipschitz group with symbol $\Gamma(2,0)$, also called Clifford group or versor group. Versor transformations apply via outermorphisms to all elements of a Clifford algebra. It is the group of all reflections and rotations of $\mathbb{R}^2$.
+
+The normalized subgroup of versors is called pin group
+$$
+\operatorname{Pin}(2,0)=\{A \in \Gamma(2,0) \mid A \widetilde{A}= \pm 1\} .
+$$
+
+In the case of $C l(2,0)$ we have
+$$
+\begin{aligned}
+& \operatorname{Pin}(2,0) \\
+& =\left\{a \in \mathbb{R}^2 \mid a^2=1\right\} \cup\left\{A \mid A=\cos \varphi+e_{12} \sin \varphi, \varphi \in \mathbb{R}\right\} .
+\end{aligned}
+$$
+
+The pin group has an even subgroup, called spin group
+$$
+\operatorname{Spin}(2,0)=\operatorname{Pin}(2,0) \cap C l^{+}(2,0) .
+$$
+
+The spin group has in general a spin plus subgroup
+
+$$\operatorname{Spin}_{+}(2,0)=\{A \in \operatorname{Spin}(2,0) \mid A \widetilde{A}=+1\}.$$
+}

trees/spin-000J.tree

@@ -0,0 +1,24 @@
+\import{base-macros}
+
+\texdef{Spin group}{hahn2004clifford}{
+We continue to let $F$ be a field of characteristic not 2 and $M$ a quadratic space over $F$.
+
+Recall that $\gamma: M \rightarrow C(M)$ is injective and that there is a unique involution - on $C(M)$ taking $\gamma x$ to $\gamma x$ for all $x$. Consider $M$ to be a subset of $C(M)$ via $\gamma$, and define the group $\operatorname{Spin}_{\infty}(M)$ by
+$$
+\operatorname{Spin}_{\infty}(M)=\left\{c \in C_0(M)^{\times} \mid c M c^{-1}=M, c \bar{c}=1_C\right\},
+$$
+
+where $C_0(M)^{\times}$is the group of invertible elements of the $\operatorname{ring} C_0(M)$. The isometries from $M$ onto $M$ constitute the orthogonal group $O(M)$ and $S O(M)$ is the subgroup of elements of determinant 1. For $c$ in $\operatorname{Spin}(M)$, define
+$$
+\pi c: M \rightarrow M
+$$
+by $\pi c(x)=c x c^{-1}$. This provides a homomorphism
+$$
+\pi: \operatorname{Spin}(M) \rightarrow S O(M) .
+$$
+
+By a theorem of Cartan and Dieudonné, any element $\sigma$ in $O(M)$ is a product $\sigma=\tau_{y_1} \cdots \tau_{y_k}$ of hyperplane reflections $\tau_{y_i}$. The assignment $\Theta(\sigma)=$ $q\left(y_1\right) \cdots q\left(y_k\right)\left(F^{\times}\right)^2$ defines the spinor norm homomorphism
+$$
+\Theta: S O(M) \rightarrow F^{\times} /\left(F^{\times}\right)^2 .
+$$
+}

trees/spin-000K.tree

@@ -0,0 +1,28 @@
+\import{base-macros}
+
+\texdef{Spin group}{porteous1995clifford}{
+Let $g$ be an invertible element of a universal Clifford algebra $A$ such that, for each $x \in X, g x \widehat{g}^{-1} \in X$. Then the map
+$$
+\rho_{X, g}: x \mapsto g x \widehat{g}^{-1}
+$$
+is an orthogonal automorphism of $X$.
+
+The element $g$ will be said to induce or represent the orthogonal transformation $\rho_{X, g}$ and the set of all such elements $g$ will be denoted by $\Gamma(X)$ or simply by $\Gamma$.
+
+The subset $\Gamma$ is a subgroup of $A$.
+
+The group $\Gamma$ is called the Clifford group (or Lipschitz group) for $X$ in the Clifford algebra $A$. Since the universal algebra $A$ is uniquely defined up to isomorphism, $\Gamma$ is also uniquely defined up to isomorphism.
+
+An element $g$ of $\Gamma(X)$ represents a rotation of $X$ if and only if $g$ is the product of an even number of elements of $X$. The set of such elements will be denoted by $\Gamma^0=\Gamma^0(X)$. An element $g$ of $\Gamma$ represents an anti-rotation of $X$ if and only if $g$ is the product of an odd number of elements of $X$. The set of such elements will be denoted by $\Gamma^1=\Gamma^1(X)$. Clearly, $\Gamma^0=\Gamma \cap A^0$ is a subgroup of $\Gamma$, while $\Gamma^1=\Gamma \cap A^1$.
+
+The Clifford group $\Gamma(X)$ of a quadratic space $X$ is larger than is necessary if our interest is in representing orthogonal transformations of $X$. Use of a quadratic norm $N$ on the Clifford algebra $A$ leads to the definition of subgroups of $\Gamma$ that are less redundant for this purpose. This quadratic norm $N: A \rightarrow A$ is defined by the formula
+$$
+N(a)=a^{-} a, \text { for any } a \in A,
+$$
+
+For $X$ and $\Gamma=\Gamma(X)$ as above we now define
+$$
+\operatorname{Pin} X=\{g \in \Gamma:|N(g)|=1\} \text { and } \operatorname{Spin} X=\left\{g \in \Gamma^0:|N(g)|=1\right\} \text {. }
+$$
+
+}

trees/spin-000L.tree

@@ -0,0 +1,27 @@
+\import{base-macros}
+
+\texdef{Spin group}{rosen2019geometric}{
+Let $V$ be an inner product space. We denote by $\Delta V$ the standard Clifford algebra $(\wedge V,+, \Delta)$ defined by the Clifford product $\Delta$ on the space of multivectors in $V$.
+
+Let $V$ be an inner product space. The Clifford cone of $V$ is the multiplicative group $\widehat{\triangle} V \subset \triangle V$ generated by nonsingular vectors, that is, vectors $v$ such that $\langle v\rangle^2 \neq 0$. More precisely, $q \in \widehat{\triangle} V$ if there are finitely many nonsingular vectors $v_1, \ldots, v_k \in V$ such that
+$$
+q=v_1 \Delta \cdots \Delta v_k .
+$$
+
+Let $w \in \triangle V$. Then $w \in \widehat{\triangle} V$ if and only if $w$ is invertible and
+$\widehat{w} v w^{-1} \in V$ for all $v \in V$.
+
+In this case $w$ can be written as a product of at most $\operatorname{dim} V$ nonsingular vectors, and $\bar{w} w=w \bar{w} \in \mathbf{R} \backslash\{0\}$.
+
+Let $V$ be an inner product space. Define the orthogonal, special orthogonal, pin, and spin groups
+$$
+\begin{aligned}
+\mathrm{O}(V) & :=\{\text { isometries } T: V \rightarrow V\} \subset \mathcal{L}(V), \\
+\mathrm{SO}(V) & :=\{T \in \mathrm{O}(V) ; \operatorname{det} T=+1\} \subset \mathcal{L}(V), \\
+\operatorname{Pin}(V) & :=\left\{q \in \widehat{\triangle} V ;\langle q\rangle^2= \pm 1\right\} \subset \triangle V, \\
+\operatorname{Spin}(V) & :=\left\{q \in \operatorname{Pin}(V) ; q \in \triangle^{\mathrm{ev}} V\right\} \subset \triangle^{\mathrm{ev}} V .
+\end{aligned}
+$$
+
+We call $T \in \operatorname{SO}(V)$ a rotation and we call $q \in \operatorname{Spin}(V)$ a rotor.
+}

trees/spin-000M.tree

@@ -0,0 +1,40 @@
+\import{base-macros}
+
+\texdef{Spin group}{ruhe2024clifford}{
+
+Motivation E. 39 (The problem of generalizing the definition of the Spin group). For a positive definite quadratic form $\mathfrak{q}$ on the real vector space $V=\mathbb{R}^n$ with $n \geq 3$ the $\operatorname{Spin}$ group $\operatorname{Spin}(n)$ is defined via the kernel of the Spinor norm (=extended quadratic form on $\mathrm{Cl}(V, \mathfrak{q})$ ) restricted to the special Clifford group $\Gamma^{[0]}(V, \mathfrak{q})$ :
+$$
+\operatorname{Spin}(n):=\operatorname{ker}\left(\overline{\mathfrak{q}}: \Gamma^{[0]}(V, \mathfrak{q}) \rightarrow \mathbb{R}^{\times}\right)=\left\{w \in \Gamma^{[0]}(V, \mathfrak{q}) \mid \overline{\mathfrak{q}}(w)=1\right\}=\left.\overline{\mathfrak{q}}\right|_{\Gamma^{[0]}(V, \mathfrak{q})} ^{-1}(1) .
+$$
+$\operatorname{Spin}(n)$ is thus a normal subgroup of the special Clifford group $\Gamma^{[0]}(V, \mathfrak{q})$, and, as it turns out, a double cover of the special orthogonal group $\mathrm{SO}(n)$ via the twisted conjugation $\rho$. The latter can be summarized by the short exact sequence:
+$$
+1 \longrightarrow\{ \pm 1\} \xrightarrow{\text { incl }} \operatorname{Spin}(n) \xrightarrow{\rho} \mathrm{SO}(n) \longrightarrow 1 .
+$$
+
+We intend to generalize this in several directions: 1. from Spin to Pin group, 2. from $\mathbb{R}^n$ to vector spaces $V$ over general fields $\mathbb{F}$ with $\operatorname{ch}(\mathbb{F}) \neq 2$, 3. from non-degenerate to degenerate quadratic forms $\mathfrak{q}$, 4. from positive (semi-)definite to non-definite quadratic forms $\mathfrak{q}$. This comes with several challenges and ambiguities.
+
+Definition E. 40 (The real Pin group and the real Spin group). Let $V$ be a finite dimensional $\mathbb{R}$-vector space $V, \operatorname{dim} V=n<\infty$, and $\mathfrak{q} a$ (possibly degenerate) quadratic form on $V$. We define the (real) Pin group and (real) Spin group, resp., of $(V, \mathfrak{q})$ as the following subquotients of the Clifford group. $\Gamma(V, \mathfrak{q})$ and its even parity part $\Gamma^{[0]}(V, \mathfrak{q})$, resp.:
+$$
+\begin{aligned}
+\operatorname{Pin}(V, \mathfrak{q}) & :=\{x \in \Gamma(V, \mathfrak{q}) \mid \overline{\mathfrak{q}}(x) \in\{ \pm 1\}\} / \bigwedge^{[*]}(\mathcal{R}) \\
+\operatorname{Spin}_{\infty}(V, \mathfrak{q}) & :=\left\{x \in \Gamma^{[0]}(V, \mathfrak{q}) \mid \overline{\mathfrak{q}}(x) \in\{ \pm 1\}\right\} / \bigwedge^{[*]}(\mathcal{R})
+\end{aligned}
+$$
+
+Corollary E.41. Let $(V, \mathfrak{q})$ be a finite dimensional quadratic vector space over $\mathbb{R}$. Then the twisted conjugation induces a well-defined and surjective group homomorphism onto the group of radical preserving orthogonal automorphisms of $(V, \mathfrak{q})$ :
+$$
+\rho: \operatorname{Pin}(V, \mathfrak{q}) \rightarrow \mathrm{O}_{\mathcal{R}}(V, \mathfrak{q}),
+$$
+with kernel:
+$$
+\operatorname{ker}\left(\rho: \underset{\sim \text { in }}{\operatorname{Pin}}(V, \mathfrak{q}) \rightarrow \mathrm{O}_{\mathcal{R}}(V, \mathfrak{q})\right)=\{ \pm 1\} .
+$$
+
+Correspondingly, for the $\operatorname{Spin}(V, \mathfrak{q})$ group. In short, we have short exact sequences:
+$$
+\begin{aligned}
+& 1 \longrightarrow\{ \pm 1\} \xrightarrow{\text { incl }} \operatorname{Pin}(V, \mathfrak{q}) \xrightarrow{\rho} \mathrm{O}_{\mathcal{R}}(V, \mathfrak{q}) \longrightarrow 1, \\
+& 1 \longrightarrow\{ \pm 1\} \xrightarrow{\text { incl }} \operatorname{Spin}(V, \mathfrak{q}) \xrightarrow{\rho} \operatorname{SO}_{\mathcal{R}}(V, \mathfrak{q}) \longrightarrow 1 .
+\end{aligned}
+$$
+}