Abelian extension

Stream: mathlib4

[Xavier Roblot]

Is this the correct way to define an abelian extension of fields?

import Mathlib.FieldTheory.Galois.Basic

variable (F E : Type*) [Field F] [Field E] [Algebra F E] [IsGalois F E]
  [Subgroup.IsCommutative (⊤ : Subgroup (E ≃ₐ[F] E))]

[Kevin Buzzard]

On the poster for https://www.claymath.org/events/formalizing-class-field-theory/ I went for \forall a b : G, a * b = b * a which feels a bit less contrived than what you've written but I'm certainly not convinced that my way is optimal either

[Andrew Yang]

I had something like in a branch of mine.

 class IsAbelianGalois (K L : Type*) [Field K] [Field L] [Algebra K L] extends
   IsGalois K L, Std.Commutative (α := L ≃ₐ[K] L) (· * ·)

 instance (K L : Type*) [Field K] [Field L] [Algebra K L] [IsAbelianGalois K L] :
     CommGroup (L ≃ₐ[K] L) where
   mul_comm := Std.Commutative.comm

[Xavier Roblot]

I like the idea of having a class for abelian extensions rather than some ad-hoc hypothesis.

[Filippo A. E. Nuccio]

Another option would be to add an assumption like

Subgroup.center G = ⊤

and to benefit from docs#Group.commGroupOfCenterEqTop; this might make it easier to speak about "abelian subextensions of a given extension" or the like; but @Andrew Yang 's solution is also very nice.

[Kevin Buzzard]

Yes, because this is how the library is designed, e.g. we have Group and CommGroup so it feels like if we have IsGalois then we should have IsAbelianGalois

[Xavier Roblot]

I am starting to play a bit with abelian extensions and it would be helpful to have some solid base to build on. @Andrew Yang , could you PR this definition?

[Andrew Yang]

I don't have much but here's a PR: #23669

[Antoine Chambert-Loir]

It would nice to fix the way that some properties of a group (and other algebraic objects) are stated. Subgroup.IsCommutative ⊤ is not really legible. Why not having a class IsCommutativefor groups (or monoids)?

[Kevin Buzzard]

Because then do you have the instance [Group G] [IsCommutative G] -> [CommGroup G] or [CommGroup G] -> [IsCommutative G]? Probably you can't have both because of loops. If we have IsCommutative then probably we should literally remove CommGroup which sounds like a massive nightmare.

[Kevin Buzzard]

The current design is throughout the library, for example we have NonAssocRing and Ring, and NonUnitalRing and Ring. For commutativity and associativity we have chosen a different design to IsCommutative and IsAssociative.

[Jz Pan]

Kevin Buzzard said:

Because then do you have the instance [Group G] [IsCommutative G] -> [CommGroup G]

This should not be an instance, but only a def, just like [Ring R] [IsField R] -> [Field R] is only a def: docs#IsField.toField

[Jz Pan]

Or define CommGroup as class abbrev

[Edward van de Meent]

Jz Pan said:

Kevin Buzzard said:

Because then do you have the instance [Group G] [IsCommutative G] -> [CommGroup G]

This should not be an instance, but only a def, just like [Ring R] [IsField R] -> [Field R] is only a def: docs#IsField.toField

these are not the same at all. IsField.toField creates data (it creates the inverse function), while CommGroup compared to Group only adds a proof of commutativity

[Edward van de Meent]

because it creates data, if it were an instance it would create diamonds, hence why it's a def

[Edward van de Meent]

Kevin Buzzard said:

Because then do you have the instance [Group G] [IsCommutative G] -> [CommGroup G] or [CommGroup G] -> [IsCommutative G]? Probably you can't have both because of loops. If we have IsCommutative then probably we should literally remove CommGroup which sounds like a massive nightmare.

i think this is actually a loop that lean is able to detect, so this may actually be fine?

[Aaron Liu]

What's an example of a loop Lean is not able to detect?

[Edward van de Meent]

one that changes the type, i think. i.e. things like [Group (MulOpposite G)] -> Group G

[Edward van de Meent]

which causes lean to look for Group on increasingly many MulOpposite applied to G, when trying to synthesise Group G

[Aaron Liu]

That's what I thought, but then people were worrying about loops on stuff that was not changing the type and I got confused.

[Edward van de Meent]

another example of what can go wrong is that (when a specific option set to a high value, i forget which one) there can be an increase of local variables. An example would be [forall (n:Nat), Group G] -> Group G. In this example, the context keeps getting more and more free variables of type Nat

[Edward van de Meent]

(the option was SynthPendingDepth)

[Johan Commelin]

I think we should add the looping instance, and see what the effect is on !bench. If the effect is tiny, then I would really prefer an IsCommutative typeclass, instead of a specialized IsAbelianGalois.

[Eric Wieser]

