REVIEW 2 major objections 4 minor 11 references
Note on the coincidence of two henselisations
T0 review · 2 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash
Pith's one-line read Two henselisation constructions coincide: proof supplied
desk verdict A modest, useful constructive proof that two henselisations coincide, but the surjectivity step is too under-documented to trust as written. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The argument is carried by three linked devices. First, special polynomials of the form $g(X)=X^n-X^{n-1}+a_0\ell(X)$ with $a_0\in m$: every Hensel polynomial can be replaced by one of these, so each elementary step of the local-ring henselisation adds a single special zero $\delta=1+\mu$ and computations can be done in the algebra $K[\delta]$. Second, Newton polygons of polynomials over $V$: an isolated slope of the polygon of $q\in V[X]$ corresponds to a v-isolated zero in $K^H$ that is explicit as an element of $K$ or as $(a\delta+b)/(c\delta+d)$, and the characteristic polynomials $q(T)$ and $r(T)=T p(T)$ give a test for whether $\alpha'=p(\mu')$ is zero. Third, Lemma 4, imported from earlier work: every $\eta\in K[\delta]$ admits an $m$ with $\delta^m\eta$ a v-isolated zero of a polynomial with coefficients in $V$, which is what pulls arbitrary elements of $V^H$ back into $V^h$. Supporting machinery includes Tate's trace formula, used to prove $V_{g_1}$ is integrally closed and integral.
What would settle it
Take $K=\mathbb{Q}$ with the $p$-adic valuation and $V=\mathbb{Z}_{(p)}$, let $\delta$ be the special zero of $g(X)=X^2-X-p$, and for a candidate $\eta\in\mathbb{Q}[\delta]$ with $v(\eta)\ge 0$ compute whether some $\delta^m\eta$ is the zero corresponding to an isolated Newton-polygon slope of a polynomial in $V[X]$; if any $\eta$ fails the test, Lemma 4 is false and the proof breaks, while an element of $V^H$ that stays outside every intermediate $V_u$ in the colimit would falsify Theorem 1 itself.
Extended reading notes
Core claim
Let $(K,V)$ be a discrete valued field with henselisation $(K^H,V^H)$, and let $(V^h,m^h)$ be the henselisation of the residually discrete local ring $(V,m)$. The paper establishes that the unique local morphism of $V$-algebras $\varphi: V^h \to V^H$ is an isomorphism. Injectivity is proved step by step: for each elementary extension $V_{g_1}$ obtained by adding the Hensel zero of a special polynomial, an element $\alpha=p(\mu)$ that maps to zero in $V^H$ is shown to be zero in $V_{g_1}$, using the characteristic polynomial $q(T)$ of $p(x)$ and the fact that if $q(0)=0$, writing $q=T^m q_1$ with $q_1(0)\neq 0$, the relation $q_1(\alpha')\neq 0$ forces $q_1(\alpha)\neq 0$ and hence $\alpha=0$. Since $V_{g_1}$ is integral, the map is injective. Surjectivity reduces to showing that every element $\eta\in K[\mu]$ with $v(\eta)\ge 0$ lies in $V^h$: Lemma 4 gives an exponent $m$ such that $\delta^m\eta$ is a v-isolated zero of a polynomial with coefficients in $V$, so $\delta^m\eta$ lands in some intermediate henselisation step inside $V^h$, and since $1/\delta\in V^h$, $\eta\in V^h$. Consequently the fields of fractions coincide and $V^H\subseteq V^h$, completing the isomorphism.
Load-bearing premise
Lemma 4, cited rather than reproved, claims that for every element $\eta\in K[\delta]$ some power $\delta^m\eta$ is a v-isolated zero of a polynomial with coefficients in $V$; if that characterisation fails for a discrete valued field, the surjectivity conclusion $\eta\in V^h$ does not follow.
Editorial extensions
If this is right
- The henselisation $K^H$ is the field of fractions of $V^h$, giving a direct embeddability of the valued-field henselisation inside the local-ring henselisation.
- Every element of $V^H$ can be written as an element of $V^h$ divided by a power of a special zero $\delta$, so membership in the henselisation is controlled by Newton polygon data.
- The two universal properties—being the universal henselian residually discrete local ring over $V$ and being the universal henselian discrete valued field over $(K,V)$—define the same extension, so results proved for one construction transfer to the other.
- Because the proof is constructive, the equality-to-zero test for elements of $V^H$ yields a decision procedure for whether an element of $K[\delta]$ lies in $V^h$.
Reading between the lines
- The proof's reliance on Newton polygons suggests that for computable valued fields the isomorphism can be made effective: one should be able to decide membership in the henselisation by computing characteristic polynomials and isolated slopes, a concrete algorithm the paper does not spell out.
- Lemma 4 is the real engine of the surjectivity proof; a self-contained treatment would need to internalise the Newton-polygon characterisation rather than citing it, and the same lemma is likely to control how far the two henselisations differ for more general valuation rings.
- The same coincidence plausibly extends to higher-rank or non-discrete valuations whenever an analogue of Lemma 4 holds, so the theorem may be less about discreteness and more about the availability of isolated Newton slopes.
- For classical readers, the note converts a folklore commutativity of constructions into a proved statement, which matters for any work that silently identifies the two henselisations in proofs.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper compares two constructive henselisations of a discrete valued field (K,V): the henselisation Vh of the residually discrete local ring V, built in Alonso García–Lombardi–Perdry 2008, and the valuation ring VH of the henselised field KH, built in Kuhlmann–Lombardi 2000. Theorem 1 asserts that the canonical local morphism of V-algebras φ: Vh → VH is an isomorphism, and that the proof is valid both in Bishop-style constructive mathematics and classically. Injectivity is shown by reducing to elementary steps and using a characteristic-polynomial zero test; surjectivity is reduced to showing that every element of VH with nonnegative valuation lies in Vh, using Lemma 4 on v-isolated zeros. Three appendices give constructive proofs of integral closedness of the rings Vf, based on Tate's formula.
Significance. If the proof is completed, the paper would fill a real gap: the identification of the two henselisations is usually taken as obvious in the literature, and the authors provide a constructive proof rather than a classical existence argument. The appendices contain useful and apparently correct constructive tools, in particular Tate's lemma and the proof that the localised rings Vf are integrally closed. The paper does not claim machine-checked proofs, but it does give explicit constructive arguments for the integral-closedness side. The main theorem is natural and likely true; however, the surjectivity argument as written leaves a load-bearing inference unjustified, so the paper is not yet ready for publication without revision.
major comments (2)
- [Proof of Theorem 1, Surjectivity] The sentence 'It shows that δ^mη is in the image of a certain Vu ⊆ Vh' is not a consequence of Lemma 4 as stated. Lemma 4 only gives that α := δ^mη is a v-isolated zero of some Q ∈ V[X]. To conclude α ∈ Vh one must use the explicit description of v-isolated zeros quoted from Kuhlmann–Lombardi 2000, Proposition 2.2: either α ∈ K (then v(α) ≥ 0 gives α ∈ V), or α = (aδ'+b)/(cδ'+d) with δ' a special zero. In the second case the note does not prove that the fraction belongs to the elementary henselisation ring Vu obtained by adjoining δ': it is not shown that cδ'+d is a unit in Vu, nor that the alternative route via the integral closedness of V[δ'] (Lemma 12) applies, which would require proving that V[δ'] is the valuation ring of K[δ'] (i.e., uniqueness of the valuation extension). Since this step is exactly what completes the surjectivity of φ, the proof is incomplete as written.
- [Equality to 0 in the henselisation of a discrete valued field, Lemma 4] Lemma 4 is load-bearing for Theorem 1, but its proof is reduced to a citation: 'Result given in Kuhlmann and Lombardi 2000, proof of proposition 2.3.' The note should either reproduce the proof (the comparison of valuations of conjugates mentioned in the surrounding text is short and would fit in a note) or quote the precise statement from the cited paper and explain exactly how it yields the assertion. As it stands, the main theorem depends on an unstated proof in another paper, and this dependence is not merely cosmetic: the step from 'δ^mη is a v-isolated zero' to 'δ^mη lies in the image of some Vu' is the delicate part of the surjectivity proof and needs to be visible.
minor comments (4)
- [Equality to 0 in the henselisation of a discrete valued field] In the paragraph after the definition of the special polynomial, the sentence 'The µ′_i for i ≥ 2 are units, their valuation is zero' is easy to misread: the non-special roots of g1 are µ′_i = δ_i − 1, whose valuation is zero, whereas the special zero µ has positive valuation. Please clarify which roots are being discussed.
- [Proof of Theorem 1, Injectivity] The phrase 'Now we know that the natural morphism θ : Vg1 → VH is injective and that Vg1 itself is integral' appears after the argument that already uses the zero-divisor-free property of Vg1. The wording is confusing; it would help to state separately, before the injectivity proof, that Vg1 has no zerodivisors by Remark 3, and then to conclude injectivity at the end.
- [Appendix 1] The proof in Appendix 1 relies on the result of Alonso García–Lombardi–Neuwirth 2021 that Ker(θ_f) is a minimal detachable prime ideal. Since this is another externally imported fact, it should be stated precisely in the note rather than summarised by reference.
- [Introduction and terminology] The paper would benefit from a sentence explicitly saying which results are proved in the note and which are imported from earlier papers, so that the reader can identify the chain of dependencies for Theorem 1 at a glance.
Circularity Check
No significant circularity: the isomorphism is proved from independent prior constructions; self-citations are not load-bearing in a circular way.
full rationale
The paper's central claim is Theorem 1, stating that the canonical morphism φ: Vh → VH is an isomorphism. The morphism is obtained from the universal property of the henselisation Vh, because VH is a henselian residually discrete local ring; this is standard and does not assume the conclusion. Injectivity is proved for an elementary step Vg1 → VH using characteristic polynomials q and r: the implication α′ = 0 ⇒ α = 0 is derived algebraically from q(α) = α^m q1(α) = 0 and q1(α′) ≠ 0, not from the isomorphism being proved. Surjectivity uses Lemma 4, cited from Kuhlmann and Lombardi 2000, to obtain an m such that δ^m η is a v-isolated zero of a polynomial, and then asserts that this places δ^m η in some Vu ⊆ Vh. This inference may deserve more detail, but it is not circular: Lemma 4 is a separate result about Newton polygons and isolated zeros, and it does not state or presuppose that φ is surjective, nor does it depend on Theorem 1. The constructions of Vh and VH are taken from prior papers by the same group, but they are cited as independent published constructions, not as a self-supporting chain proving the theorem. Appendices 1–3 provide proofs of integral closedness using Tate's formula and results of Coquand and Lombardi, which are external algebraic facts. No parameter is fitted and no prediction is relabelled as an output. The skeptic's concern about the step from 'δ^m η is a v-isolated zero' to 'δ^m η ∈ Vh' is a potential correctness gap, not a circularity: the conclusion is not equivalent to an input by construction. Under the hard rules, an under-justified or cited lemma is not circularity unless the load-bearing argument reduces to the target result; here it does not.
Assumptions & free parameters
assumptions (3)
- domain assumption The constructions and universal properties of Vh and VH from Alonso García-Lombardi-Perdy 2008 and Kuhlmann-Lombardi 2000 are correct.
- domain assumption Kuhlmann-Lombardi 2000, Proposition 2.3 and its proof provide the Newton polygon equality-to-zero test and Lemma 4.
- standard math Coquand-Lombardi 2016, Theorem 6.3: if A is normal and f is monic, then A{f} is normal.
Cite this review
Pith. "Pith review of Note on the coincidence of two henselisations." pith.science (2026). https://pith.science/paper/BJWJQIHM
@misc{pith2026241118186,
author = {Pith},
title = {Pith review of: Note on the coincidence of two henselisations},
year = {2026},
howpublished = {\url{https://pith.science/paper/BJWJQIHM}},
note = {Machine review of arXiv:2411.18186}
}
read the original abstract
We compare two henselisations of a residually discrete valuation domain. Our constructive proof that a certain natural morphism is an isomorphism is also a proof in classical mathematics. Although this isomorphism is implicitly accepted as obvious in the literature, it seems that no proof was previously available.
Reference graph
Works this paper leans on
-
[1]
Elementary constructive theory of H enselian local rings
Mar\' a Emilia Alonso Garc\' a , Henri Lombardi , and Herv \'e Perdry . Elementary constructive theory of H enselian local rings. Math. Log. Q., 54: 0 253--271, 2008. doi:10.1002/malq.200710057
-
[2]
Mar\' a Emilia Alonso Garc\' a , Henri Lombardi , and Stefan Neuwirth . On a theorem by de Felipe and Teissier about the comparison of two henselisations in the non-Noetherian case . J. Algebra , 570: 0 587--594, 2021. doi:10.1016/j.jalgebra.2020.11.020
-
[3]
Foundations of constructive analysis
Errett Bishop. Foundations of constructive analysis. McGraw-Hill, New York, 1967
work page 1967
-
[4]
Errett Bishop and Douglas Bridges. Constructive analysis. Grundlehren der mathematischen Wissenschaften, 279. Springer, Berlin, 1985. doi:10.1007/978-3-642-61667-9
-
[5]
Varieties of constructive mathematics
Douglas Bridges and Fred Richman. Varieties of constructive mathematics. London Mathematical Society Lecture Note Series, 97. Cambridge University Press, Cambridge, 1987. doi:10.1017/CBO9780511565663
-
[6]
Some remarks about normal rings
Thierry Coquand and Henri Lombardi. Some remarks about normal rings. In Dieter Probst and Peter Schuster, editors, Concepts of proof in mathematics, philosophy, and computer science, Ontos Mathematical Logic, 6, pages 141--149. De Gruyter, Berlin, 2016. doi:10.1515/9781501502620-008
-
[7]
Construction du hens\'elis\'e d'un corps valu\'e
Franz-Viktor Kuhlmann and Henri Lombardi. Construction du hens\'elis\'e d'un corps valu\'e . J. Algebra, 228: 0 624--632, 2000. doi:10.1006/jabr.2000.8289
-
[8]
Commutative algebra: constructive methods
Henri Lombardi and Claude Quitt \'e . Commutative algebra: constructive methods. Finite projective modules. Algebra and applications, 20. Springer, Dordrecht, 2015. URL https://arxiv.org/abs/1605.04832. Translated from the French (Calvage & Mounet, Paris, 2011, revised and extended by the authors) by Tania K. Roblot
arXiv 2015
Show all 11 references
-
[9]
A course in constructive algebra
Ray Mines, Fred Richman, and Wim Ruitenburg. A course in constructive algebra. Universitext. Springer, New York, 1988. doi:10.1007/978-1-4419-8640-5
1988 doi
-
[10]
Anneaux locaux hens\' e liens
Michel Raynaud. Anneaux locaux hens\' e liens . Lecture Notes in Mathematics, 169. Springer, Berlin, 1970. doi:10.1007/BFb0069571
1970 doi
-
[11]
Constructive commutative algebra: projective modules over polynomial rings and dynamical Gr \"o bner bases
Ihsen Yengui. Constructive commutative algebra: projective modules over polynomial rings and dynamical Gr \"o bner bases . Lecture Notes in Mathematics, 2138. Springer, Cham, 2015. doi:10.1007/978-3-319-19494-3
2015 doi
Reviewed August 12, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.