CM-extensions of number fields

Stream: maths

[Xavier Roblot]

In #23533, I give a definition of a CM-extension of number fields:

class IsCMExtension (F K : Type*) [Field F] [NumberField F] [Field K] [NumberField K]
    [Algebra F K] : Prop
  extends IsTotallyReal F, IsTotallyComplex K where
  finrank_eq_two' : Module.finrank F K = 2

then I prove some results about these extensions in series of PR with, in the end, the proof of the relation between the regulators of F and K.

In another series of PR starting with #23760, I define maximalRealSubfield K (I guess the name is self-explanatory) and make the following definition:

abbrev IsCM : Prop := IsCMExtension (maximalRealSubfield K) K

and prove that if there exists F such that IsCMExtension F K then IsCM K since in this situation F and maximalRealSubfield K are isomorphic. Indeed, if K is a CM-field then it is a CM-field over its maximal real subfield.

In his review of #23533 (and in private DMs), @Filippo A. E. Nuccio remarked that he's not sure about the necessity to have IsCMExtension since if we have IsCMExtension F K, then we know that F will always be, essentially, equal to maximalRealSubfield K, so (a modified version of) IsCM should be enough. That's definitely true but I think it still worthwhile to keep
IsCMExtension (maybe as a def rather than a class) since I believe it will allow for more flexibility. Note that it is possible that I am not doing a very good job at presenting @Filippo A. E. Nuccio position -- and if so, I am very sorry --, but I am sure he will be able to state it more correctly if needed.

In any case, since @Filippo A. E. Nuccio and I were not able to reach a consensus, we decided to create this post to ask for some remarks, suggestions and advices from the community.

[Johan Commelin]

I haven't thought long about this, but I guess it will be quite convenient to have the flexibility of IsCMExtension, for example when looking at $\mathbb{Q}(i) / \mathbb{Q}$.

[Kevin Buzzard]

I am quite conflicted about this sort of question. I wanted to prove a bunch of results about adeles of a general number field by showing $\mathbb{A}_K=\mathbb{A}_{\mathbb{Q}}\otimes K$ (WIP in FLT) and then proving stuff for the adeles of $\mathbb{Q}$, but the way mathlib was set up a few months ago this involved having to prove results about the integers of $\mathbb{Q}$ which looked like a far less convenient object than $\mathbb{Z}$. So I made a PR to allow adeles of a number field to supply its own integer ring rather than "the ring of integers of the number field" but whilst I was waiting for it to get merged I got the hang of the integers of $\mathbb{Q}$ and ultimately just proved everything I needed for them anyway (they're isomorphic to $\mathbb{Z}$ and this is good enough in practice for what I needed). So now I just don't know whether this extra flexibility is useful or not. But my instinct is to allow it, just in case it is :-)

[Adam Topaz]

Should we introduce IsRingOfIntegers A K with an instance for IsRingOfIntegers Z Q?

[Kevin Buzzard]

What are the typeclasses on K making this meaningful?

[Adam Topaz]

Maybe just NumberField K for now.

[Adam Topaz]

The function field case is more subtle, of course

[Kevin Buzzard]

Do we want S-integers? This is more complicated because the S is currently HeightOneSpectrum A rather than depending on K alone.

[David Ang]

#docs4 Set.integer

[Kevin Buzzard]

But what we want is IsInteger, not Integer

[Kevin Buzzard]

There's also Nonarch local fields of course!

[Riccardo Brasca]

For number fiels we basically already have it, IsIntegralClosure Z ...

[Filippo A. E. Nuccio]

It seems to me that we are departing from @Xavier Roblot 's initial topic of CM fields. Let me try to explain why I believe that a class IsCMExtension is not very useful, and even on my opinion a bit unfortunate, unlike IsCMField. It seems to meet that being CM is really an absolute notion, not a relative one, so carrying over the totally real subfield is useless, it just makes it necessary to define it before stating that a field is CM. For instance, the Hilbert class field of an imaginary quadratic field whose class group is a 2-group is CM, but the totally real subfield is nasty to describe.

[Filippo A. E. Nuccio]

Moreover, two non definitionally equal descriptions of the totally real subfield for the same CM field would give rise to two different terms, so if you start with a pair F K that is a CM extension, most probably F will be different from K+, so you also end up with the CM extension K+ K.

[Filippo A. E. Nuccio]

Finally, I do not really see how type class inference night fire, because I see no example of an Algebra F K instance that woould be promoted to IsCMExtension automatically.

[Filippo A. E. Nuccio]

