understanding Algebra.discr

Stream: new members

[Noah Anderson]

I didn't quite understand how to calculate Algebra.discr. It seems to have a different definition compared to whats on a regular undergraduate textbook?

For example:

import Mathlib

open Polynomial

variable {d : ℂ} {d' : ℤ} (zbase : PowerBasis ℤ (Algebra.adjoin ℤ {d}))
         (hzbase : zbase.dim = 2) (hd : d' = d ^ 2)

def gen : Algebra.adjoin ℤ {d} :=
  ⟨d, SetLike.mem_coe.1 <| Algebra.subset_adjoin <| Set.mem_singleton d⟩

lemma gen_eq : gen = zbase.gen :=
  sorry -- solved

lemma aux₀ : minpoly ℤ (@gen d) = X ^ 2 - C d' :=
  sorry -- solved

lemma aux₁ (x : Algebra.adjoin ℤ {d}) : ∃ r s : ℤ, x = r + s * (@gen d) := by
  sorry -- solved

#check Algebra.discr ℤ zbase.basis
-- ↑ how to convert it to the "elementary form" ?
-- that is, the conjugate of `gen` is `- gen`, then we have two morphisms:
-- `σ₁ : r + s * gen ↦ r + s * gen`
-- `σ₂ : r + s * gen ↦ r + s * (- gen)`
-- and the discriminant would be the square of the determinant of `!![1, gen; 1, - gen]`

[Noah Anderson]

or perhaps more straightforward:

import Mathlib

variable (zbase : PowerBasis ℤ (Algebra.adjoin ℤ {Complex.I}))

example : Algebra.discr ℤ zbase.basis = - 4 := sorry

[Kevin Buzzard]

Can you ask your question as a #mwe ? Your code doesn't compile for me, even after adding import Mathlib at the top.

[Noah Anderson]

Sorry, I forgot to open polynomial namespace, it should be working now

[Suzuka Yu]

If this still interests you, I wrote something on the discriminate of quadratic extension (also under your notation).
I am pretty sure it is not welly written, but hopefully might provides you with some ideas on how to break the discriminate down:

https://github.com/Yu-Misaka/Lean-Example/blob/main/LeanExample/QuadraticExtension.lean