This repository was archived by the owner on Jul 24, 2024. It is now read-only.
feat(field_theory/normal_closure): New file#18971
Closed
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
urkud
reviewed
Jul 15, 2023
urkud
reviewed
Jul 16, 2023
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
riccardobrasca
approved these changes
Jul 26, 2023
| If `K` is an intermediate field of `L/F` (in mathlib this means that `K` is both a subfield of `L` | ||
| and an `F`-subalgebra of `L`), then `K.normal_closure` is the smallest intermediate field of `L/F` | ||
| that contains the image of every `F`-algebra embedding `K →ₐ[F] L`. This will agree with the | ||
| absolute normal closure (`normal_closure` in the root namespace) whenever `L/F` is normal, but with |
Member
There was a problem hiding this comment.
Can you add a reference to the declaration saying that this agrees with normal_closure if L/F is normal?
2 tasks
Collaborator
Author
|
For some reason I thought that the existing normal closure was absolute, but it was actually relative too. So I don't think it makes sense to keep both. I opened #6163 |
Member
|
So this one can be closed? |
Collaborator
Author
|
Yes, I think there's no point keeping this one open now that all of the same material has be rewritten in lean4. |
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 6, 2023
…6163) This PR adds API and changes the definition of the normal closure of $F\leq K\leq L$ to be an intermediate field of L/F, rather than an intermediate field of L/K. For example, I think it would be more common to say that the normal closure of $\mathbb{Q}(\sqrt[3]{2})/\mathbb{Q}$ is $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}$ rather than $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}(\sqrt[3]{2})$. This change also means that the normal closure goes from being a dependent function `(K : Type) → IntermediateField K L` to being a non-dependent function `Type → IntermediateField F L`, making it easier to compare across the Galois corespondence. Supersedes leanprover-community/mathlib3#18971 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 7, 2023
…6163) This PR adds API and changes the definition of the normal closure of $F\leq K\leq L$ to be an intermediate field of L/F, rather than an intermediate field of L/K. For example, I think it would be more common to say that the normal closure of $\mathbb{Q}(\sqrt[3]{2})/\mathbb{Q}$ is $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}$ rather than $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}(\sqrt[3]{2})$. This change also means that the normal closure goes from being a dependent function `(K : Type) → IntermediateField K L` to being a non-dependent function `Type → IntermediateField F L`, making it easier to compare across the Galois corespondence. Supersedes leanprover-community/mathlib3#18971 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
ebab
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 11, 2023
…6163) This PR adds API and changes the definition of the normal closure of $F\leq K\leq L$ to be an intermediate field of L/F, rather than an intermediate field of L/K. For example, I think it would be more common to say that the normal closure of $\mathbb{Q}(\sqrt[3]{2})/\mathbb{Q}$ is $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}$ rather than $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}(\sqrt[3]{2})$. This change also means that the normal closure goes from being a dependent function `(K : Type) → IntermediateField K L` to being a non-dependent function `Type → IntermediateField F L`, making it easier to compare across the Galois corespondence. Supersedes leanprover-community/mathlib3#18971 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
kodyvajjha
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 22, 2023
…6163) This PR adds API and changes the definition of the normal closure of $F\leq K\leq L$ to be an intermediate field of L/F, rather than an intermediate field of L/K. For example, I think it would be more common to say that the normal closure of $\mathbb{Q}(\sqrt[3]{2})/\mathbb{Q}$ is $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}$ rather than $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}(\sqrt[3]{2})$. This change also means that the normal closure goes from being a dependent function `(K : Type) → IntermediateField K L` to being a non-dependent function `Type → IntermediateField F L`, making it easier to compare across the Galois corespondence. Supersedes leanprover-community/mathlib3#18971 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
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
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
4 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 intermediate_field.normal_closure, which interprets the normal closure as a function from intermediate_field to intermediate_field which should mesh nicely with the Galois correspondence.
Supersedes #18925