Should `PowerBasis` take a parameter

Stream: mathlib4

[Artie Khovanov]

In my continued attempts to refactor IsAdjoinRootMonic to be easier to use, I have turned my attention to PowerBasis (which is logically equivalent but parameterised differently).
I have an idea to make PowerBasis into a Prop parameterised by its generating element. So, rather than "here is a power basis" - "this element generates a basis". My thought was this would make the definition more flexible.
Does anyone have any thoughts on this or any rationale for the original design for PowerBasis?

[Artie Khovanov]

@Anne Baanen tagging you as the original author of the file

[Andrew Yang]

I think one point of power basis is to contain the basis as data. I would suggest you to first develop the Prop valued analog, replace all the statements on PowerBasis that does not mention the basis to that predicate, and we will probably have a better idea about if we should remove PowerBasis or not.

[Artie Khovanov]

I have done / am doing this
what criteria should I be judging by?

[Anne Baanen]

The motivation for the original design was for the development of Dedekind domains, to have PowerBasis R S as a way to say S = R[α] without particularly caring about which α we have. But I suppose that just like IsAdjoinRoot we would like to control this α (and especially its defeqs) better, so I can certainly imagine that IsPowerBasis R S α n (or so) would be nicer in practice. Having to rewrite pb.gen = α and pb.dim = n all the time can get annoying :)

[Anne Baanen]

For places taking a powerbasis as hypothesis, I'd like to see a reduction in the number of rewrites of the form pb.gen = α and pb.dim = n, and for places returning a powerbasis as conclusion, I'd like to see more IsPowerBasis R S α n for specific α n than ∃ α n, IsPowerBasis R S α n.

[Artie Khovanov]

OK, I've now re-written the entire PowerBasis and IsAdjoinRoot API to depend on only the root/generator x as a parameter. My proposed design is the following:

Fix CommRing R, Ring S, Algebra R S, x : S. The situation where $S=R[x]\cong R[X]/\langle f\rangle$ is then described by

1. hx : IsPrimitiveElement R x : Prop, a predicate on x that then determines all other data: hx.basis, hx.ker_aeval_eq_span_minpoly, and so on.
2. hS : IsAdjoinRootMonic S (f : R[X]) : Prop, which is equivalent to ∃ x : S, IsPrimitiveElement R x ∧ minpoly R x = f. This allows you to talk about properties of the extension $S/R$, e.g. the degree, without having to fix a root. Note that unlike the current IsAdjoinRootMonic, this is a Prop! Of course you can still create the data (using choice) through definitions like hS.root, hS.basis, etc.

I'd welcome feedback on this design in principle before I try to implement it in some concrete cases to see if it's better than what we have now.

[Anne Baanen]

Hooray! Do you have some code for us to check out?

So for the case where we don't care about the precise value of x nor f, we would write ∃ x : S, IsPrimitiveElement R x? Or ∃ f : R[X], IsAdjoinRootMonic S f? Or this would depend on the precise generality of the situation? We'd definitely need easy ways to convert back and forth (under the right assumptions).

And for the case where we want to control both x and f, we'd say something like IsPrimitiveElement R x ∧ minpoly R x = f? I think we can live with writing that out, since it is not very verbose.

Also, how does the conclusion of the primitive element theorem end up looking?

[Artie Khovanov]

The only mathematically relevant case I can think of where we don't care about either the root or the polynomial is showing that the resulting algebra is finite and free, which will be theorems of both forms. Generally you care about the root when you're reasoning about the elements of the algebra and about the polynomial when you're reasoning about the algebra as a whole. In any case it's trivial to convert between the two.

My intention when we care about both was to use IsPrimitiveElement R x ∧ minpoly R x = f, yes. I could absolutely see having f as a parameter in IsPrimitiveElement alongside x, though it is uniquely determined. In that case the IsAdjoinRootMonic API could just use the IsPrimitiveElement API.

