From 56dda2fce0cec1371d43b892effd2a1c7c91591b Mon Sep 17 00:00:00 2001 From: utensil Date: Sun, 2 Jun 2024 17:51:18 +0800 Subject: [PATCH] feat(ca): add operations --- .vscode/settings.json | 3 ++- fize.sh | 5 ++-- tex/preamble.tex | 2 ++ trees/ca-0001.tree | 2 ++ trees/ca-0009.tree | 2 +- trees/ca-000C.tree | 4 +-- trees/ca-000G.tree | 14 +++++++++++ trees/ca-000H.tree | 15 +++++++++++ trees/ca-000I.tree | 48 ++++++++++++++++++++++++++++++++++++ trees/ca-000J.tree | 45 +++++++++++++++++++++++++++++++++ trees/ca-000K.tree | 56 ++++++++++++++++++++++++++++++++++++++++++ trees/spin-macros.tree | 1 + 12 files changed, 191 insertions(+), 6 deletions(-) create mode 100644 trees/ca-000G.tree create mode 100644 trees/ca-000H.tree create mode 100644 trees/ca-000I.tree create mode 100644 trees/ca-000J.tree create mode 100644 trees/ca-000K.tree diff --git a/.vscode/settings.json b/.vscode/settings.json index 471a701..7782d58 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -3,6 +3,7 @@ "explorer.excludeGitIgnore": false, "latex-workshop.latex.autoBuild.run": "never", "conventionalCommits.scopes": [ - "style" + "style", + "ca" ], } \ No newline at end of file diff --git a/fize.sh b/fize.sh index b522b92..f16a486 100755 --- a/fize.sh +++ b/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 diff --git a/tex/preamble.tex b/tex/preamble.tex index fe6917f..312b382 100644 --- a/tex/preamble.tex +++ b/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} diff --git a/trees/ca-0001.tree b/trees/ca-0001.tree index 9364dc4..562c4fd 100644 --- a/trees/ca-0001.tree +++ b/trees/ca-0001.tree @@ -33,4 +33,6 @@ \block{Clifford Algebra}{ \transclude{ca-000F} + + \transclude{ca-000G} } diff --git a/trees/ca-0009.tree b/trees/ca-0009.tree index 14cd218..f855618 100644 --- a/trees/ca-0009.tree +++ b/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 diff --git a/trees/ca-000C.tree b/trees/ca-000C.tree index b672cab..10461cd 100644 --- a/trees/ca-000C.tree +++ b/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} diff --git a/trees/ca-000G.tree b/trees/ca-000G.tree new file mode 100644 index 0000000..e418bc7 --- /dev/null +++ b/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} diff --git a/trees/ca-000H.tree b/trees/ca-000H.tree new file mode 100644 index 0000000..601f860 --- /dev/null +++ b/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)}. +}} + diff --git a/trees/ca-000I.tree b/trees/ca-000I.tree new file mode 100644 index 0000000..e643cd4 --- /dev/null +++ b/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}.} + +} + diff --git a/trees/ca-000J.tree b/trees/ca-000J.tree new file mode 100644 index 0000000..8cff2f8 --- /dev/null +++ b/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}. +}} + diff --git a/trees/ca-000K.tree b/trees/ca-000K.tree new file mode 100644 index 0000000..ab80d0c --- /dev/null +++ b/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}. +}} + diff --git a/trees/spin-macros.tree b/trees/spin-macros.tree index 0763dd6..ae021e5 100644 --- a/trees/spin-macros.tree +++ b/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}}