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