Definition of IsAdjoinRoot

Stream: mathlib4

[Artie Khovanov]

Fix a ring extension $B/A$. Currently, IsAdjoinRoot B takes a parameter f : A[X] and means "$A$-isomorphism between $A[X]/\langle f\rangle$ and $B$."

The point of this object, as far as I understand, is to allow abstract reasoning about simple extensions $K[\alpha]$ without needing to commit to a particular model e.g. AdjoinRoot. In this sense it's similar to IsLocalization.

In practice I've found a couple problems with this definition:
(a) it creates data
(b) distinct parameters create the same data: multiply f by a constant

I want to change the definition to instead take a parameter x : B and mean "$x$ generates $B$ as an $A$-algebra."

This leads to the same definition over a field, since you can recover the minimal polynomial, and is also Prop-valued. I think this new definition is more flexible.

What are people's thoughts? Pinging @Anne Baanen as they wrote this file.

[Riccardo Brasca]

What if there no B?

[Riccardo Brasca]

What you describe already exists, it is Algebra.adjoin.

[Riccardo Brasca]

Or close to that.

[Artie Khovanov]

@Riccardo Brasca as I describe, IsAdjoinRoot takes B as a parameter in either case. To answer your question, you choose whatever model you want the defeqs for eg AdjoinRoot or QuadraticAlgebra. The point AIUI is to have a unified API for the models.

[Artie Khovanov]

And Algebra.adjoin is the construction, I am talking about the predicate!

[Riccardo Brasca]

Ah sorry, you are talking about IsAdjoinRoot, not AdjoinRoot.

[Riccardo Brasca]

The problem is that to make the link with AdjoinRoot you really want a polynomial. There is a rather long discussion about the actual implementation IIRC

[Artie Khovanov]

Could you link the discussion? That would be very useful to me in understanding how to extend IsAdjoinRoot.

[Artie Khovanov]

My thought was that you can recover the polynomial using minpoly the same way you recover the root from the image of X currently.

[Riccardo Brasca]

It seems I dreamed about the discussion

[Artie Khovanov]

To un-xy myself: I am formalising the algebraic proof of the fundamental theorem of algebra ("a real-closed field $R$ has algebraic closure $R[i]$"), which requires reasoning concretely about generic field extensions. So for instance you have an arbitrary finite extension K/R and then you prove it has degree 2 and then you prove it is in fact R[i]. The idiomatic way to do this in Lean, avoiding tons of isomorphisms, appears to be IsAdjoinRoot, but I've found myself having to repeat lots of boilerplate nonsense for the reasons I specified above.

[Andrew Yang]

I think the point of IsAdjoinRoot is about the polynomial itself? Is Algebra.adjoin R {x} = top not enough for you?

[Riccardo Brasca]

I agree with Andrew, both AdjoinRoot and IsAdjoinRoot are fundamentally about the polynomial.

[Artie Khovanov]

Andrew Yang said:

I think the point of IsAdjoinRoot is about the polynomial itself? Is Algebra.adjoin R {x} = top not enough for you?

I mean yes in principle, and I've already PRed the equivalence of these predicates. But I'm trying to avoid duplicating API. IsAdjoinRoot has all sorts of things defined on top of it.

[Andrew Yang]

In that case perhaps the solution is to generalize those APIs to only require Algebra.adjoin R {x} = top? Are there any concrete examples of such things?

[Kenny Lau]

image.png

I think orthogonal to all of the discussion above, one improvement that could be made is to just take the root instead of one whole map

[Artie Khovanov]

Andrew Yang said:

In that case perhaps the solution is to generalize those APIs to only require Algebra.adjoin R {x} = top? Are there any concrete examples of such things?

Yeah good shout actually. It is strictly more general (though equivalent over a field). I will do this and come back with a concrete proposal at some point in the future.

[Riccardo Brasca]

Another comment is that maybe (but this depends on precisely what you are doing), you should ignore $i$ and only use the polynomial $x^2+1$

[Artie Khovanov]

I'm not sure what this means, sorry. The $i$ above was just informal mathematical notation. But the proof I am formalising uses the data of the isomorphism and not just its existence, if that's what you mean?

[Riccardo Brasca]

Never mention any explicit root of $x^2+1$ in your argument. Like avoid saying that $\mathbb{C}$ is $\mathbb{R}[i]$, say that $\mathbb{C}$ is $\mathbb{R}[X]/(X^2+1)$

[Artie Khovanov]

