# The ring of integers of a cyclotomic field

In PR #13585 we compute the discriminant of cyclotomic fields. This is an important result, usually treated in a first year graduate course in number theory. In this post we would like to explain why it is an important result, and briefly explain how we proved it.

Number fields, finite extensions of $\mathbb{Q}$, are fundamental objects in modern number theory. To give a simple application, let us consider the equation $x^2 + 2 = y^3$, where we are looking for integer solutions. It's not easy to treat this equation directly in $\mathbb{Z}$, since the left hand side is irreducible. On the other hand, working in $\mathbb{Q}(\sqrt{-2})$ (the finite extension of $\mathbb{Q}$ obtained adding a root of $x^2 + 2$), the equation becomes $(x + \sqrt{-2})(x - \sqrt{-2}) = y^3$. We have now written a cube as a product and we can study the relations between the prime factors of the left and of the right hand side. One problem is that $\mathbb{Q}(\sqrt{-2})$ is a field, so there is no useful notion of prime factors. The idea is that the same decomposition holds in $ℤ[\sqrt{-2}]$ (the smallest subring of $\mathbb{C}$ containing $\sqrt{-2}$). This is a ring that "looks like $\mathbb{Z}$" (to be precise it is a euclidean domain), where we can do arithmetic and solve the equation (whose only solution is $x = \pm 5$ and $y = 3$).

In the flt-regular project we consider the equation $x ^ p + y ^ p = z ^ p$ over $ℤ$, where $p$ is a (regular, but this is irrelevant for our discussion) prime. The natural idea is to consider the cyclotomic field $\mathbb{Q}(\zeta_p)$ and the ring $\mathbb{Z}[\zeta_p]$, where $\zeta_p$ is a primitive $p$-th root of unity, to write $$x ^ p + y ^ p = (x + y)(x + \zeta_p y)\cdots(x + \zeta_p ^ {p - 1}).$$ This was indeed the original ideal to tackle Fermat's last theorem, and it can be seen as the birth of algebraic number theory. Since we want to study prime factorizations in $\mathbb{Z}[\zeta_p]$, we need to know that this ring is well behaved. For example, when it is a unique factorization domain, the equation can be completely solved. Unfortunately, this rarely happens, but we can replace unique factorization of elements by unique factorization of ideals, a property that holds in any Dedekind domain. In particular we need to know that $\mathbb{Z}[\zeta_p]$ is a Dedekind domain.

Mathlib already knows quite a lot about Dedekind domains. For example, it knows that the ring of integers of any number field is such a domain. Given $K$ a number field, its ring of integers $\mathcal{O}_K$ is the set of elements of $K$ that are root of a monic polynomial with integers coefficients. If $K = \mathbb{Q}(\alpha)$, with $\alpha$ an algebraic integer, then $\mathbb{Z}[\alpha] \subseteq \mathcal{O}_K$, but in general $\mathcal{O}_K$ can be bigger: for example if $\alpha = \sqrt{-3}$, then $\frac{1 + \sqrt{-3}}{2}$ is a root of $x^2 + x + 1$ and so it lies in $\mathcal{O}_K$, but not in $\mathbb{Z}[\alpha]$. In general, $\mathcal{O}_K$ is the "correct" ring to work with.

To be able to attack Fermat's Last theorem in the flt-regular project, we hence need to explicitly compute the ring of integers of $\mathbb{Q}(\zeta_p)$. It turns out that $\mathcal{O}_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p]$, as proved in PR #13585. This a nontrivial result, and it is a good demonstration that we can do serious algebraic number theory in mathlib.

We didn't want to prove the result in the fastest way, but we preferred to develop the theory organically, to pave the way for similar theorems. Here is a short account of what we did. The math proof we decided to follow is the following.

Since $\mathbb{Q}(\zeta_p) = \mathbb{Q}(\varepsilon_p)$ and $\mathbb{Z}[\zeta_p] = \mathbb{Z}[\varepsilon_p]$, where $\varepsilon_p = \zeta_p - 1$ and the minimal polynomial of $\varepsilon_p$ is Eiseinstein at $p$, the result immediately follows. We actually proved this for the $p ^ n$-cyclotomic field, but the strategy is essentially the same.

Beside results specific to cyclotomic fields, the most important part of this work is by far the introduction of the discriminant in mathlib. The computation of the discriminant of cyclotomic fields shows that we have enough API to treat, say, the case of quadratic extensions of $\mathbb{Q}$. Lastly, it should now be possible to connect it with ramification.

# This month in mathlib (May 2022)

In May 2022 there were 606 PRs merged into mathlib. We list some of the highlights below.

• Model theory

• PR #13980 proves that any theory with infinite models has arbitrarily large models
• PR #13723 and PR #13982 prove the Löwenheim–Skolem theorem
• Category theory and homological algebra

