From cde9c5fb67451721966e5e163d7f626e5f355775 Mon Sep 17 00:00:00 2001
From: Deyao Chen <chendeyao000@gmail.com>
Date: Wed, 3 Dec 2025 13:31:37 +0000
Subject: [PATCH 1/2] add helper function and one example

---
 ha/3-tp.typ       |  2 +-
 ha/4-enough.typ   |  2 +-
 libs/template.typ | 11 +++++++++++
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/ha/3-tp.typ b/ha/3-tp.typ
index eb73700..f1f236b 100644
--- a/ha/3-tp.typ
+++ b/ha/3-tp.typ
@@ -415,7 +415,7 @@ $
 
 Then this makes $hom_S (B, -)$ a functor from $ModS$ to $ModR$.
 
-#theorem[
+#theorem("Tensor-hom Adjunction")[
   Let $R$, $S$ be rings. Let $A$ be a #rrm, $B$ be an $R$-$S$-bimodule, and $C$ be a right $S$-module. Then we have a canonical isomorphism
   $ tau: hom_S (A tpr B, C) bij hom_R (A, hom_S (B, C)), $
   where for $f : A tpr B -> C$, $a in A$, and $b in B$,
diff --git a/ha/4-enough.typ b/ha/4-enough.typ
index 2d140a8..5855559 100644
--- a/ha/4-enough.typ
+++ b/ha/4-enough.typ
@@ -366,6 +366,6 @@ With this proposition, we can prove that an abelian category has enough projecti
   // Exercise: $e_M$ is one-to-one (mono). (like what we did before.) [TODO]
   We would like to show that $e_M$ is an injective function.
   We only need to show that for any $0 != m in M$, there exists $phi : M -> hom_Ab (R, QQ over ZZ)$ such that $phi(m) != 0$. Then since $ phi in homr(M, hom_Ab (R, QQ over ZZ)) iso hom_Ab (M, QQ over ZZ) $
-  by @tensor-hom,
+  by #thmref(<tensor-hom>),
   we only need to find some $phi : M -> QQ over ZZ$ in $Ab$ so that $phi(m) != 0$, which is given by @map-to-q-over-z.
 ]
diff --git a/libs/template.typ b/libs/template.typ
index 4124c3e..d73e07b 100644
--- a/libs/template.typ
+++ b/libs/template.typ
@@ -117,6 +117,17 @@
   breakable: true,
 )[_#title._ #term #h(1fr) $qed$]
 
+// Helper to reference theorems/props with their optional name.
+#let thmref(id) = {
+  context {
+    if query(id).at(0).caption != none {
+      [#ref(id) (#query(id).at(0).caption.body)]
+    } else {
+      [#ref(id)]
+    }
+  }
+}
+
 #let project(title: "", authors: (), date: none, body) = {
   // Set the document's basic properties.
   set document(author: authors, title: title)

From 471555281e4fa366c233c6ec46f13580d3d6be3d Mon Sep 17 00:00:00 2001
From: Deyao Chen <chendeyao000@gmail.com>
Date: Wed, 3 Dec 2025 14:11:13 +0000
Subject: [PATCH 2/2] change Baer's Criterion

---
 ha/4-enough.typ | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ha/4-enough.typ b/ha/4-enough.typ
index 5855559..cf00ba5 100644
--- a/ha/4-enough.typ
+++ b/ha/4-enough.typ
@@ -239,7 +239,7 @@ For most of our homological algebra to work, an abelian category needs to have e
 #proof[@rotman[Corollary 3.35] and @notes[Corollary 5.9].
   Let $M$ be an injective $R$-module, and let $m in M$ and
   $r in R without brace.l 0 brace.r$. Set $J eq r R$ (which is an ideal of $R$) and define
-  $f colon J arrow.r M$ by $f lr((r)) eq m$. By Baer’s Criterion, we may
+  $f colon J arrow.r M$ by $f lr((r)) eq m$. By #thmref(<baer-cri>), we may
   extend $f$ to a homomorphism $tilde(f) colon R arrow.r M$. Then
   $
     m eq f lr((r)) = tilde(f)(r)eq tilde(f) lr((r dot.op 1)) eq r dot.op tilde(f) lr((1)).
@@ -254,7 +254,7 @@ For most of our homological algebra to work, an abelian category needs to have e
   $m eq f lr((r))$. Then since $M$ is divisible, there is some $m' in M$
   such that $m eq r m'$. Define $tilde(f) colon R arrow.r M$ by
   $tilde(f) lr((1)) eq m'$. Clearly $tilde(f)$ is an extension of $f$, so
-  $M$ is injective by Baer’s Criterion.
+  $M$ is injective by #thmref(<baer-cri>).
 ]
 
 #corollary[