feat(ca): add operations

.vscode/settings.json

@@ -3,6 +3,7 @@
   "explorer.excludeGitIgnore": false,
   "latex-workshop.latex.autoBuild.run": "never",
   "conventionalCommits.scopes": [
-    "style"
+    "style",
+    "ca"
   ],
 }

fize.sh

@@ -17,8 +17,9 @@ sed -i '' -E 's/\$([^$]+)\$/#{\1}/g' $TREE
 cat $TREE | tr '\n' '\r' | sed -E 's/\$\$([^$]+)\$\$/##{\1}/g' > $TREE.tmp
 # 1. \texdef{}{}{ -> \refdef{}{}{\r\\p{
 sed -i '' -E 's/\\texdef\{([^\}]*)\}\{([^\}]*)\}\{/\\refdef\{\1\}\{\2\}\{\n\\p\{/g' $TREE.tmp
+sed -i '' -E 's/\\texnote\{([^\}]*)\}\{([^\}]*)\}\{/\\refnote\{\1\}\{\2\}\{\n\\p\{/g' $TREE.tmp
 # 2. before the line containing \refdef, skip; after the line, replace \r\r -> }\r\r\\p{ 
-awk 'BEGIN {skip=1} {if ($0 ~ /\\refdef/) {skip=0;print $0} else if (skip==1) {print $0} else { gsub(/\r\r/,"}\r\r\\p{", $0); print $0} }' $TREE.tmp > $TREE.tmp2
+awk 'BEGIN {skip=1} {if ($0 ~ /\\(refdef|refnote)/) {skip=0;print $0} else if (skip==1) {print $0} else { gsub(/\r\r/,"}\r\r\\p{", $0); print $0} }' $TREE.tmp > $TREE.tmp2
 # 3. }\s*$ -> }}
 sed -i '' -E 's/\}\s*$/\}\}\r/g' $TREE.tmp2
 cat $TREE.tmp2 | tr '\r' '\n' > $TREE
@@ -32,5 +33,5 @@ sed -i '' -E 's/\\\[/##\{/g' $TREE
 # for the file $TREE, replace all string \] to } using sed inplace
 sed -i '' -E 's/\\\]/}/g' $TREE
 # for the file $TREE, replace \texdef to \refdef using sed inplace
-sed -i '' -E 's/\\texdef/\\refdef/g' $TREE
+# sed -i '' -E 's/\\texdef/\\refdef/g' $TREE
 

tex/preamble.tex

@@ -100,6 +100,7 @@
 	roundcorner = 10pt,
 	linewidth=1pt,
 	skipabove=4ex,
+	innertopmargin=4ex,
 	innerbottommargin=9pt,
 	skipbelow=2pt,
 	nobreak=true,
@@ -202,6 +203,7 @@
 % \newtheorem{claim}[theorem]{Claim}
 % \newtheorem{definition}[theorem]{Definition}
 \declaretheorem[style=def,name=Definition,sibling=theorem]{definition}
+\declaretheorem[style=def,name=Convention,sibling=theorem]{convention}
 % \newtheorem{fact}[theorem]{Fact}
 % \newtheorem{abuse}[theorem]{Abuse of Notation}
 

trees/ca-0001.tree

@@ -33,4 +33,6 @@
 
 \block{Clifford Algebra}{
   \transclude{ca-000F}
+
+  \transclude{ca-000G}
 }

trees/ca-0009.tree

@@ -1,6 +1,6 @@
 \import{spin-macros}
 % clifford hopf spin draft
-\tag{draft}
+\tag{clifford}
 
 % definition theorem lemma construction observation
 % convention corollary axiom example exercise proof

trees/ca-000C.tree

@@ -8,8 +8,8 @@
 % \taxon{}
 % \texnote{}{}{
 % }
