Z[(1+sqrt(1+4k))/2]

Stream: Is there code for X?

[Kenny Lau]

we have Zsqrtd d for $\Bbb Z[\sqrt d]$, but do we have $\Bbb Z\left[\frac{1+\sqrt{1+4k}}2\right]$? This seems useful.
if there's not, i don't mind doing it

[Kevin Buzzard]

What we should have is QuadraticAlgebra R a b := $R[X]/(X^2-aX-b)$ defined as a two-field structure. This is what Bourbaki does.

[Kenny Lau]

well, i think we can still have the special case R=Z

[Andrew Yang]

We could just develop API over docs#AdjoinRoot via docs#AdjoinRoot.powerBasis' and not define a separate type.
...unless one cares about computability.

[Aaron Liu]

I care about computability

[Kenny Lau]

I care about computability

[Kevin Buzzard]

But as for QuadraticAlgebra you can mimic QuaternionAlgebra which was recently redone to be the same as Bourbaki. You should do it in the general case and then make notation or whatever for the $\Z$ case.

[Kenny Lau]

If anyone is interested in doing this:

[Kenny Lau]

import Mathlib

universe u

/-- `R[X]/(X^2−a*X−b)` -/
@[ext]
structure QuadraticAlgebra (R : Type u) (a b : R) : Type u where
  re : R
  im : R

namespace QuadraticAlgebra

variable {R : Type u} [CommSemiring R] {a b : R}

def ofInt (n : R) : QuadraticAlgebra R a b :=
  ⟨n, 0⟩

theorem ofInt_re (n : R) : (ofInt n : QuadraticAlgebra R a b).re = n :=
  rfl

theorem ofInt_im (n : R) : (ofInt n : QuadraticAlgebra R a b).im = 0 :=
  rfl

/-- The zero of the ring -/
instance : Zero (QuadraticAlgebra R a b) :=
  ⟨ofInt 0⟩

@[simp]
theorem zero_re : (0 : QuadraticAlgebra R a b).re = 0 :=
  rfl

@[simp]
theorem zero_im : (0 : QuadraticAlgebra R a b).im = 0 :=
  rfl

/-- The one of the ring -/
instance : One (QuadraticAlgebra R a b) :=
  ⟨ofInt 1⟩

@[simp]
theorem one_re : (1 : QuadraticAlgebra R a b).re = 1 :=
  rfl

@[simp]
theorem one_im : (1 : QuadraticAlgebra R a b).im = 0 :=
  rfl

instance : Add (QuadraticAlgebra R a b) :=
  ⟨fun z w => ⟨z.1 + w.1, z.2 + w.2⟩⟩

@[simp]
theorem add_re (z w : QuadraticAlgebra R a b) : (z + w).re = z.re + w.re :=
  rfl

@[simp]
theorem add_im (z w : QuadraticAlgebra R a b) : (z + w).im = z.im + w.im :=
  rfl

instance : Mul (QuadraticAlgebra R a b) :=
  ⟨fun z w => ⟨z.1 * w.1 + b * z.2 * w.2, z.1 * w.2 + z.2 * w.1 + a * z.2 * w.2⟩⟩

@[simp]
theorem mul_re (z w : QuadraticAlgebra R a b) :
    (z * w).re = z.re * w.re + b * z.im * w.im :=
  rfl

@[simp]
theorem mul_im (z w : QuadraticAlgebra R a b) :
    (z * w).im = z.re * w.im + z.im * w.re + a * z.im * w.im :=
  rfl

instance addCommMonoid : AddCommMonoid (QuadraticAlgebra R a b) := by
  refine
  { add := (· + ·)
    zero := 0
    nsmul n z := ⟨n • z.1, n • z.2⟩
    add_assoc := ?_
    zero_add := ?_
    add_zero := ?_
    add_comm := ?_
    nsmul_zero := ?_
    nsmul_succ := ?_ } <;>
  intros <;>
  ext <;>
  simp [add_comm, add_left_comm, add_mul]

instance addMonoidWithOne : AddMonoidWithOne (QuadraticAlgebra R a b) :=
  { QuadraticAlgebra.addCommMonoid with
    natCast := fun n => ofInt n
    natCast_zero := by ext <;> simp [ofInt_re, ofInt_im]
    natCast_succ := fun n => by
      ext <;> simp [ofInt_re, ofInt_im, Nat.succ_eq_add_one]
    one := 1 }

instance commSemiring : CommSemiring (QuadraticAlgebra R a b) := by
  refine
  { addMonoidWithOne with
    mul := (· * ·)
    npow := @npowRec (QuadraticAlgebra R a b) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ } <;>
  intros <;>
  ext <;>
  simp <;>
  ring

end QuadraticAlgebra

[Kenny Lau]

I basically copied Zsqrtd with adjustments

[Kenny Lau]

could be a nice project

[Eric Wieser]

Perhaps dump it in a PR and mark please-adopt?

[Kenny Lau]

it's interesting that we have quaternion algebra but not quadratic ring

[Kenny Lau]

Eric Wieser said:

Perhaps dump it in a PR and mark please-adopt?

https://github.com/leanprover-community/mathlib4/pull/25223

[Kevin Buzzard]

It's just a historical quirk, the reason we have quaternion algebras in the right generality and not quadratic algebras.

[Notification Bot]

45 messages were moved from this topic to #mathlib4 > Why is `Polynomial` noncomputable? by Eric Wieser.

[Eric Wieser]

(I think there are probably good reasons to develop QuadraticAlgebra irrespective of what happens with Polynomial, so lets not drown this thread; for one, they could replace GaussianInt)

[Kevin Buzzard]

We could also do classification of integers of quadratic number fields

[Alex J. Best]

We used QuadraticRing in lean 3 in https://arxiv.org/abs/2209.15492 perhaps it can be of some inspiration