[Merged by Bors] - feat(FieldTheory): abelian extensions #23669

erdOne · 2025-04-04T15:22:08Z

github-actions · 2025-04-04T15:23:11Z

PR summary 5a6cfc3c42

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Cyclotomic.Basic	2395	2400	+5 (+0.21%)

Import changes for all files

Files	Import difference
32 files `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.NumberField.Cyclotomic.Basic` `Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings` `Mathlib.NumberTheory.NumberField.Cyclotomic.PID` `Mathlib.NumberTheory.NumberField.Cyclotomic.Three` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic`	5
`Mathlib.FieldTheory.Galois.Abelian` (new file)	1839

Declarations diff

+ IsAbelianGalois
+ IsAbelianGalois.of_algHom
+ IsAbelianGalois.of_isCyclic
+ IsAbelianGalois.tower_bot
+ IsAbelianGalois.tower_top
+ instance (K L : Type*) [Field K] [Field L] [Algebra K L] [IsAbelianGalois K L]
+ instance : IsAbelianGalois K (⊥ : IntermediateField K L)
+ instance : IsAbelianGalois K K
+ instance [IsAbelianGalois K L] (K' : IntermediateField K L) : IsAbelianGalois K K'
+ isAbelianGalois

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

xroblot · 2025-04-04T15:47:40Z

LGTM. Thanks!

alreadydone

Wondering whether we should add an instance [IsGalois K L] [IsCyclic (L ≃ₐ[K] L)] : IsAbelianGalois K L ...

erdOne · 2025-04-04T19:48:48Z

Not sure about having it as an instance but I added a lemma. We can upgrade it into an instance later if we find it useful.

alreadydone · 2025-04-04T20:08:06Z

It could be used to infer the IsAbelianGalois instance from FiniteField.instIsCyclicAlgEquivOfFinite and GaloisField.instIsGaloisOfFinite (though we should also add the IsAbelianGalois instance when the smaller field is finite, not necessarily the larger field). (Edit: the extension also needs to be algebraic.)

chrisflav · 2025-05-04T10:28:54Z

Given that #23773 is merged, I think we don't need an IsAbelianGalois typeclass anymore? @xroblot suggests to use

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

instead (see https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Abelian.20extension/near/511347691).

Still, the lemmas / instances in this PR should be preserved. So I would suggest to drop the class and replace it by Xavier's suggestion.

acmepjz · 2025-06-06T06:03:07Z

Given that #23773 is merged, I think we don't need an IsAbelianGalois typeclass anymore? @xroblot suggests to use
variable (E F : Type*) [Field E] [Field F] [Algebra F E] [IsGalois F E] [IsMulCommutative (E ≃ₐ[F] E)]
instead (see https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Abelian.20extension/near/511347691).

Still, the lemmas / instances in this PR should be preserved. So I would suggest to drop the class and replace it by Xavier's suggestion.

But maybe class abbrev IsAbelianGalois (E F : Type*) [Field E] [Field F] [Algebra F E] := IsGalois F E, IsMulCommutative (E ≃ₐ[F] E)?

…ian (#26427) Proved `IsCyclotomicExtension.isMulCommutative` that any cyclotomic extension (of rings) is abelian. Deprecated `IsCyclotomicExtension.Aut.commGroup` which is `CommGroup` and only adjoins one root of unity. Now `CommGroup` instance should be inferred automatically if `IsMulCommutative` is provided (the preferred spelling of abelian extension, see #23669 (comment)).

…ian (leanprover-community#26427) Proved `IsCyclotomicExtension.isMulCommutative` that any cyclotomic extension (of rings) is abelian. Deprecated `IsCyclotomicExtension.Aut.commGroup` which is `CommGroup` and only adjoins one root of unity. Now `CommGroup` instance should be inferred automatically if `IsMulCommutative` is provided (the preferred spelling of abelian extension, see leanprover-community#23669 (comment)).

riccardobrasca

Thanks!

bors d+

riccardobrasca · 2025-07-08T11:51:05Z

Mathlib/NumberTheory/Cyclotomic/Gal.lean


+variable (n K) in
+/-- Cyclotomic extensions are abelian. -/
+theorem isAbelianGalois (L : Type*) [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] :


This is already in mathlib now.

mathlib-bors · 2025-07-08T11:53:09Z

✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

acmepjz · 2025-07-08T17:06:41Z

Oh but I think the definition of IsAbelianGalois should be refactored to class abbrev. But this branch is locked due to in official mathlib4 repository. Any further changes to the code must be in a fork.

alreadydone · 2025-07-08T19:08:16Z

I can still push to my branches at least as of now ...

acmepjz · 2025-07-09T08:25:55Z

Seems that erdOne has Member permission so it's still OK to push to this branch?

riccardobrasca · 2025-07-09T08:38:49Z

Please migrate to a fork, the script makes this very simple.

riccardobrasca · 2025-07-09T08:50:23Z

I mean, migrate if you need to work on it, otherwise just merge.

…ian (leanprover-community#26427) Proved `IsCyclotomicExtension.isMulCommutative` that any cyclotomic extension (of rings) is abelian. Deprecated `IsCyclotomicExtension.Aut.commGroup` which is `CommGroup` and only adjoins one root of unity. Now `CommGroup` instance should be inferred automatically if `IsMulCommutative` is provided (the preferred spelling of abelian extension, see leanprover-community#23669 (comment)).

acmepjz · 2025-07-30T08:01:29Z

ping what's the progress of this PR?

riccardobrasca · 2025-08-06T10:51:08Z

@erdOne is this one ready to go?

erdOne · 2025-08-06T13:03:55Z

I asked a question here

…lib4 into erd1/abelianGalois

erdOne · 2025-10-17T15:31:04Z

@riccardobrasca Can you please take a look before I merge this? I think a significant portion has changed (in particular the switch to IsMulCommutative and the new Galois group notation).

riccardobrasca · 2025-10-18T09:23:03Z

LGTM, thanks! @xroblot can you have a quick look?

xroblot · 2025-10-18T16:41:13Z

LGTM, thanks! @xroblot can you have a quick look?

LGTM too and it will be very helpful for my current work on cyclotomic fields! Thanks.

erdOne · 2025-10-18T16:42:09Z

Great!
bors merge

mathlib-bors · 2025-10-18T17:12:01Z

Pull request successfully merged into master.

Build succeeded:

feat(FieldTheory): abelian extensions

c7f218c

erdOne added the t-algebra Algebra (groups, rings, fields, etc) label Apr 4, 2025

xroblot approved these changes Apr 4, 2025

View reviewed changes

alreadydone approved these changes Apr 4, 2025

View reviewed changes

cyclic => abelian

0504519

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label May 4, 2025

acmepjz mentioned this pull request Jun 26, 2025

[Merged by Bors] - feat(NumberTheory/Cyclotomic/Basic): any cyclotomic extension is abelian #26427

Closed

riccardobrasca self-assigned this Jun 29, 2025

riccardobrasca approved these changes Jul 8, 2025

View reviewed changes

leanprover-community-mathlib4-bot added delegated and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 8, 2025

erdOne added 4 commits October 5, 2025 21:13

Merge branch 'master' of https://github.com/leanprover-community/math…

9ba7421

…lib4 into erd1/abelianGalois

fix

0222e32

Merge branch 'master' of https://github.com/leanprover-community/math…

308945e

…lib4 into erd1/abelianGalois

fix

289f0e8

mathlib-bors bot pushed a commit that referenced this pull request Oct 18, 2025

feat(FieldTheory): abelian extensions (#23669)

06ed561

mathlib-bors bot changed the title ~~feat(FieldTheory): abelian extensions~~ [Merged by Bors] - feat(FieldTheory): abelian extensions Oct 18, 2025

mathlib-bors bot closed this Oct 18, 2025

mathlib-bors bot deleted the erd1/abelianGalois branch October 18, 2025 17:12

[Merged by Bors] - feat(FieldTheory): abelian extensions #23669

[Merged by Bors] - feat(FieldTheory): abelian extensions #23669

Uh oh!

Conversation

erdOne commented Apr 4, 2025

Uh oh!

github-actions bot commented Apr 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5a6cfc3c42

Import changes for modified files

Declarations diff

Uh oh!

xroblot commented Apr 4, 2025

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

erdOne commented Apr 4, 2025

Uh oh!

alreadydone commented Apr 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chrisflav commented May 4, 2025

Uh oh!

acmepjz commented Jun 6, 2025

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

riccardobrasca Jul 8, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jul 8, 2025

Uh oh!

acmepjz commented Jul 8, 2025

Uh oh!

alreadydone commented Jul 8, 2025

Uh oh!

acmepjz commented Jul 9, 2025

Uh oh!

riccardobrasca commented Jul 9, 2025

Uh oh!

riccardobrasca commented Jul 9, 2025

Uh oh!

acmepjz commented Jul 30, 2025

Uh oh!

riccardobrasca commented Aug 6, 2025

Uh oh!

erdOne commented Aug 6, 2025

Uh oh!

erdOne commented Oct 17, 2025

Uh oh!

riccardobrasca commented Oct 18, 2025

Uh oh!

xroblot commented Oct 18, 2025

Uh oh!

erdOne commented Oct 18, 2025

Uh oh!

mathlib-bors bot commented Oct 18, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

github-actions bot commented Apr 4, 2025 •

edited

Loading

alreadydone commented Apr 4, 2025 •

edited

Loading