-
-\refdef{Universal property}{wieser2022formalizing}{
+\taxon{theorem}
+\refnote{Universal property}{wieser2022formalizing}{
 \p{
   \label{univ}
   \lean{CliffordAlgebra.ι_comp_lift, CliffordAlgebra.lift_unique}

trees/ca-000G.tree

@@ -0,0 +1,14 @@
+\import{spin-macros}
+% clifford hopf spin draft
+\tag{clifford}
+
+\parent{ca-0001}
+\title{Operations}
+
+\transclude{ca-000H}
+
+\transclude{ca-000I}
+
+\transclude{ca-000J}
+
+\transclude{ca-000K}

trees/ca-000H.tree

@@ -0,0 +1,15 @@
+\import{spin-macros}
+% clifford hopf spin draft
+\tag{clifford}
+
+% definition theorem lemma construction observation
+% convention corollary axiom example exercise proof
+% discussion remark
+\taxon{convention}
+\refnote{ }{wieser2022formalizing}{
+\p{
+Same as the previous section, let #{M} be a module over a commutative ring #{R}, equipped with a quadratic form #{Q: M \to R}.}
+
+\p{We also use #{m} or #{m_1, m_2, \dots} to denote elements of #{M}, i.e. vectors, and #{x, y, z} to denote elements of #{\Cl(Q)}.
+}}
+

trees/ca-000I.tree

@@ -0,0 +1,48 @@
+\import{spin-macros}
+% clifford hopf spin draft
+\tag{clifford}
+
+% definition theorem lemma construction observation
+% convention corollary axiom example exercise proof
+% discussion remark
+% \taxon{}
+% \refnote{}{}{
+% }
+
+\refdef{Grade involution}{wieser2022formalizing}{
+\p{
+    \label{involute}
+    \lean{CliffordAlgebra.involute}
+    \leanok
+    \uses{iota}}
+
+\p{    \newvocab{Grade involution}, intuitively, is negating each basis vector.}
+
+\p{    Formally, it's an \vocab{algebra homomorphism} #{\alpha : \Cl(Q) \amap \Cl(Q)}, satisfying:}
+
+\ol{
+
+    \li{#{\alpha \circ \alpha = \operatorname{id}}}
+
+    \li{#{\alpha(\iota(m)) = - \iota(m)}}
+
+}
+
+\p{    for all #{m \in M}.}
+
+\p{    That is, the following diagram commutes:}
+
+\tikz{
+    \begin{tikzcd}[column sep=huge, row sep=huge]
+    \Cl(Q) \arrow[r, "\alpha"] & \Cl(Q) \\
+    V \arrow[ru, "-\iota"] \arrow[u, "\iota"]
+    \end{tikzcd}
+}
+
+\p{    It's called \newvocab{main involution} #{\alpha} or \newvocab{main automorphism} in \cite{jadczyk2019notes}, 
+    the \newvocab{canonical automorphism} in \cite{gallier2008clifford}.}
+
+\p{    It's denoted #{\hat{m}} in \cite{lounesto2001clifford}, #{\alpha(m)} in \cite{jadczyk2019notes}, #{m^*} in \cite{chisolm2012geometric}.}
+
+}
+

trees/ca-000J.tree

@@ -0,0 +1,45 @@
+\import{spin-macros}
+% clifford hopf spin draft
+\tag{clifford}
+
+% definition theorem lemma construction observation
+% convention corollary axiom example exercise proof
+% discussion remark
+% \taxon{}
+% \refnote{}{}{
+% }
+
+\refdef{Grade reversion}{wieser2022formalizing}{
+\p{
+    \label{reverse}
+    \lean{CliffordAlgebra.reverse}
+    \leanok
+    \uses{iota}}
+
+\p{    \newvocab{Grade reversion}, intuitively, is reversing the multiplication order of basis vectors.
+
+    Formally, it's an \vocab{algebra homomorphism} #{\tau : \Cl(Q) \amap \Cl(Q)^{\mathtt{op}}}, satisfying:}
+
+\ol{
+
+    \li{#{\tau(m_1 m_2) = \tau(m_2) \tau(m_1)}}
+    \li{#{\tau \circ \tau = \operatorname{id}}}
+    \li{#{\tau(\iota(m)) = \iota(m)}}
+
+}
+
+\p{    That is, the following diagram commutes:}
+
+\p{    \tikz{
+        \begin{tikzcd}[column sep=huge, row sep=huge]
+        \Cl(Q) \arrow[r, "\tau"] & \Cl(Q)^{\mathtt{op}} \\
+        V \arrow[ru, "\iota"] \arrow[u, "\iota"]
+        \end{tikzcd}
+      }}
+
+\p{    It's called \newvocab{anti-involution} #{\tau} in \cite{jadczyk2019notes}, the \newvocab{canonical anti-automorphism} in \cite{gallier2008clifford},
+    also called \newvocab{transpose}/\newvocab{transposition} in some literature, following tensor algebra or matrix.}
+
+\p{    It's denoted #{\tilde{m}} in \cite{lounesto2001clifford}, #{m^\tau} in \cite{jadczyk2019notes} (with variants like #{m^t} or #{m^\top} in other literatures), #{m^\dagger} in \cite{chisolm2012geometric}.
+}}
+

trees/ca-000K.tree

@@ -0,0 +1,56 @@
+\import{spin-macros}
+% clifford hopf spin draft
+\tag{clifford}
+
+% definition theorem lemma construction observation
+% convention corollary axiom example exercise proof
+% discussion remark
+% \taxon{}
+% \refnote{}{}{
+% }
+
+\refdef{Clifford conjugate}{wieser2022formalizing}{
+\p{
+    \label{conjugate}
+    \lean{CliffordAlgebra.reverse}
+    \leanok
+    \uses{involute,reverse}}
+
+\p{    \newvocab{Clifford conjugate} is an \vocab{algebra homomorphism}  #{{*} : \Cl(Q) \amap \Cl(Q)},
+    denoted #{x^{*}} (or even #{x^\dagger}, #{x^v} in some literatures),
+    defined to be:
+
+    ##{ x^{*} = \operatorname{reverse}(\operatorname{involute}(x)) = \tau(\alpha(x)) }
+
+    for all #{x \in \Cl(Q)}, satisfying
+    (as a \href{https://en.wikipedia.org/wiki/*-algebra#*-ring}{\newvocab{#{*}-ring}}):
+
+\ol{
+
+\li{#{(x + y)^{*} = (x)^{*} + (y)^{*}}}
+    \li{#{(x y)^{*} = (y)^{*} (x)^{*}}}
+    \li{#{{*} \circ {*} = \operatorname{id}}}
+    \li{#{1^{*} = 1}}
+
+}
+
+and (as a \href{https://en.wikipedia.org/wiki/*-algebra#*-algebra}{\newvocab{#{*}-algebra}}):
+
+    ##{ (r x)^{*} = r' x^{*} }
+
+    for all #{r \in R}, #{x, y \in \Cl(Q)} where #{'} is the involution of the commutative #{*}-ring #{R}.
+}
+
+\p{    Note: In our current formalization in \Mathlib, the application of the involution on #{r} is ignored,
+    as there appears to be nothing in the literature that advocates doing this.}
+
+\p{    % Grade reversion, reversing the multiplication order of basis vectors.
+    % Also called *transpose* in some literature, thus denoted
+}
+
+\p{    % It's called \newvocab{anti-involution} #{\tau} in \cite{jadczyk2019notes}.
+}
+
+\p{    \vocab{Clifford conjugate} is denoted #{\bar{m}} in \cite{lounesto2001clifford} and most literatures, #{m^\ddagger} in \cite{chisolm2012geometric}.
+}}
+

trees/spin-macros.tree

@@ -50,6 +50,7 @@
 \def\rfun{\mathit{1}} %{\iota_{0}}
 \def\afun{\iota_{a}}
 
+\def\href[url][t]{[\t](\url)}
 \def\Mathlib{\textsf{Mathlib} }
 \def\MathlibDoc[x]{\href{https://leanprover-community.github.io/mathlib4_docs/find/\#docs/\x}{\x}}