6 Remaining sorry’s
Here is the list of all the remaining Lean statements using sorry at the time of writing, with a mathematical description and some ideas for the proofs.
Let \(R\) be a Noetherian ring. Then \(R[[X]]\) is Noetherian.
This is necessary for section 5.1 especially to show that some quotients of \(S = \Lambda [[X_1, \ldots , X_r]]\) are in \(\mathbf{C}_\Lambda \). This is an important result that is currently missing from Mathlib. I have heard that someone was working on this, so I shouldn’t need to prove this.
Let \(R\) be a local ring, \(\mathfrak {m}\) its maximal ideal, \(r, k \in \mathbb {N}\), \(\mathfrak {n}\) the maximal ideal of \(R[[X_1, \cdots , X_r]]\) and \(x = (x_n)_{n \in \mathbb {N}^{r}} \in R[[X_1, \cdots , X_r]]\). Then \(x \in \mathfrak {n}^k \iff \forall n \in \mathbb {N}^{r}, x_n \in \mathfrak {m}^{k - \deg (n)}\).
The forward direction is easy. The converse should probably be shown by induction on \(r\) (and \(k\)).
This lemma is very important to deal with \(S = \Lambda [[X_1, \ldots , X_r]]\), for example to show that \(S\) is complete when \(\Lambda \) is and to show that \(R_2 \cong k[k^r]\) in section 5.1.
The functor \(h_R\) (see definition 22) preserves pullbacks.
See lemma 42.
It suffices to show that the inclusion functor preserves pullbacks.
The functor \(h_R\) satisfies \((H_3)\).
See lemma 42.
I have shown that \(h_R(k[\varepsilon ]) = Hom(R, k[\varepsilon ]) \cong Der_\Lambda (R, k[\varepsilon ]) \cong (\mathfrak {m}_R / (\mathfrak {m}_R ^2 + \mathfrak {m}_\Lambda R))^*\). The main missing part is the linearity of the first bijection. The fact that \(\mathfrak {m}_R / (\mathfrak {m}_R ^2 + \mathfrak {m}_\Lambda R)\) is finite dimensional is also missing for now.
The map \(Hom(k^r, k) \to Hom(k[k^r], k[\varepsilon ])\) is \(k\)-linear (\(r \in \mathbb {N}\)). (\(k\) here is the residue field of \(\Lambda \))
The vector space structure on \(Hom(k[k^r], k[\varepsilon ])\) here is the one induced by the coyoneda functor \(Hom(k[k^r], -)\) (lemma 18). This is somewhat similar to the previous point, where the abstract vector space structure is the main issue. This is used in section 5.1 to show the existence of \(\xi _2\).
Let \(R\) be a \(Λ\)-algebra, and \(J, K\) ideals of \(R\). Then,
This is the easiest sorry.
In the proof of the theorem, we have \(r \in \mathbb {N}\), \(S = \Lambda [[X_1, \cdots , X_r]]\), and \(J \neq S\) an ideal of \(S\). \(S / J\) is complete (as a local ring).
This is needed for section 5.1. It is essentially a topological result that is in Mathlib (as ), however it is stated here in a way that doesn’t mention topology, and in fact the topology has not been defined at all in Lean yet.
theorem 44 Only \((H_3)\) has been shown for now. The proof is described in section 5.2.