Zulip Chat Archive
Stream: new members
Topic: understanding Algebra.discr
Noah Anderson (Apr 01 2025 at 12:19):
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 (Apr 01 2025 at 12:34):
or perhaps more straightforward:
import Mathlib
variable (zbase : PowerBasis ℤ (Algebra.adjoin ℤ {Complex.I}))
example : Algebra.discr ℤ zbase.basis = - 4 := sorry
Kevin Buzzard (Apr 01 2025 at 22:22):
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 (Apr 02 2025 at 00:40):
Sorry, I forgot to open polynomial namespace, it should be working now
Suzuka Yu (Apr 06 2025 at 06:49):
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
Last updated: May 02 2025 at 03:31 UTC