Asserting ℤ[(1 + √(-19))/2] forms a principal ideal domain

Stream: new members

[Isak Colboubrani]

I want to assert that ℤ[(1 + √(-19))/2] forms a principal ideal domain (PID):

import Mathlib
example : IsPrincipalIdealRing [something] := by infer_instance
example : IsDomain [something] := by infer_instance

… or even better …

import Mathlib
example : IsPrincipalIdealRing [something] ∧ IsDomain [something] := by infer_instance

What is the idiomatic way to express ℤ[(1 + √(-19))/2]?

[Daniel Weber]

I think you should use docs#AdjoinRoot.instNumberFieldRat with X^2 - X + 5

[Daniel Weber]

Ah, you want the extension of Z. That's the ring of integers of that number field, isn't it?

[Daniel Weber]

Or you can use docs#AdjoinRoot directly on Z

[Isak Colboubrani]

Thank you!

Is AdjoinRoot ((X ^ 2 - X + 5) : ℤ[X]) the correct formulation for the ring ℤ[(1 + √(-19))/2] ?

Additionally, is it correct that AdjoinRoot ((X ^ 2 - X + 5) : ℤ[X]) is shorthand for the quotient ring ℤ[X] ⧸ Ideal.span {((X ^ 2 + 5) : ℤ[X])}?

[Isak Colboubrani]

These fail:

import Mathlib
open Polynomial
noncomputable example : IsDomain (AdjoinRoot ((X ^ 2 - X + 5) : ℤ[X])) := by infer_instance
-- failed to synthesize: IsDomain (AdjoinRoot (X ^ 2 - X + 5))
noncomputable example : IsDomain (ℤ[X] ⧸ Ideal.span {((X ^ 2 + 5) : ℤ[X])}) := by infer_instance
-- failed to synthesize: IsDomain (ℤ[X] ⧸ Ideal.span {X ^ 2 + 5})

In contrast, the following examples work as expected:

import Mathlib
open Polynomial
noncomputable example : NonUnitalRing (AdjoinRoot ((X ^ 2 - X + 5) : ℤ[X])) := by infer_instance
noncomputable example : Ring (AdjoinRoot ((X ^ 2 - X + 5) : ℤ[X])) := by infer_instance
noncomputable example : CommRing (AdjoinRoot ((X ^ 2 - X + 5) : ℤ[X])) := by infer_instance
noncomputable example : NonUnitalRing (ℤ[X] ⧸ Ideal.span {((X ^ 2 + 5) : ℤ[X])}) := by infer_instance
noncomputable example : Ring (ℤ[X] ⧸ Ideal.span {((X ^ 2 + 5) : ℤ[X])}) := by infer_instance
noncomputable example : CommRing (ℤ[X] ⧸ Ideal.span {((X ^ 2 + 5) : ℤ[X])}) := by infer_instance

What steps do I need to take to convince Lean/Mathlib that these are domains?

[Damiano Testa]

This would work for the first example: not inferInstance, but not long either:

noncomputable example (hf : Prime ((X ^ 2 - X + 5) : ℤ[X])) : IsDomain (AdjoinRoot ((X ^ 2 - X + 5) : ℤ[X])) :=
  AdjoinRoot.isDomain_of_prime hf

You still have to prove that the polynomial is Prime, though.

[Kevin Buzzard]

I think we should have a general degree two extension of an arbitrary commutative ring R, with data given by a and b via R[X]/(X^2-aX-b) (but implemented as two elements of R)

[Riccardo Brasca]

I also agree we need some sort of general theory of quadratic fields

[Michael Stoll]

Quadratic rings! (Of which quadratic fields will be a special case...)

[Riccardo Brasca]

Yes sorry