[Merged by Bors] - feat: notation for galois group #30266
Closed
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
PR summary 60b581d0dbImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
github-actions
bot
added
the
large-import
github-actions
bot
removed
the
large-import
erdOne
commented
Oct 6, 2025
Comment on lines
19
to
35
| section Notation | ||
|
|
||
| notation "Gal(" L:100 "/" K ")" => L ≃ₐ[K] L | ||
|
|
||
| open Lean PrettyPrinter.Delaborator SubExpr in | ||
| /-- Pretty printer for the `Gal(L/K)` notation. -/ | ||
| @[app_delab AlgEquiv] | ||
| partial def delabGal : Delab := whenPPOption getPPNotation do | ||
| guard <| (← getExpr).isAppOfArity ``AlgEquiv 8 | ||
| let [u, v, _] := (← getExpr).getAppFn'.constLevels! | failure | ||
| let #[R, A, B, _, _, _, _, _] := (← getExpr).getAppArgs | failure | ||
| guard (A == B) -- We require that A = B syntatically, not merely defeq. | ||
| let some _ ← Meta.synthInstance? (.app (.const ``Field [u]) R) | failure | ||
| let some _ ← Meta.synthInstance? (.app (.const ``Field [v]) A) | failure | ||
| `(Gal($(← withNaryArg 1 <| delab)/$(← withNaryArg 0 <| delab))) | ||
|
|
||
| end Notation |
There was a problem hiding this comment.
The new notation is defined here.
kckennylau
reviewed
Oct 6, 2025
kckennylau
reviewed
Oct 6, 2025
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
…lib4 into erd1/galNotation
github-actions
bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
…lib4 into erd1/galNotation
github-actions
bot
removed
the
merge-conflict
thorimur
reviewed
Oct 15, 2025
There was a problem hiding this comment.
Thanks very much for this! :) I know large PRs like this are horrible to keep alive, so I've tried to make these review suggestions easy to apply.
The big ask is for a test file (e.g. at MathlibTest.GaloisNotation); the content of it can be relatively simple, and look like this:
import Mathlib.FieldTheory.Galois.Notation
import Mathlib.Algebra.Field.Rat
/-! Tests both elaboration and delaboration for `Gal(L/K)`. -/
section
universe u v w
variable (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A]
/- `Gal(A/R)` elaborates successfully, but `AlgEquiv` delaborates as usual because no `Field`
instance is found. -/
/-- info: A ≃ₐ[R] A : Type v -/
#guard_msgs in
#check Gal(A/R)
end
/- `Gal(L/K)` delaborates successfully when `L`, `K` are fields. -/
/-- info: Gal(ℚ/ℚ) : Type -/
#guard_msgs in
#check Gal(ℚ/ℚ)
section
universe u v w
variable (R : Type u) (A : Type v) [Field R] [Field A] [Algebra R A]
/- FIXME: `Gal(A/R)` should delaborate to `Gal(A/R)`, but `synthInstance?` during delaboration
can't pick up field instances which are variables. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Bug.3F.20Local.20instances.20not.20populated.20during.20delaboration/with/544850819). -/
/-- info: A ≃ₐ[R] A : Type v -/
#guard_msgs in
#check Gal(A/R)
end
Elaboration could sort of be considered "tested" by Mathlib itself (though it's good practice to test it directly in a test file anyway!), but delaboration (usually) needs to be tested directly.
Also, please edit the PR description to something slightly more descriptive, e.g.
This PR adds support for the notation
Gal(L/K) := L ≃ₐ[K] L.Gal(L/K)is a simple macro forL ≃ₐ[K] L, butL ≃ₐ[K] Lonly delaborates toGal(L/K)whenLandKare fields. Zulip thread ...
Pending these changes, LGTM! :) 🎉
Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean
Outdated
Show resolved
Hide resolved
thorimur
reviewed
Oct 16, 2025
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
thorimur
reviewed
Oct 16, 2025
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
thorimur
reviewed
Oct 16, 2025
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
thorimur
reviewed
Oct 16, 2025
|
Thanks very much for staying responsive through the review of this PR, and for keeping the many edits up-to-date! :) Thanks as well for adding the nice test file; I appreciate including a test that we're using I've reviewed the meta code, and it looks solid to me. I've also read through the library-wide replacements, and they do indeed get rid of now-extraneous parentheses and maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by thorimur. |
|
🚀 Pull request has been placed on the maintainer queue by thorimur. |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 16, 2025
This PR adds support for the notation `Gal(L/K) := L ≃ₐ[K] L`. `Gal(L/K)` is a simple macro for `L ≃ₐ[K] L`, but `L ≃ₐ[K] L` only delaborates to `Gal(L/K)` when `L` and `K` are fields. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Notation.20for.20Galois.20group/with/543320864
leanprover-community-mathlib4-bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
3 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds support for the notation
Gal(L/K) := L ≃ₐ[K] L.Gal(L/K)is a simple macro forL ≃ₐ[K] L, butL ≃ₐ[K] Lonly delaborates toGal(L/K)whenLandKare fields.Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Notation.20for.20Galois.20group/with/543320864