From 9956de5277e99408b7a204677d3a495bb529ac16 Mon Sep 17 00:00:00 2001 From: Josia Pietsch Date: Fri, 16 Feb 2024 23:28:14 +0100 Subject: [PATCH] yaref dependencies --- inputs/lecture_02.tex | 4 ++-- inputs/lecture_03.tex | 4 ++-- inputs/lecture_06.tex | 4 ++-- inputs/lecture_07.tex | 4 ++-- inputs/lecture_11.tex | 4 ++-- inputs/lecture_14.tex | 8 +++---- inputs/lecture_15.tex | 12 +++++----- inputs/lecture_16.tex | 4 ++-- inputs/lecture_17.tex | 4 ++-- inputs/lecture_23.tex | 8 +++---- jrpie-yaref.sty | 54 ++++++++++++++++++++++++++++++++++++++++++- 11 files changed, 81 insertions(+), 29 deletions(-) diff --git a/inputs/lecture_02.tex b/inputs/lecture_02.tex index d7c6879..985b39c 100644 --- a/inputs/lecture_02.tex +++ b/inputs/lecture_02.tex @@ -40,7 +40,7 @@ \label{lem:closedaccumulation} A set $A \subseteq \R$ is closed iff $A' \subseteq A$. \end{lemma} -\begin{refproof}{lem:closedaccumulation} +\begin{yarefproof}{lem:closedaccumulation} ``$\implies$'' \gist{% Let $A$ be closed. Suppose that $x \in A' \setminus A$. @@ -75,7 +75,7 @@ there would be some Cauchy-sequence $(x_n)$ in $A$ such that $\lim_{n \to \infty} x_n \not\in A$. But then $x \in A' \subseteq A \lightning$. -\end{refproof} +\end{yarefproof} \begin{definition} $P \subseteq \R$ (or, more generally, a subset of any topological space) is called \vocab{perfect} diff --git a/inputs/lecture_03.tex b/inputs/lecture_03.tex index b740841..984d9b1 100644 --- a/inputs/lecture_03.tex +++ b/inputs/lecture_03.tex @@ -37,7 +37,7 @@ By the fact we just proved, all condensation points are accumulation points. -\begin{refproof}{thm:cantorbendixson} +\begin{yarefproof}{thm:cantorbendixson} Fix $A \subseteq \R$ closed. We want to see that $A$ is at most countable or there is some perfect $P \subseteq A$. @@ -109,7 +109,7 @@ all condensation points are accumulation points. \[ A = \overbrace{P}^{\mathclap{\text{perfect, unless $= \emptyset$}}} \cup \underbrace{(A \setminus P)}_{\mathclap{\text{at most countable}}}. \] -\end{refproof} +\end{yarefproof} \gist{\todo{Alternative proof of Cantor-Bendixson}}{} % \begin{remark} diff --git a/inputs/lecture_06.tex b/inputs/lecture_06.tex index ee18c61..22f0160 100644 --- a/inputs/lecture_06.tex +++ b/inputs/lecture_06.tex @@ -7,7 +7,7 @@ and $ b$ linearly ordered, $b$ has an upper bound. Then $a$ has a maximal element. \end{theorem} -\begin{refproof}{thm:zorn} +\begin{yarefproof}{thm:zorn} \gist{% Fix $(a, \le )$ as in the hypothesis. Let $A \coloneqq \{ \{(b,x) : x \in b\} : b \subseteq a, b \neq \emptyset\}$. @@ -96,7 +96,7 @@ \end{itemize} } -\end{refproof} +\end{yarefproof} \begin{remark} Over $\ZF$ the \yaref{ax:c} and \yaref{thm:zorn} diff --git a/inputs/lecture_07.tex b/inputs/lecture_07.tex index 9bb4ee5..bbe2262 100644 --- a/inputs/lecture_07.tex +++ b/inputs/lecture_07.tex @@ -19,7 +19,7 @@ or $\alpha \ni \beta$. \end{enumerate} \end{lemma} -\begin{refproof}{lem:7:ordinalfacts} +\begin{yarefproof}{lem:7:ordinalfacts} \gist{ We have already proved (a) before. @@ -115,7 +115,7 @@ as $\alpha_0 \in \beta_0 \in \alpha_0$. \end{subproof} }{Long and tedious, but not many ideas.} -\end{refproof} +\end{yarefproof} \begin{lemma} Let $X$ be a set of ordinals, diff --git a/inputs/lecture_11.tex b/inputs/lecture_11.tex index d304051..d887e0f 100644 --- a/inputs/lecture_11.tex +++ b/inputs/lecture_11.tex @@ -137,7 +137,7 @@ so $|a| = \aleph_\beta$ for some $\beta \le |\alpha|$. \] }{Then $\aleph_{\beta} \le \aleph_\alpha + \aleph_{\beta} \le \aleph_\alpha \cdot \aleph_\beta \le \aleph_\beta \cdot \aleph_\beta = \aleph_\beta$.} \end{proof} -\begin{refproof}{thm:hessenberg} +\begin{yarefproof}{thm:hessenberg} \gist{% Define a well-order $<^\ast$ on $\OR \times \OR$ by setting \[ @@ -218,7 +218,7 @@ so $|a| = \aleph_\beta$ for some $\beta \le |\alpha|$. \end{itemize} \end{itemize} } -\end{refproof} +\end{yarefproof} \gist{% However, exponentiation of cardinals is far from trivial: \begin{observe} diff --git a/inputs/lecture_14.tex b/inputs/lecture_14.tex index dcfc009..937e5f1 100644 --- a/inputs/lecture_14.tex +++ b/inputs/lecture_14.tex @@ -37,7 +37,7 @@ Clearly this is club but $\bigcap_{\beta < \kappa} C_\beta = \emptyset$. \end{warning} -\begin{refproof}{lem:clubintersection} +\begin{yarefproof}{lem:clubintersection} \gist{% First let $\alpha = 2$. Let $C, D \subseteq \kappa$ @@ -97,7 +97,7 @@ (we used $\cf(\kappa) > \alpha\cdot \omega$). \end{itemize} } -\end{refproof} +\end{yarefproof} \begin{definition} $F \subseteq \cP(a)$ is a \vocab{filter} @@ -172,7 +172,7 @@ We have shown (assuming \AxC to choose contained clubs): then $\diagi_{\beta < \kappa} C_{\beta}$ contains a club. \end{lemma} -\begin{refproof}{lem:diagiclub} +\begin{yarefproof}{lem:diagiclub} % TODO THINK \gist{ Let us fix $\langle C_{\beta} : \beta < \alpha \rangle$. @@ -277,7 +277,7 @@ We have shown (assuming \AxC to choose contained clubs): \end{itemize} } -\end{refproof} +\end{yarefproof} \begin{remark}+ $\diagi_{\beta < \kappa} C_{\beta}$ actually \emph{is} a club, diff --git a/inputs/lecture_15.tex b/inputs/lecture_15.tex index a4af044..420e20c 100644 --- a/inputs/lecture_15.tex +++ b/inputs/lecture_15.tex @@ -105,7 +105,7 @@ to be an elementary substructure of $V_\theta$. \end{lemma} Let's do a second proof of \yaref{thm:fodor}. -\begin{refproof}{thm:fodor} +\begin{yarefproof}{thm:fodor} \gist{% Fix $\theta > \kappa$ and look at $V_{\theta}$. @@ -151,7 +151,7 @@ Let's do a second proof of \yaref{thm:fodor}. such that $X_\xi \cap \kappa = \xi$ for all $\xi \in C$. \end{claim} - \begin{refproof}{thm:fodor:p2:c1} + \begin{yarefproof}{thm:fodor:p2:c1} Write $C = \{\xi < \kappa:X_\xi \cap \kappa = \xi\}$. Trivially $C$ is closed. Let us show that $C$ is unbounded in $\kappa$. @@ -171,7 +171,7 @@ Let's do a second proof of \yaref{thm:fodor}. \label{thm:fodor:p2:c1.1} $\xi \in C$, i.e.~$X_\xi \cap \kappa = \xi$. \end{claim} - \begin{refproof}{thm:fodor:p2:c1.1} + \begin{yarefproof}{thm:fodor:p2:c1.1} If $\eta < \xi$, then $\eta < \xi_n$ for some $n$ and then $\eta \in \xi_n \subseteq X_{\xi_n} \subseteq X_{\xi}$. @@ -180,8 +180,8 @@ Let's do a second proof of \yaref{thm:fodor}. Then $\eta \in X_{\xi_n}$ for some $n < \omega$, so $\eta < \xi_{n+1} < \xi$, hence $X_{\xi} \cap \kappa \subseteq \xi$. - \end{refproof} - \end{refproof} + \end{yarefproof} + \end{yarefproof} Now let $\alpha \in S \cap C$, i.e.~$X_\alpha \prec V_{\theta}$ and $\alpha = X_{\alpha} \cap \kappa$. @@ -280,4 +280,4 @@ Let's do a second proof of \yaref{thm:fodor}. \end{itemize} \end{itemize} } -\end{refproof} +\end{yarefproof} diff --git a/inputs/lecture_16.tex b/inputs/lecture_16.tex index d4ffb15..ccb7c01 100644 --- a/inputs/lecture_16.tex +++ b/inputs/lecture_16.tex @@ -101,7 +101,7 @@ one cofinality. -\begin{refproof}{thm:solovay}% +\begin{yarefproof}{thm:solovay}% \gist{% \footnote{``This is one of the arguments where it is certainly worth it to look at it again.''} We will only prove this for $\aleph_1$. @@ -253,7 +253,7 @@ one cofinality. \item $S_0 \coloneqq T_0 \cup \left( S \setminus \bigcup_{j > 0} T_j \right)$, $S_i \coloneqq T_i$. \end{itemize} } -\end{refproof} +\end{yarefproof} \gist{% We now want to do another application of \yaref{thm:fodor}. Recall that $2^{\kappa} > \kappa$, in fact $\cf(2^{\kappa}) > \kappa$ diff --git a/inputs/lecture_17.tex b/inputs/lecture_17.tex index 4ed2f66..e0d1558 100644 --- a/inputs/lecture_17.tex +++ b/inputs/lecture_17.tex @@ -25,7 +25,7 @@ We will only prove \end{remark} }{} -\begin{refproof}{thm:silver1} +\begin{yarefproof}{thm:silver1} \gist{% We need to count the number of $X \subseteq \aleph_{\omega_1}.$ Let us fix $\langle f_\lambda : \lambda < \kappa \text{ an infinite cardinal} \rangle$ @@ -274,4 +274,4 @@ We will only prove \end{itemize} } -\end{refproof} +\end{yarefproof} diff --git a/inputs/lecture_23.tex b/inputs/lecture_23.tex index 8f275f3..2f32611 100644 --- a/inputs/lecture_23.tex +++ b/inputs/lecture_23.tex @@ -73,7 +73,7 @@ We shall prove: \footnote{Being a cardinal is $\Pi_1$, so $M[h]$ cardinals are always $M$ cardinals.} \end{claim} -\begin{refproof}{l23:c:2} +\begin{yarefproof}{l23:c:2} Suppose not. Let $\kappa$ be minimal such that $M \models \text{``$\kappa$ is a cardinal''}$, but $M[h] \models \text{``$\kappa$ is not a cardinal''}$. @@ -119,12 +119,12 @@ We shall prove: But $|\lambda \times \omega| = |\lambda| = \lambda$, so in $M$ there is a surjection $F' \colon \lambda \to \kappa$, but $\kappa$ is a cardinal in $M$ $\lightning$. -\end{refproof} +\end{yarefproof} -\begin{refproof}{l23:c:1} +\begin{yarefproof}{l23:c:1} Omitted. % TODO combinatorial argument -\end{refproof} +\end{yarefproof} diff --git a/jrpie-yaref.sty b/jrpie-yaref.sty index d7347cd..5c21fa8 100644 --- a/jrpie-yaref.sty +++ b/jrpie-yaref.sty @@ -5,6 +5,48 @@ \RequirePackage{amstext} \RequirePackage{xspace} +\newwrite\yaref@output +\immediate\openout\yaref@output=\jobname.yaref.json +\write\yaref@output{data = [} + +\newcounter{yarefproof@depth} +\setcounter{yarefproof@depth}{0} + +\edef\yaref@hastag{\string#}% + +\let\yaref@oldlabel\label +\def\publicurl{https://josia-notes.users.abstractnonsen.se/w23-logic-2/logic2.pdf} + +\newenvironment{yarefproof}[1]{% + \ifnum\the\value{yarefproof@depth}=0% + \global\def\yarefproof@current{#1}% + \fi% + \addtocounter{yarefproof@depth}{1}% + \begin{refproof}{#1}% Depth: \theyarefproof@depth +}{% + \end{refproof}% + \addtocounter{yarefproof@depth}{-1}% + %\ifnum\yarefproof@depth=0% + % \def\yarefproof@current{nothing}% + %\fi% + %\let\yarefproof@current=\undefined% + \ignorespacesafterend% +} + +\newcommand{\yaref@writedependency}[1]{% + \ifnum\the\value{yarefproof@depth}=0% + % not in a proof environment + %\write\yaref@output{EDGE: #1 - \theyarefproof@depth}% + \else% + \ifcsname yarefproof@current\endcsname% + \write\yaref@output{{data: {id:"#1\yarefproof@current", source:"#1", target: "\yarefproof@current"}},}% + \else% + % in a proof env, but no label defined ??? + %\write\yaref@output{{#1 - ERROR}}% + \fi% + \fi% +} + \newcommand{\yaref@text@large}[1]{% \ifcsname yaref@longlabel@#1\endcsname% \hyperref[#1]{\csname yaref@longlabel@#1\endcsname\ (\ref*{#1})}% @@ -30,14 +72,16 @@ } \newcommand{\yalabel}[3]{% + \yaref@oldlabel{#3}% \write\@auxout{\noexpand\expandafter\noexpand\gdef\noexpand\csname yaref@longlabel@#3\noexpand\endcsname{#1}}% \write\@auxout{\noexpand\expandafter\noexpand\gdef\noexpand\csname yaref@shortlabel@#3\noexpand\endcsname{#2}}% + \write\yaref@output{{data: {id: "#3", label: "#1", short: "#2", href: "\publicurl\yaref@hastag\getrefbykeydefault{#3}{anchor}{}"}},}% \expandafter\gdef\csname yaref@longlabel@#3\endcsname{#1}% \expandafter\gdef\csname yaref@shortlabel@#3\endcsname{#2}% - \label{#3}% } \newcommand{\yaref}[1]{% + \yaref@writedependency{#1}% \relax\ifmmode% \mathchoice {\yaref@math@large{#1}} % display style @@ -50,9 +94,17 @@ } % Force a small reference \newcommand{\yarefs}[1]{% + %\yaref@writedependency{#1}% \relax\ifmmode% \yaref@math@verysmall{#1}% scriptscript style \else% \yaref@text@small{#1}\xspace% \fi% } +\renewcommand{\label}[1]{% + \yaref@oldlabel{#1}% + % \getrefbykeydefault{#1}{name}{} + \write\yaref@output{{data: {id: "#1", label: "\getrefnumber{#1}", href: "\publicurl\yaref@hastag\getrefbykeydefault{#1}{anchor}{}"}},}% +} + +\AtEndDocument{\write\yaref@output{{}]}}