-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' of https://github.com/utensil/forest
- Loading branch information
Showing
14 changed files
with
255 additions
and
28 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -22,4 +22,5 @@ latex/trees | |
public | ||
server | ||
*.lock | ||
jms/ | ||
jms/ | ||
.vscode/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,3 @@ | ||
#!/bin/bash | ||
rm -rf output | ||
opam exec -- forester build --dev | ||
opam exec -- forester build # --dev |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
\title{basic macros} | ||
|
||
\p{Here we define:} | ||
|
||
\import{latex-preamble} | ||
|
||
\alloc\base/tex-preamble | ||
|
||
\p{\code{minitex}: A macro for typesetting LaTeX code in a minipage, with the width of an A5 paper, | ||
so the text size almost matches the size output by native forester code. This doesn't work very well on mobile yet.} | ||
|
||
\def\minitex[body]{ | ||
\scope{ | ||
\put?\base/tex-preamble{ | ||
\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} | ||
} | ||
} | ||
} | ||
|
||
\p{\code{texdef}: A macro for making a \code{minitex} definition with a reference.} | ||
|
||
\p{Usage:} | ||
|
||
\p{ | ||
\startverb | ||
\texdef{name}{reference}{ | ||
definition body in LaTeX | ||
} | ||
\stopverb | ||
} | ||
|
||
\def\texdef[name][reference][body]{ | ||
\title{\name ([[\reference]])} | ||
\taxon{definition} | ||
\minitex{\body} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
\title{LaTeX preambles} | ||
|
||
\p{Here we define:} | ||
|
||
\p{\code{latex-preamble/common}: Some common LaTeX preambles.} | ||
|
||
\def\latex-preamble/common{ | ||
\startverb | ||
% because LaTeX is running in `build` directory | ||
\input{../trees/preamble} | ||
\stopverb | ||
} | ||
|
||
\p{They are used by [[base-macros]].} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,133 @@ | ||
\usepackage{amsmath,amsfonts,amsthm,amssymb} | ||
\usepackage{tikz, tikz-cd, mathtools, stmaryrd} | ||
\usepackage[a5paper,margin=1in]{geometry} | ||
\usepackage{thmtools} | ||
\usepackage[framemethod=TikZ]{mdframed} | ||
|
||
\theoremstyle{definition} | ||
\theoremstyle{definition} | ||
\mdfdefinestyle{mdbluebox}{% | ||
roundcorner = 10pt, | ||
linewidth=1pt, | ||
skipabove=12pt, | ||
innerbottommargin=9pt, | ||
skipbelow=2pt, | ||
nobreak=true, | ||
linecolor=blue, | ||
backgroundcolor=TealBlue!5, | ||
} | ||
\declaretheoremstyle[ | ||
headfont=\sffamily\bfseries\color{MidnightBlue}, | ||
mdframed={style=mdbluebox}, | ||
headpunct={\\[3pt]}, | ||
postheadspace={0pt} | ||
]{thmbluebox} | ||
|
||
\mdfdefinestyle{mdredbox}{% | ||
linewidth=0.5pt, | ||
skipabove=12pt, | ||
frametitleaboveskip=5pt, | ||
frametitlebelowskip=0pt, | ||
skipbelow=2pt, | ||
frametitlefont=\bfseries, | ||
innertopmargin=4pt, | ||
innerbottommargin=8pt, | ||
nobreak=true, | ||
linecolor=RawSienna, | ||
backgroundcolor=Salmon!5, | ||
} | ||
\declaretheoremstyle[ | ||
headfont=\bfseries\color{RawSienna}, | ||
mdframed={style=mdredbox}, | ||
headpunct={\\[3pt]}, | ||
postheadspace={0pt}, | ||
]{thmredbox} | ||
|
||
\mdfdefinestyle{mdgreenbox}{% | ||
skipabove=8pt, | ||
linewidth=2pt, | ||
rightline=false, | ||
leftline=true, | ||
topline=false, | ||
bottomline=false, | ||
nobreak=true, | ||
linecolor=ForestGreen, | ||
backgroundcolor=ForestGreen!5, | ||
% innerleftmargin=20pt, | ||
innerrightmargin=15pt | ||
} | ||
\declaretheoremstyle[ | ||
headfont=\bfseries\sffamily\color{ForestGreen!70!black}, | ||
bodyfont=\normalfont, | ||
spaceabove=2pt, | ||
spacebelow=1pt, | ||
mdframed={style=mdgreenbox}, | ||
headpunct={ --- }, | ||
]{thmgreenbox} | ||
\declaretheoremstyle[ | ||
headfont=\bfseries\sffamily\color{ForestGreen!70!black}, | ||
bodyfont=\normalfont, | ||
spaceabove=2pt, | ||
spacebelow=1pt, | ||
mdframed={style=mdgreenbox}, | ||
headpunct={}, | ||
]{thmgreenbox*} | ||
|
||
\mdfdefinestyle{mdblackbox}{% | ||
skipabove=8pt, | ||
linewidth=3pt, | ||
rightline=false, | ||
leftline=true, | ||
topline=false, | ||
bottomline=false, | ||
linecolor=black, | ||
backgroundcolor=RedViolet!5!gray!5, | ||
} | ||
\declaretheoremstyle[ | ||
headfont=\bfseries\sffamily, | ||
bodyfont=\normalfont\small, | ||
spaceabove=0pt, | ||
spacebelow=0pt, | ||
mdframed={style=mdblackbox} | ||
]{thmblackbox} | ||
|
||
\declaretheoremstyle[ | ||
headfont=\bfseries\sffamily, | ||
bodyfont=\normalfont, %\small, %\sffamily, | ||
spaceabove=0pt, | ||
spacebelow=0pt | ||
]{def} | ||
|
||
\declaretheoremstyle[ | ||
headfont=\bfseries\sffamily, | ||
bodyfont=\normalfont, %\small, %\sffamily, | ||
spaceabove=0pt, | ||
spacebelow=0pt, | ||
numbered=no | ||
]{def*} | ||
|
||
\theoremstyle{definition} | ||
% \declaretheorem[style=thmblackbox,name=Definition,numberwithin=subsection]{definition} | ||
\declaretheorem[style=thmbluebox,name=Theorem,numberwithin=subsection]{theorem} | ||
\declaretheorem[style=thmbluebox,name=Theorem,numberwithin=subsection]{theoremx} % theorem not in dep graph | ||
\declaretheorem[style=thmbluebox,name=Lemma,sibling=theorem]{lemma} | ||
\declaretheorem[style=thmbluebox,name=Lemma,sibling=theorem]{lemmax} % lemma not in dep graph | ||
\declaretheorem[style=thmbluebox,name=Corollary,sibling=theorem]{corollary} | ||
\declaretheorem[style=thmbluebox,name=Proposition,sibling=theorem]{proposition} | ||
|
||
\theoremstyle{definition} | ||
% \newtheorem{claim}[theorem]{Claim} | ||
% \newtheorem{definition}[theorem]{Definition} | ||
\declaretheorem[style=def,name=Definition,sibling=theorem]{definition} | ||
\declaretheorem[style=def*,name=Definition]{definition*} | ||
% \newtheorem{fact}[theorem]{Fact} | ||
% \newtheorem{abuse}[theorem]{Abuse of Notation} | ||
|
||
\declaretheorem[style=thmredbox,name=Example,sibling=theorem]{example} | ||
|
||
\theoremstyle{theorem} | ||
% \declaretheorem[name=Question,sibling=theorem,style=thmblackbox]{ques} | ||
% \declaretheorem[name=Exercise,sibling=theorem,style=thmblackbox]{exercise} | ||
\declaretheorem[name=Remark,sibling=theorem,style=thmgreenbox]{remark} | ||
\declaretheorem[name=Remark,sibling=theorem,style=thmgreenbox*]{remark*} | ||
% \declaretheorem[name=Step,style=thmgreenbox]{step} % only used in Lebesgue int |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,4 @@ | ||
\title{Spin Geometry} | ||
\date{2019-03-05} | ||
\taxon{reference} | ||
|
||
% \author{todo} | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
\title{Clifford algebra (Wikipedia)} | ||
\taxon{reference} | ||
|
||
\p{See [Clifford algebra (Wikipedia)](https://en.wikipedia.org/wiki/Clifford_algebra).} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
\title{a survey of Spin groups} | ||
|
||
\author{utensil} | ||
|
||
\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/).} | ||
|
||
\p{This is also my first [[uts-0002]].} | ||
|
||
\transclude{spin-0002} | ||
|
||
\transclude{spin-0003} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
\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 | ||
|
||
$$ | ||
\operatorname{Spin}(V, q)=\operatorname{Pin}(V, q) \cap \mathrm{Cl}^0(V, q) | ||
$$ | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
\import{base-macros} | ||
|
||
\texdef{Spin group}{wiki-0001}{ | ||
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)$. | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,7 +1,9 @@ | ||
\title{Home} | ||
\title{home} | ||
|
||
\author{utensil} | ||
|
||
\date{2024-04-24} | ||
|
||
\p{Testing, see [Spin groups](uts-0002) for some math.} | ||
\p{[Experimenting](uts-0002), see [[spin-0001]] for some math.} | ||
|
||
\p{To search, press \code{Ctrl+K} or \code{Cmd+K}.} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,22 +1,11 @@ | ||
\title{A survey of Spin groups} | ||
\title{Forester experiment} | ||
|
||
\author{utensil} | ||
\date{2024-04-27} | ||
|
||
\date{2024-04-26} | ||
\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{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 [my PR to Mathlib4 about Spin groups](https://github.com/leanprover-community/mathlib4/pull/9111/).} | ||
\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.} | ||
|
||
\p{This is also an experiment of using [Forester](https://www.jonmsterling.com/jms-005P.xml) for building [forests of evergreen notes](https://www.jonmsterling.com/tfmt-000V.xml). I wish to use it to organize many definitions and discussions about Spin groups. My hope to find these notes easier to reuse and refer to in blogs, papers, blueprints etc.} | ||
|
||
\def\my-tex[body]{ | ||
\tex{ | ||
% \usepackage{tikz, tikz-cd, mathtools, amsmath, amssymb, stmaryrd} | ||
}{\body} | ||
} | ||
|
||
\my-tex{ | ||
Let $M$ be a module over a commutative ring $R$, equipped with a quadratic form $Q: M \to R$. | ||
} | ||
|
||
\p{See [[lawson2016spin]].} | ||
\p{My hope is to find these notes easier to reuse and refer to in blogs, papers, blueprints etc.} | ||
|
||
\p{See [The Forester markup language](https://www.jonmsterling.com/jms-007N.xml) for Markup references, also consult [Forester changlog](https://www.jonmsterling.com/jms-005P.xml) for updates.} |