From e64b710025e18c7432b86775d714ef8b96f21aa5 Mon Sep 17 00:00:00 2001
From: Patrick Massot <patrickmassot@free.fr>
Date: Sun, 7 Jun 2020 23:44:35 +0200
Subject: [PATCH] BP: smoothness of dual basis

---
 blueprint/src/loops.tex | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/blueprint/src/loops.tex b/blueprint/src/loops.tex
index 12748902..a11f1f60 100644
--- a/blueprint/src/loops.tex
+++ b/blueprint/src/loops.tex
@@ -171,8 +171,19 @@ \section{Preliminaries}
   By continuity of the determinant, this stays true
   for $q$ in $Π_i B_δ(p_i)$ for some positive $δ$.
   Let $e^*_i(q)$ denote the elements of the dual basis.
-  The map $q ↦ e^*_i(q)$ is smooth on $Π_i B_δ(p_i)$ because this can't
-  be false.
+  In order to prove smoothness of these maps and define them
+  for every $q$, we fix a basis $B$ of $E$ and the corresponding
+  determinant $\det_B : E^d → ℝ$.
+  We set $δ(q) = \det_B(e(q))$ and define
+  \[
+    e^*_i(q) = v ↦
+    \det_B(e_1(q), \dots, e_{i-1}(q), v, e_{i+1}(q), \dots, e_d(q))/δ(q).
+  \]
+  which should be interpreted as the zero linear form if $δ(q) = 0$
+  (this interpretation is automatic if division by zero in $ℝ$
+  is defined as zero, as it should be).
+  The map $q ↦ e^*_i(q)$ is smooth on $Π_i B_δ(p_i)$ where $δ$
+  does not vanish since the determinant is polynomial.
   We set $w_i(y, q) = e^*_i(q)(y - q_0)$.
   The computation of $x - p_0$ above proves that
   $w_i(x, p) = w_i$.