• PR #13882 proves that simple objects are indecomposable
• PR #13707 proves that a left rigid category is monoidal closed and that functors from a groupoid to a rigid category is again a rigid category.
• Homology is still making progress, both in concrete setups such as PR #12622 which develops the API for complexes of modules, and in abelian categories with PR #14009 bringing short exact sequences from the Liquid Tensor Experiment.
• In algebraic topology, PR #14304 defines the nerve of a category as a simplicial set.
• Algebra

• PR #13414 starts the study of torsion ideals. This is a step towards the long awaited classification of finite type modules over principal ideal domains, stay tuned!
• PR #13784 starts the formalization of Laurent Polynomials. Many more PRs followed or are on their way.
• The work to remove unneeded commutativity assumptions continued, in particular in PR #13966 and PR #13865.
• Matrices also got some work, both on the algebraic side with PR #13845 proving that invertible matrices over a ring with invariant basis number are square, and the analytical side with PR #13520 defining the matrix exponential. In order to make this easier to work with, mathlib now has two different normed algebra structures on matrices, the $L^\infty$ operator norm from PR #13518 and the frobenius norm from PR #13497.
• In representation theory, PR #13685 proves the category of Rep k G of representations of a group G on k-vector spaces is symmetric monoidal, and PR #13782 proves it is linear. PR #13740 introduces the category of finite dimensional representations.
• Number theory

• The general theory of Dedekind domains progressed with PR #13067 about the Chinese remainder theorem and PR #13462 which extends the v-adic valuation on a Dedekind domain to its field of fractions K and defines the completion of K with respect to this valuation, as well as its ring of integers, and provides some topological instances.
• On the concrete examples side, PR #13585 computes the ring of integers of a $p^ n$-th cyclotomic extension of $ℚ$.
• Functional analysis and geometry:

• PR #9862 finished the Banach-Alaoglu theorem.
• A long series of PRs culminated in PR #7288 proving several versions of the geometric Hahn Banach theorem.
• Also related to convexity, there had been progress on locally convex topological vector spaces, including PR #13547 characterizing the topology induced by seminorms in terms of neighborhoods of zero, and the introduction of uniformly convex normed spaces in PR #13480.
• The theory of vector bundles over topological spaces progressed with PR #14361 and PR #8545 building the pullback of a vector bundle under a continuous map.
• Integration theory and calculus

• PR #13540 defines the convolution of two functions. It proves that when one of the functions has compact support and is $C^n$ and the other function is locally integrable, the convolution is $C^n$ and its total derivative can be expressed as a convolution (this requires to generalize the usual notion of convolution which would be enough only for partial derivatives). This PR also proves that when taking the convolution with functions that "tend to the Dirac delta function", the convolution tends to the original function. This all comes from the sphere eversion project.
• PR #13179 proves comparison lemmas between finite sums and integrals.
• PR #14129 ensure that the asymptotic relations is_o/is_O work in calc blocks.
• Complex analysis

• PR #13178 proves the Phragmen-Lindelöf principle for some shapes in the complex plane.
• PR #13000 continues the study of the $\Gamma$ function, proving it is complex analytic (away from its poles at non-positive integrers of course).
• PR #12892 introduces torus integrals, paving the way towards the higher-dimensional Cauchy formula.
• Probability theory

• In elementary probabilities, PR #13484 use the counting measure to reformulate earliers contributions.
• PR #13630 proves the optional stopping theorem from martingale theory.
• After a long series of PRs including PR #13912 which defines the variance of a random variable, and proves its basic properties, and PR #14024 which defines identically distributed random variables, we finally got PR #13690 which proves the strong law of large numbers!

Note also that, with PR #14237 we finally completed the long quest to provide module docstring for all math files in mathlib.

# This month in mathlib (Apr 2022)

In April 2022 there were 661 PRs merged into mathlib. We list some of the highlights below.

# This month in mathlib (Mar 2022)

March 2022 saw a record number of new contributions to mathlib: 682 PRs were merged, obliterating the old record of 565 merged PRs.

# This month in mathlib (Feb 2022)

February 2022 saw 501 commits to mathlib. In this post we highlight some of these contributions.

About a month ago, the Cauchy integral theorem for some simple domains landed in mathlib. PR number 10000 was specially allocated for this occasion in advance. In this post I will recollect the events that led to this formalization.

# This month in mathlib (Jan 2022)

January 2022 saw 533 commits to mathlib. In this post we highlight some of these contributions.

# Backstage with Yakov Pechersky

The next installment in the series of backstage interviews with mathlib's active contributors!

Today, Johan Commelin interviews Yakov Pechersky. The first half of the interview's video was lost, so it was "recovered" via written communication.