Search

Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some global-to-local results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field $\mathbb{Q}_p$ of $p$-adic numbers and of the field $\mathbb{F}_p(\!(X)\!)$ of Laurent series over $\mathbb{F}_p$ are local fields., Comment: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '24), Jan 2024, London, United Kingdom

Let $K/k$ be a finite Galois extension of global function fields. Let $E$ be a Drinfeld module over $k$. We state and prove an equivariant refinement of Taelman's analogue of the analytic class number formula for $(E,K/k)$, and derive explicit consequences for the Galois structure of the Taelman class group of $E$ over $K$., Comment: 41 pages

Let $K$ be a field complete with respect to a nonarchimedean real-valued norm, and let $L/K$ be an algebraic extension. We show that there is a unique norm on $L$ extending the given norm on $K$, with an explicit description. As an application, we extend the $p$-adic norm on the field $\mathbb{Q}_p$ of $p$-adic numbers to its algebraic closure $\mathbb{Q}_p^{\text{alg}}$, and we define the field $\mathbb{C}_p$ of $p$-adic complex numbers as the completion of the latter with respect to the $p$-adic norm. Building on the definition of $\mathbb{C}_p$, we formalize the definition of the Fontaine period ring $B_{\text{HT}}$ and discuss some applications to the theory of Galois representations and to $p$-adic Hodge theory. The results formalized in this paper are a prerequisite to formalize Local Class Field Theory, which is a fundamental ingredient of the proof of Fermat's Last Theorem., Comment: Accepted for the 14th International Conference on Interactive Theorem Proving (ITP 2023). 18 pages

The ring of ad\`eles of a global field and its group of units, the group of id\`eles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalized adic valuations on Dedekind domains. We present some applications, including the statement of the main theorem of global class field theory and a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its id\`ele class group., Comment: 15 pages

Fix positive integers $n,r,d$. We show that if $n,r,d$ satisfy a suitable inequality, then any smooth hypersurface $X\subset \mathbb{P}^n$ defined over a finite field of characteristic $p$ sufficiently large contains a rational $r$-plane. Under more restrictive hypotheses on $n,r,d$ we show the same result without the assumption that $X$ is smooth or that $p$ is sufficiently large., Comment: 8 pages

We provide explicit equations for moduli spaces of Drinfeld shtukas over the projective line with $\Gamma(N)$, $\Gamma_1(N)$ and $\Gamma_0(N)$ level structures, where $N$ is an effective divisor on $\mathbb{P}^1$. If the degree of $N$ is high enough, these moduli spaces are relative surfaces. We study some invariants of the moduli space of shtukas with $\Gamma_0(N)$ level structure for several degree $4$ divisors on $\mathbb{P}^1$., Comment: 21 pages

We compute rational points on genus $3$ odd degree hyperelliptic curves $C$ over $\mathbb{Q}$ that have Jacobians of Mordell-Weil rank $0$. The computation applies the Chabauty-Coleman method to find the zero set of a certain system of $p$-adic integrals, which is known to be finite and include the set of rational points $C(\mathbb{Q})$. We implemented an algorithm in Sage to carry out the Chabauty-Coleman method on a database of $5870$ curves., Comment: revisions to Section 2

Considering the sensitivity of both fatigue strength and corrosion rate to the surface characteristics, apposite surface treatments could address the related challenges for biodegradable magnesium-based materials. Herein, we treated the surface of a biocompatible magnesium alloy by a low cost and versatile severe plastic deformation technique, severe shot peening, to evaluate the potential of surface grain refinement to enhance functionality in biological environment. The evolution of surface grain structure and surface morphology were investigated using optical as well as scanning and transmission electron microscopy. Surface roughness, wettability and chemical composition, as well as in depth-microhardness and residual stress distribution, and corrosion resistance were investigated. Successive light surface grinding was used after severe shot peening to eliminate the effect of surface roughness and separately investigate the influence of grain refinement alone. Cytocompatibility tests with osteoblasts (or bone forming cells) were performed using sample extracts. Results revealed for the first time that severe shot peening can significantly enhance mechanical properties without causing adverse effects to the growth of surrounding osteoblasts. The corrosion behavior, on the other hand, was not improved by severe shot peening; nevertheless, slight grinding of the rough surface layer with a high density of crystallographic lattice defects, without removing the entire nanocrystallized layer, provided a good potential for improving corrosion characteristics after severe shot peening and thus, this method should be studied for a wide range of orthopedic applications in which biodegradable magnesium is used.