[Merged by Bors] - refactor(FieldTheory/NormalClosure): change definition and add API#6163
[Merged by Bors] - refactor(FieldTheory/NormalClosure): change definition and add API#6163
Conversation
|
I am not sure I understand the point of the new definition, since as you said normalClosure is already an |
Yes sorry, I got myself confused. The difference is that if you apply the old definition to an intermediate field, then you have to restrict scalars to get back to the same intermediate field type. It's more convenient in this case to have a function |
|
I especially have in mind the Galois correspondence, where |
Ah, so the point is if |
|
Yeah, having both does seems strange. I'll look into refactoring the current definition to be |
|
One problem with your definition is that |
|
The refactor seemed to go through smoothly, and I've added back the lost instances. |
This comment is a bit misleading, the |
Good point. I've updated the PR description. |
|
I made another edit, your spelling looked like it was describing |
|
@jcommelin, I'd argue that a TFAE is worse because:
This came up when definig |
|
This looks great to me. Can you show it's a |
|
I think @YaelDillies concluded that ClosureOperator was poorly designed and not worth trying to use; I think a galois connection would be more sensible? |
|
Wouldn't defining a Galois connection require defining a type of normal intermediate fields? Is that something that we want to do? |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
You can try using |
|
Thanks 🎉 bors merge |
…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 PR was included in a batch that was canceled, it will be automatically retried |
…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>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
…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>
…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 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 Lto being a non-dependent functionType → IntermediateField F L, making it easier to compare across the Galois corespondence.Supersedes leanprover-community/mathlib3#18971