Oh also a related issue: currently I have to write something like Nonempty (IsAdjoinRoot K (X^2 - (C -1))) rather than IsAdjoinRoot K (X^2 + 1) because of the predicate being data and not a proposition. I'm not sure this is really fixable though.

[Kenny Lau]

Riccardo Brasca said:

Never mention any explicit root of $x^2+1$ in your argument. Like avoid saying that $\mathbb{C}$ is $\mathbb{R}[i]$, say that $\mathbb{C}$ is $\mathbb{R}[X]/(X^2+1)$

that seems impossible without picking out which element in C corresponds to X

[Kenny Lau]

Artie Khovanov said:

Nonempty (IsAdjoinRoot

we could make this into a definition called IsIsAdjoinRoot

[Andrew Yang]

I think the solution is to make it take in an element of K as well, like IsAdjoinRoot i (X^2 + 1) instead of IsAdjoinRoot C (X^2 + 1), and then make it prop valued.

[Riccardo Brasca]

Well, it should be the definition of $\mathbb{C}$!

[Artie Khovanov]

Riccardo Brasca said:

Never mention any explicit root of $x^2+1$ in your argument. Like avoid saying that $\mathbb{C}$ is $\mathbb{R}[i]$, say that $\mathbb{C}$ is $\mathbb{R}[X]/(X^2+1)$

What do you mean by is here? If it's an isomorphism, then $i$ is just the image of $X$. And it's much easier to reason about an element of my field satisfying some equation than it is to carry proofs along isomorphisms - that's the whole reason we have this IsAdjoinRoot pattern in the first place!

[Kenny Lau]

Artie Khovanov said:

What do you mean by is here?

Bill Clinton would be proud

[Artie Khovanov]

Andrew Yang said:

I think the solution is to make it take in an element of K as well, like IsAdjoinRoot i (X^2 + 1) instead of IsAdjoinRoot C (X^2 + 1).

This is unsatisfactory because you want the conclusion of the theorem I mentioned to be something like IsAdjoinRoot K (X^2+1) and not exists x. IsAdjoinRoot x (X^2+1). I think on reflection we do need both views (via the root, and via the poly).

[Riccardo Brasca]

I don't know what you are proving precisely, so it's difficult to answer, but I am saying something like

import Mathlib

open Polynomial

example : IsAdjoinRoot (AlgebraicClosure ℝ) (X^2 + 1 : ℝ[X]) := by
  sorry

[Kenny Lau]

Riccardo, that structure requires choosing a root

[Andrew Yang]

I'm not entirely sure why exists x. IsAdjoinRoot x (X^2+1) is bad. Is it a usability concern or an aesthetical one?

[Artie Khovanov]

Riccardo Brasca said:

Well, it should be the definition of $\mathbb{C}$!

I think the definition of \bbC should be via QuadraticAlgebra. But in any case, sometimes we have to start from an abstract field extension and conclude that it has some concrete form. In that case you can't simply redefine things to use AdjoinRoot. Indeed I thought that was the whole point of having an abstraction like IsAdjoinRoot?

[Aaron Liu]

fortunately AlgebraicClosure gives you roots of polynomials of degree n indexed by Fin n

[Riccardo Brasca]

Well quadratic algebras exist since like two months, and the complex numbers are a bit older. Anyway you may also avoid AdjointRoot entirely if it is unsuitable for your work and use IsSplittingField, or whatever.

[Artie Khovanov]

Andrew Yang said:

I'm not entirely sure why exists x. IsAdjoinRoot x (X^2+1) is bad. Is it a usability concern or an aesthetical one?

hm good question
it's certainly less aesthetic
it's basically extra redundant data on top of "Algebra.adjoin {x} = top"
it just means "exists x. Algebra.adjoin {x} = top and minpoly R x = X^2+1"

[Artie Khovanov]

Riccardo Brasca said:

Well quadratic algebras exist since like two months, and the complex numbers are a bit older. Anyway you may also avoid AdjointRoot entirely if it is unsuitable for your work and use IsSplittingField, or whatever.

I'm sorry, I don't understand. An isomorphism with AdjoinRoot is a choice of root. And I don't want a splitting field (though it's equivalent here, sure), I want to capture this fact, which is equivalent to both "x generates K as an R algebra" and "K is isomorphic to R[X]/(minpoly x)"

[Andrew Yang]

I think this is the point? IsAdjoinRoot x (X^2+1) should just be a wrapper for Algebra.adjoin {x} = top and R[X] -> S has kernel {X^2+1}.

[Artie Khovanov]

Alright the first thing I'll do is generalise the IsAdjoinRoot stuff to "adjoin = top" and see how that makes my proofs look. If that's an improvement then I can come back to thinking about this. Thanks all!