The primitive element theorem just says ∃ x : S, adjoin R {x} = S. Then there's a result that says that, when either
(a) R is a field, or
(b) R is an integrally closed domain and S is a domain and a torsion-free R-algebra
we in fact have IsPrimitiveElement x.

The name IsPrimitiveElement is therefore not ideal - happy to take suggestions for alternatives.

Code will be provided shortly.

[Artie Khovanov]

Also, I'm not sure what to do about IsAdjoinRoot. It would be easiest to just get rid of it but then we do lose some generality. The most general approach would be:

1. Define IsAdjoinRoot
2. Define IsPrimitiveElement and show the algebra satisfies IsAdjoinRoot
3. Define IsAdjoinRootMonic and show it's equivalent to IsPrimitiveElement

[Artie Khovanov]

OK @Anne Baanen the design is at https://github.com/artie2000/real_closed_field/blob/master/RealClosedField/PrimitiveElement.lean

[Anne Baanen]

Thanks! :octopus: Right now, I need to go arrange dinner. Will check in as soon as I have some Lean time.

[Anne Baanen]

I have been thinking about this for a bit, and wonder if it wouldn't be better if we split IsPrimitiveElement into two parts: IsGeneratingElement R x saying adjoin R {x} = \top, and IsPrimitiveElement adding the IsIntegralUnique part. A lot of the basic properties you prove for primitive elements also hold for generating elements.

It looks like you're working over integral domains, which loses us a tiny bit of generality compared to what we have now (PowerBasis basically doesn't use domains, and a lot of commutativity assumptions can be dropped there too). But I don't know from the top of my head if we actually use that generality in full, certainly I've always had the case of domains in the back of my mind and done all the generalizations opportunistically. Do you have something to point to as to why you chose this level of generality?

[Anne Baanen]

As for actually implementing this in Mathlib, I think it's best if the first PR(s) only develop the theory of IsPrimitiveElement, without any replacements downstream. Then when we have enough theory, we can replace existing uses of PowerBasis and IsAdjoinRoot incrementally. (Development-wise I'd suggest you try and do a few trial replacements as you develop the theory, so we can be sure the results actually work well. But the list of PRs you open does not need to reflect your actual development history.)

[Anne Baanen]

Let's stick with IsPrimitiveElement R x ∧ minpoly R x = f for now, we can always introduce a structure/abbrev if this turns out to be too much of a mouthful.

[Anne Baanen]

Naming: as far as I know the term "primitive element" really only refers to the generator of a field extension (or sometimes to the generator of the field's multiplicative group). A bit of generalizing of names is very common in Mathlib, so I don't think it's really bad practice to generalize here too. I'm happy to be corrected by others though.

If you really dislike the current naming, and you agree with my idea to split the adjoin R {x} = \top hypothesis off, maybe IsGenerating / IsGeneratingUnique to match IsIntegral/IsIntegralUnique?

[Artie Khovanov]

I think I already did prove everything I can prove for generating elements, for generating elements. It turns out it's not actually very much! But I can make it a structure so we eg get dot notation for reprAdjoinEqTop.

I am not working over an integral domain, and nor do I assume commutativity. I am not sure which declarations you are referring to. Indeed, IsPrimitiveElement is equivalent to PowerBasis, as demonstrated by .basis and .ofBasis.

[Anne Baanen]

Ah sorry, I didn't notice that R S get redefined in https://github.com/artie2000/real_closed_field/blob/master/RealClosedField/PrimitiveElement.lean#L176

[Anne Baanen]

Okay, I am confident now that this will be a useful replacement if we get the details above worked out! :tada:

[Artie Khovanov]

Yeah the stuff above that line is all preliminaries

[Artie Khovanov]

OK I've done some more work. The current design satisfies the following:
(1) All existing material from PowerBasis and IsAdjoinRoot is maintained.
(2) All material is as general as possible.
(3) All defs are directly accessible via dot notation in all structures.
Unfortunately this means there are now 4 different structures and slightly weird definitions.