Why do we need the loopy instance?

[Junyan Xu]

test PR: #23773

[Johan Commelin]

Eric Wieser said:

Why do we need the loopy instance?

So that you can apply all lemmas about commutative monoids/groups to your Galois group.

[Eric Wieser]

What's the precise example we need to succeed?

[Xavier Roblot]

Results are in and they're not really good: https://github.com/leanprover-community/mathlib4/pull/23773#issuecomment-2783321596

[Johan Commelin]

rw [mul_comm] for starters.

[Johan Commelin]

Junyan Xu said:

test PR: #23773

This doesn't even add the other part of the loop, right? CommGroup -> IsMulCommutative...

[Johan Commelin]

Eric Wieser said:

What's the precise example we need to succeed?

But besides the trivial rw [mul_comm], facts like "every subgroup is normal", etc...

[Johan Commelin]

I guess it's hard to make a list here.

[Xavier Roblot]

Johan Commelin said:

Junyan Xu said:

test PR: #23773

This doesn't even add the other part of the loop, right? CommGroup -> IsMulCommutative...

Yes, the loop is there: Group + IsMulCommutative -> CommGroup and CommGroup -> IsMulCommutative

[Eric Wieser]

I was looking for a mwe with variables and a failing #synth

[Eric Wieser]

I guess it's

import Mathlib

variable (F E : Type*) [Field F] [Field E] [Algebra F E] [IsGalois F E]

-- add a hypothesis to make this work
#synth CommGroup (E ≃ₐ[F] E)

[Xavier Roblot]

A solution is proposed there: #23669

[Jz Pan]

BTW I'm trying IsZpExtension here https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/FieldTheory/ZpExtension/Basic.lean and I also defined a CommGroup instance. Clearly abelian extension is very useful in my application.

[Xavier Roblot]

Removing the loop in #23773 make everything runs smoothly (If I understand the results properly). Now, I think that we actually do not need the instance CommGroup -> IsCommutative for abelian extensions. It is enough to have Group + IsCommutative -> CommGroup so that we can promote E ≃ₐ[F] E to a CommGroup.

[Xavier Roblot]

OK, so when I sent the previous message, I actually had forgotten to rerun !bench first :face_palm: but now I did run it and the results of the bench of #23773 are a lot better.

[Kevin Buzzard]

Pretriangulated gets slower but Triangulated gets faster by more :-)

[Kevin Buzzard]

It would probably not be difficult to avoid needing CommGroup -> IsCommutative -- presumably the only point of IsCommutative is to get you to CommGroup anyway.

[Xavier Roblot]

That's what I think. In any case, I checked that Group + IsCommutative -> CommGroup is enough for my needs.

[Kevin Buzzard]

Is this PR WIP or ready for review? If ready for review you should delete the dead code and probably also not call the section test.

[Xavier Roblot]

No. It is not for review (I'll mark it WIP), it was just for testing. If there is an agreement that this is the way to go, I'll clean it up and probably add also the CommMonoid instance and maybe some more.

[Xavier Roblot]

Well, I'll probably do that anyway so we get something more concrete to discuss about but that will have to wait for tomorrow...

[Filippo A. E. Nuccio]

Jz Pan said:

BTW I'm trying IsZpExtension here https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/FieldTheory/ZpExtension/Basic.lean and I also defined a CommGroup instance. Clearly abelian extension is very useful in my application.

BTW, although a bit unrelated to this, I think we really need to set up the theory of multiple Zp extensions from the start indexed by a Fintype I and have an abbrev for the special case I=Unit as we do for polynomials.

[Jz Pan]

@Filippo A. E. Nuccio Maybe we should continue discussing Zp-extension things here #maths > Discussion on formalization of Iwasawa Theory in Lean :)

[Xavier Roblot]

I added more instances to #23773 and benchmarked the new version. It is not as bad as with the loop but still 3 files got notably slower and the overall slowdown is +0.48%

[Xavier Roblot]

I looked in details at Mathlib.LinearAlgebra.Semisimple and there is no place where it got significantly slower. It just that everything takes a little more time.

[Xavier Roblot]

After lowering the priority of the new instances in #23773, the slowdown is only +0.15% with only one file Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup significantly slower (+6%).

[Xavier Roblot]

(but still a bunch of files getting somewhat slower)

[Xavier Roblot]

The latest version of #23773 is ready for review. The slowdown is now "only" +0.09%.

[Xavier Roblot]

#23773 has been merged. The proper way to define an abelian extension is now:

import Mathlib.FieldTheory.Galois.Basic

variable (E F : Type*) [Field E] [Field F] [Algebra F E] [IsGalois F E] [IsMulCommutative (E ≃ₐ[F] E)]

#synth CommGroup (E ≃ₐ[F] E) -- CommGroup.ofIsMulCommutative