[Andrew Yang]

And also note that this minpoly trick to recover the poly only works when you are in a field or at least an integrally closed domain.

[Artie Khovanov]

Yes indeed - but that's also the only place most of the API holds!

[Riccardo Brasca]

@Artie Khovanov the point is that often if someone finds the current API very annoying to use is because they are using it in the wrong way, so before changing a def we prefer to be sure it's not the case.
I am not saying you are doing things in the wrong way, I haven't used IsAdjoinRoot a lot, but please consider that if a definition is painful to use it may be that you are doing something wrong.

[Riccardo Brasca]

Having said that it's completely possible the actual code is not the best one, and all contributions are very welcome!

[Artie Khovanov]

Like mathematically speaking we never want to reason about "an A-algebra map from A[X] onto B with a principal kernel" without caring about the image of X

[Riccardo Brasca]

Well, I would say exactly the opposite: I usually don't want to fix the root!

[Artie Khovanov]

Riccardo Brasca said:

Artie Khovanov the point is that often if someone finds the current API very annoying to use is because they are using it in the wrong way, so before changing a def we prefer to be sure it's not the case.
I am not saying you are doing things in the wrong way, I haven't used IsAdjoinRoot a lot, but please consider that if a definition is painful to use it may be that you are doing something wrong.

I am no longer proposing changing the definition, at least for now. I've said I'm going to try generalising some results and see if that cleans up my proofs.

[Kenny Lau]

Riccardo Brasca said:

Well, I would say exactly the opposite: I usually don't want to fix the root!

I think the two paragraphs of yours are saying opposite things, because IsAdjoinRoot does require fixing a root

[Artie Khovanov]

Riccardo Brasca said:

Well, I would say exactly the opposite: I usually don't want to fix the root!

I'm not saying in terms of the external definition, I'm saying internally - the specialisation to principal kernels is not mathematically meaningful. I was responding to @Andrew Yang's point that we can't always recover a minpoly.

[Artie Khovanov]

Kenny Lau said:

Riccardo Brasca said:

Well, I would say exactly the opposite: I usually don't want to fix the root!

I think the two paragraphs of yours are saying opposite things, because IsAdjoinRoot does require fixing a root

I think the point is that we don't want to introduce the root explicitly, which is totally fair. But yes it is necessarily there in the data.

[Riccardo Brasca]

Kenny Lau said:

Riccardo Brasca said:

Well, I would say exactly the opposite: I usually don't want to fix the root!

I think the two paragraphs of yours are saying opposite things, because IsAdjoinRoot does require fixing a root

Oh yeah, this shows that I am really not used to IsAdjoinRoot :sweat_smile:

[Artie Khovanov]

Indeed the fact it's data is the whole problem! The name IsAdjoinRoot is misleading in this sense because it implies that it's just a predicate when it isn't.

[Artie Khovanov]

What I hope to gain from generalising to "this element is a generator" is in part that I have a predicate and so I'm no longer in defeq hell.

[Riccardo Brasca]

Ok, I actually read the code and I don't have a real opinion about the actual implementation, but the name is no misleading that there are surely results that use IsAdjoinRoot and actually only use the existence of the isomorphism, and this is surely a problem.

[Riccardo Brasca]

It should be clearly explained that IsAdjoinRoot generalize AdjoinRoot to avoid defeq hell, not to actually forget data. Sorry for all the noise.

[Artie Khovanov]

IsAdjoinRoot is just saying the isomorphism exists. Are you drawing a distinction between data and prop here?

[Artie Khovanov]

Oh sorry just saw your second message yeah

[Riccardo Brasca]

Currently IsAdjoinRoot is the isomorphism rather than its existence (bundled in some way).

[Riccardo Brasca]

In particular it's not at all like IsLocalization.

[Artie Khovanov]

And yes there are results like "the degree of L/K where IsAdjoinRoot L f is deg f" that don't use the choice of root but rather just the existence of some isomorphism. I see what you thought IsAdjoinRoot said.

I think it should say what you thought it said, and then the whole API should be generalised to "Algebra.adjoin {x} = \top" and in particular implemented in IsAdjoinRoot using choice.

[Kenny Lau]

yeah and that's because every localisation is an epimorphism

[Aaron Liu]

well with localizations there's no choice

[Aaron Liu]

it's not like roots where you can choose a different root

[Kenny Lau]

let me reassert the idea IsIsAdjoinRoot

[Aaron Liu]

localizations have a universal property

[Andrew Yang]

Do we actually need the data carrying version if we have the prop valued version?

