Projects: Quadratic Integers

Stream: ItaLean 2025

[Pietro Monticone]

This thread is dedicated to the Quadratic Integers project:

• Repository: https://github.com/pitmonticone/QuadraticIntegers
• Informal & Formal Manager: @Riccardo Brasca

[Riccardo Brasca]

There is a typo in both main theorems (sorry...)

theorem d_2_or_3 (hd : d ≡ 2 [ZMOD 4] ∨ d ≡ 3 [ZMOD 4]) : IsIntegralClosure ℤ R K := by
  sorry

should be

theorem d_2_or_3 (hd : d ≡ 2 [ZMOD 4] ∨ d ≡ 3 [ZMOD 4]) : IsIntegralClosure R ℤ K := by
  sorry

and similarly for the other one.

[Riccardo Brasca]

Thanks @Pietro Monticone for spotting this (using aristotle, that was actually able to prove that previous version is false)

[Pietro Monticone]

Riccardo Brasca said:

theorem d_2_or_3 (hd : d ≡ 2 [ZMOD 4] ∨ d ≡ 3 [ZMOD 4]) : IsIntegralClosure R ℤ K := by

Fixed in main.

[Riccardo Brasca]

The issue we discovered with QuadraticAlgebra has been fixed in #32797, which is now included in the latest version of mathlib. In my opinion, this is already a success for our project!

For those interested, here is a brief explanation of the problem. Given any field K of characteristic zero, there are canonical maps ℕ → K, ℤ → K, and ℚ → K, which, for example, send 3 to $1_K + 1_K + 1_K$. On paper, we simply write 3, and if we need it to be an element of K we apply this map implicitly (for instance, we write 3 + x, where x : K).

In Lean, these maps exist and are called coercions. Lean inserts them automatically, allowing us to do mathematics as usual. You can still see them in the infoview: if x : K and you write 3 + x, what actually appears is 3 + ↑x. The upward arrow indicates that a map has been applied, but this is usually something you can ignore—Lean has found it for you, and you can move on.

When QuadraticAlgebra was introduced, the authors decided to define the canonical map R → QuadraticAlgebra R a b as a coercion. Thus, if r : R and Lean expects a term of type QuadraticAlgebra R a b, one can simply write r rather than somemap r. Mathematically, this is just the canonical inclusion of R into the extension, so this choice seems reasonable.

The problem arises in the (very common) situation where R is ℚ and a and b are such that QuadraticAlgebra ℚ a b is a field (of characteristic zero). In this case, there are two maps ℚ → QuadraticAlgebra ℚ a b: one coming from the general coercion ℚ → K for fields of characteristic zero, and one coming from the algebra structure. Of course, these two maps are equal mathematically, but they are not equal by definition, and Lean cannot recognize this on its own.

In practice, this led to goals such as

↑x = ↑x

with x : ℚ, where rfl does not close the goal, because the two arrows actually correspond to different maps. While it is not difficult to prove that the two maps are equal, Lean repeatedly asks you to supply this proof, and the situation only worsens as the theory becomes more complicated.

In #32797, I removed the coercion R → QuadraticAlgebra R a b, and as a result this problem completely disappeared. The drawback is that one now has to write the map explicitly, but it is simply algebraMap—the standard map from R to an R-algebra A, and nothing specific to QuadraticAlgebra. Moreover, mathlib provides many lemmas and good automation to work with it effectively.

[Riccardo Brasca]

What made things even more confusing is that there was also another issue, and at first I did not realize that one group was encountering one problem while the other group was facing the other.

This second issue comes from the fact that QuadraticAlgebra R a b is, of course, always an R-algebra. In the situation discussed above, this means it is a ℚ-algebra. On the other hand, it is also a field of characteristic zero, and therefore again a ℚ-algebra. The problem is the same as above: these two structures are mathematically equal, but Lean fails to recognize this fact. This situation is what is known as a diamond.

There are general techniques to resolve such situations, but for various reasons it is very difficult to fix this particular diamond. As a result, I ended up adding a warning advising users of QuadraticAlgebra that, when working over ℚ, they will probably want to deactivate the instance stating that a field of characteristic zero is a ℚ-algebra. This way, Lean can find only a single ℚ-algebra structure on QuadraticAlgebra ℚ a b, and the ambiguity disappears.

Concretely, this is achieved by the line

attribute [-instance] DivisionRing.toRatAlgebra

at the beginning of our file.