IMHO we need the classes IsCMField and a more general one IsQuadraticExtension (for very general fields beyond number fields) and an instance of IsCMField K out of a IsTotallyImmaginary K, IsTotallyReal F and IsQuadraticExtension F K.

[Filippo A. E. Nuccio]

The disadvantage of having both classes IsCMField K and IsCMExtension F K is the high risk of code duplication, plus a flurry design, where it would not be clear if we want to develop the library for one or for the other class, ending up with some contributors developing one and other developing the other.

[Xavier Roblot]

So the idea in the current design is that if there is a IsCM K instance (I guess that's what Filippo calls IsCMField K) then automatically a IsCMExtension (maximalRealSubfield K) K instance is added and thus all the general results about IsCMExtension can be applied to maximalRealSubfield K.

I agree that there is a chance that people start developing results about maximalRealSubfield K under the IsCM K instance rather than use the general case given by IsCMExtension F K. I was planning to add a remark in the implementation notes against doing that.

In any case, whether we call it IsCMExtension or decide to not give it a name, we need something that says: "this is the maximal real subfield of this totally complex number field", thus why not develop the API for this general case...

[Filippo A. E. Nuccio]

I think that one point is to decide whether to steer they library towards proving results for CM fields or for pairs of a CM field together with a totally real subfield. My idea is that the former is preferable, and that all results I can think of that speak about the totally real subfield should just depend on the general setting of quadratic extensions (plus tot. imaginary/real assumptions)

[Johan Commelin]

@Filippo A. E. Nuccio So do I understand correctly that you are advocating for IsCM K and that Xavier's IsCMExtension F K is spelled as [IsTotallyReal F] [IsCM K] [IsQuadratic F K] instead?

[Filippo A. E. Nuccio]

Johan Commelin said:

Filippo A. E. Nuccio So do I understand correctly that you are advocating for IsCM K and that Xavier's IsCMExtension F K is spelled as [IsTotallyReal F] [IsCM K] [IsQuadratic F K] instead?

Yes, this is precisely what I have in mind.

[Johan Commelin]

@Xavier Roblot To me :up: seems a reasonable design. What do you think of it?
Because IsCM K will not be able to be inferred from [IsCMExtension ?F K] if ?F is unknown. For that reason, I think Filippo A. E. Nuccio's suggestion is a good one.

[Xavier Roblot]

Note that in the spelling [IsTotallyReal F] [IsCM K] [IsQuadratic F K], the only necessary information provided by IsCM K is that K is totally complex and thus the spelling:
[IsTotallyReal F] [IsTotallyComplex K] [IsQuadratic F K] is probably better (which is more or less the content of IsCMExtension). So the suggestion is, I guess, to not define the class IsCMExtension but to use instead the corresponding explicit hypothesis to prove the general results about CM extensions.

[Xavier Roblot]

Now, that means that to be able to use the results proved in the general case above to the special case of maximalRealSubfield K, it will be necessary to do something like that

class IsCM (K : Type*) [Field K] [NumberField K] : Prop where
  isTotallyReal : IsTotallyReal (maximalRealSubfield K)
  isQuadratic : IsQuadratic (maximalRealSubfield K) K

instance (K : Type*) [Field K] [NumberField K] [IsCM K] : IsTotallyReal (maximalRealSubfield K) :=

instance (K : Type*) [Field K] [NumberField K] [IsCM K] : IsQuadratic (maximalRealSubfield K) K :=

But I guess that's okay.

[Filippo A. E. Nuccio]

For the IsCM class, isn't the maximal real subfield totally real by def? Or how is it defined?

[Johan Commelin]

Xavier Roblot said:

Note that in the spelling [IsTotallyReal F] [IsCM K] [IsQuadratic F K], the only necessary information provided by IsCM K is that K is totally complex and thus the spelling:
[IsTotallyReal F] [IsTotallyComplex K] [IsQuadratic F K] is probably better (which is more or less the content of IsCMExtension). So the suggestion is, I guess, to not define the class IsCMExtension but to use instead the corresponding explicit hypothesis to prove the general results about CM extensions.

I agree that in the presence of [IsTotallyReal F] [IsQuadratic F K] the two assumptions [IsTotallyComplex K] and [IsCM K] are equivalent. And it definitely should be a lemma!
But this is not something that TC synthesis can figure out. It can do the direction IsCM K -> IsTotallyComplex K. But the converse is not possible, because it will have to pull F out of thin air.

That's why I would consider keeping the IsCM K hypothesis in place in examples where we want to reason flexibly about the totally real subfield.