[Riccardo Brasca]

We should think if we want both versions

[Kenny Lau]

the "lfiting" one requires data

[Kenny Lau]

IsAdjoinRoot.lift

[Andrew Yang]

It only requires the existence of data.

[Kenny Lau]

well the lift depends on the choice of root anyways

[Kenny Lau]

Andrew Yang said:

It only requires the existence of data.

the existence of lift only requires the existence of data

[Artie Khovanov]

Andrew Yang said:

Do we actually need the data carrying version if we have the prop valued version?

Yes because we want to prove results about the actual root sometimes. But we should generalise that to a predicate on the root ("adjoin {x} = top") and leave IsAdjoinRoot to results that don't care about the choice of root (eg the degree of the extension).

[Riccardo Brasca]

This is just the universal property of polynomials and of the quotient

[Aaron Liu]

You can't compute it without the data

[Aaron Liu]

Polynomials have a different kind of universal property

[Kenny Lau]

Riccardo Brasca said:

universal property of polynomials

which has data

[Artie Khovanov]

In pseudocode
"IsPrimitiveElement K (x : L) := (adjoin K {x} = top)"
"IsAdjoinRoot L (f : K[X]) := exists (F : AlgHom K K[X] L). F.surjective and F.ker = <f>"

[Kenny Lau]

again I propose that we should take the root instead of the whole map

[Artie Khovanov]

sure

[Andrew Yang]

Sure I can agree with this. But my question is do we still need the current docs#IsAdjoinRoot ?

[Artie Khovanov]

"IsAdjoinRoot L (f : K[X]) := exists x : L. IsPrimitiveElement K x and (all g : K[X]. aeval g x = 0 iff f | g)"

[Artie Khovanov]

or something

[Riccardo Brasca]

I mean that one can write IsAdjoinRoot.lift only assuming the existence of h (I am personally not interested in computability). Of course it will be an arbitrary choice, it will not be unique

[Artie Khovanov]

Andrew Yang said:

Sure I can agree with this. But my question is do we still need the current docs#IsAdjoinRoot ?

Under this proposal the results from that file mostly go to IsPrimitiveElement with the few that don't mention the root specialised to the new IsAdjoinRoot using choice

[Artie Khovanov]

Question: when do we actually use IsAdjoinRoot.lift? The only way I've really used IsAdjoinRoot "externally" is to specify the degree of the extension and transfer instances from AdjoinRoot. Maybe I'm missing something.

[Kenny Lau]

I don't use IsAdjoinRoot either

[Riccardo Brasca]

I think one use could be to make AdjoinRoot an opaque definition and prove everything via IsAdjoinRoot, so it's impossible to abuse defeq

[Andrew Yang]

I think that would be quite painful.

[Riccardo Brasca]

But the file starts with "This file defines a predicate..." and this should surely be changed.

[Kenny Lau]

Riccardo Brasca said:

AdjoinRoot an opaque definition and prove everything via IsAdjoinRoot

the philosophy of Localization and IsLocalization, and also RingHom vs. RingHomClass, is that we need both API

[Kenny Lau]

Riccardo Brasca said:

But the file starts with "This file defines a predicate..."

But this has nothing to do with AdjoinRoot

[Riccardo Brasca]

Well, this is slightly different, since there are actually three versions: AdjointRoot, "something fixing the isomorphism" (currently IsAdjoinRoot), and something where we say there is an isomorphism.

[Kenny Lau]

AdjointRoot, which is the concrete construction, should not be part of this discussion at all, it is entirely irrelevant

[Kevin Buzzard]

We have AlgebraicClosure and IsAlgClosure, and AlgebraicClosure is not unique up to unique isomorphism, so this is a better analogue than Localization and IsLocalization. I am very surprised something called Is isn't a Prop. I argued hard that IsROrC should be renamed for this reason, and it was.

[Artie Khovanov]

Yeah that's a better analogue (and in principle supports my revised proposal)

[Artie Khovanov]

Relevant file I found: Mathlib.RingTheory.Adjoin.PowerBasis

[Artie Khovanov]

Am trying now to translate the IsAdjoinRoot stuff to

structure IsPrimitiveElem (R : Type*) {S : Type*} [CommRing R] [Ring S] [Algebra R S]
    (x : S) : Prop where
  is_integral : IsIntegral R x
  adjoin_eq_top : Algebra.adjoin R {x} = ⊤

[Artie Khovanov]

I have gone ahead and made a design to make IsAdjoinRoot and PowerBasis into predicates
See #mathlib4 > Should `PowerBasis` take a parameter