Norm in quadratic extension

Stream: Is there code for X?

[Edison Xie]

I'm currently working with quadratic extension of ℚ, namely ℚ(√a), however the method I used to construct it is by Algebra.adjoin ℚ (√a) and working with this is really hard since lean doesn't even know this is a fieldso my first question is how to express the element in ℚ(√a) as x + y *√a? And how do I tell lean that norm in quadratic extension of ℚ is precisely x^2 - ay^2?

[Riccardo Brasca]

Writing down a definition is a subtle problem. What are you goals?

[Riccardo Brasca]

Mathematically Algebra.adjoin ... is of course what you think it is, but I would strongly suggest to use what we call a "characteristic predicate" rather than a concrete definition.

[Riccardo Brasca]

By this I mean introduce something like IsQuadratric a on a field K.

[Riccardo Brasca]

You can have a look at how cyclotomic fields are set up in mathlib to have an idea.

[Edison Xie]

Riccardo Brasca said:

Writing down a definition is a subtle problem. What are you goals?

I've got two goals: 1.express all element in Q(sqrt(a)) in the form of x + y sqrt(a) and 2. show that Algebra.norm in the quadratic extensions are just (x + y sqrt(a))*(x - y sqrt(a))

[Edison Xie]

Riccardo Brasca said:

You can have a look at how cyclotomic fields are set up in mathlib to have an idea.

thanks for the tips

[Riccardo Brasca]

For a more elementary approach you can follow docs#Zsqrtd

[Riccardo Brasca]

BTW I think we really want the theory of quadratic fields in mathlib (it is ridiculous that we have cyclotomic fields and not quadratic fields).

[Edison Xie]

Riccardo Brasca said:

BTW I think we really want the theory of quadratic fields in mathlib (it is ridiculous that we have cyclotomic fields and not quadratic fields).

Yeah I know! It's really annoying!

[Kevin Buzzard]

Bourbaki develop the theory of quadratic algebras; given a commring R and two elements a,b, we can define R[a,b] to be R[X]/(X^2-(aX+b)). This can be used to make extensions by zero, quadratic fields, orders in them etc etc.