Note on the coincidence of two henselisations

TL;DR

This paper provides a constructive proof demonstrating the isomorphism between two henselisations of a residually discrete valuation domain, clarifying an implicit assumption in the literature.

Contribution

It offers the first explicit proof of the isomorphism, bridging a gap between classical and constructive mathematics in valuation theory.

Findings

Constructive proof of the isomorphism

Clarification of a previously implicit assumption

Bridging classical and constructive approaches

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.