Zsqrtd and adjoin

Stream: Is there code for X?

[Suzuka Yu]

Greetings! I wonder wether we have (or plan to build) certain connection between Zsqrtd and Algebra.adjoin? For instance, ℤ√d is isomorphic to Algebra.adjoin ℤ {(d : ℂ) ^ (1 / 2 : ℂ)}

[Suzuka Yu]

@loogle Zsqrtd, Algebra.adjoin

[loogle]

:shrug: nothing found

[Kevin Buzzard]

I doubt that's true if d is a square.

[Suzuka Yu]

Sorry but why it is not? I thought that when d is a square, (d : ℂ) ^ (1 / 2 : ℂ) would be an actual integer so Algebra.adjoin ℤ {(d : ℂ) ^ (1 / 2 : ℂ)} would be ⊥ : Subalgebra ℤ ℂ, which is basically ℤ, whereas ℤ√d should also be ℤ

[Johan Commelin]

docs#Zsqrtd

[Johan Commelin]

It looks like Zsqrtd always has rank 2. So it will be $\Z \times \Z$ when $d$ is a square.

[Suzuka Yu]

ahh, sorry I didn't think of that. Thanks for the correction! But when d is square free, would it be true?

[Kevin Buzzard]

Can you formalise your question?

[Kevin Buzzard]

And the answer to your revised question is still no because 1 is squarefree. The condition you want is "not a square"

[Suzuka Yu]

Sure! Thanks for reminding me, I'll exclude the situation where d is unit

import Mathlib

open Zsqrtd

variable {d : ℤ} (hd : Squarefree d) (hunit : ¬ IsUnit d) -- or (hnon : Nonsquare d.natAbs)?

example : ℤ√d ≃+* Algebra.adjoin ℤ {(d : ℂ) ^ (1 / 2 : ℂ)} := by
  sorry

[Kevin Buzzard]

"squarefree" isn't the opposite of "not a square". For example 12 is not a square and it's not squarefree either, and the theorem is true for 12. The theorem can also be true for units, for example -1, which is a unit but is not a square. The correct condition is nothing to do with units or squarefree or absolute values, the correct condition is "not a square".

[Kevin Buzzard]

Under this assumption you should prove that the min poly of d^{1/2} is X^2-d (using the not-a-square assumption to rule out linear factors) and then prove that both rings are isomorphic to Z[X]/(X^2-d).

[Suzuka Yu]

(sincerely apologize, feels like I'm making silly mistake all the time :pensive:

I've corrected my condition, and managed to calculate the minimal polynomial (min_polyz). Proving Algebra.adjoin is isomorphic to Z[X]/(X^2-d) is straightforward using minpoly.equivAdjoin, but is there an easy way to construct the other isomorphism? (Zsqrtd is isomorphic to Z[X]/(X^2-d))

import Mathlib

open Zsqrtd Polynomial PowerBasis Algebra

variable {d : ℤ} (hnon : ∀ x : ℤ, d ≠ x * x)

local notation "polyz" => X ^ 2 - C d
local notation: max "√[" i "]" =>  ((i : ℂ) ^ ((1 / 2) : ℂ))

private theorem polyz_natDegree : natDegree polyz = 2 := natDegree_X_pow_sub_C
private theorem polyz_Monic : Monic polyz := by monicity!

theorem integralz : IsIntegral ℤ √[d] := by
  refine ⟨polyz, ⟨polyz_Monic, ?_⟩⟩
  · simp only [algebraMap_int_eq, one_div, eq_intCast, eval₂_sub, eval₂_X_pow,
    Complex.cpow_ofNat_inv_pow]
    show d - eval₂ (Int.castRingHom ℂ) ((d : ℂ) ^ (2⁻¹ : ℂ)) (C d) = 0
    rw [eval₂_C, eq_intCast, sub_self]

private theorem min_polyz_dvd : minpoly ℤ √[d] ∣ X ^ 2 - C d := by
  refine minpoly.isIntegrallyClosed_dvd integralz ?_
  simp only [one_div, eq_intCast, map_sub, map_pow, aeval_X, Complex.cpow_ofNat_inv_pow,
    map_intCast, sub_self]

private theorem min_polyz_natDegree_le : (minpoly ℤ √[d]).natDegree ≤ 2 := by
  rw [← @polyz_natDegree d]
  exact natDegree_le_of_dvd min_polyz_dvd (X_pow_sub_C_ne_zero (Nat.zero_lt_two) d)

include hnon

theorem min_polyz_natDegree : (minpoly ℤ √[d]).natDegree = 2 := by
  refine le_antisymm min_polyz_natDegree_le ?_
  rw [minpoly.two_le_natDegree_iff (@integralz d)]
  rintro ⟨x, hx : (algebraMap ℤ ℂ) x = √[d]⟩
  have := hnon x
  apply_fun (· ^ 2) at hx
  simp only [algebraMap_int_eq, eq_intCast, one_div, Complex.cpow_ofNat_inv_pow] at hx
  norm_cast at hx
  rw [← hx, sq] at this
  exact False.elim <| this rfl

theorem min_polyz : minpoly ℤ √[d] = polyz := by
  refine (eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic integralz)
    polyz_Monic min_polyz_dvd ?_).symm
  rw [polyz_natDegree, min_polyz_natDegree hnon]

noncomputable def equiv₁ :
    AdjoinRoot (minpoly ℤ √[d]) ≃ₐ[ℤ] Algebra.adjoin ℤ {√[d]} :=
  minpoly.equivAdjoin integralz

def equiv₂ : ℤ√d ≃ₐ[ℤ] AdjoinRoot polyz := sorry

[Suzuka Yu]

Or should I try directly build the isomorphism via power basis on Algebra.adjoin?

[Junyan Xu]

Maybe you can try to use IsAdjoinRoot.aequiv

[Suzuka Yu]

Thanks for the advice! I'll look into it

[Edison Xie]

would this be better after we refactor Zsqrtd? @Kevin Buzzard

[Kevin Buzzard]

Zsqrtd is a model for $\Z[X]/(X^2-d)$ even for d a square. My proposal was to replace it by $R[X]/(X^2-aX-b)$ for a general commutative ring R and elements a,b in R.