-
Notifications
You must be signed in to change notification settings - Fork 335
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: Abstract Frobenius elements #14155
Conversation
PR summary 8d55945d70Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
…ty/mathlib4 into kbuzzard-abstractfrob
This PR/issue depends on:
|
@@ -418,6 +418,10 @@ end Semiring | |||
|
|||
section CommSemiring | |||
|
|||
lemma aeval_finset_prod {R S ι : Type*} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a special case of AlgHom.map_prod
, right?
namespace Abstract -- stuff in here is auxiliary variables etc, general stuff which will | ||
-- work in number field and function field settings. This namespace is full of junk | ||
-- like `y_spec` and `F_spec` which are auxiliary constructions needed for `Frob` and | ||
-- which we will never need again. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you make all the "junk" results private?
|
||
variable (Q : Ideal B) [Q.IsMaximal] | ||
|
||
variable [Fintype (B ⧸ Q)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
variable [Fintype (B ⧸ Q)] | |
variable [Finite (B ⧸ Q)] |
lemma g_spec : ∀ (z : (B ⧸ Q)ˣ), z ∈ Submonoid.powers (g Q) := | ||
(IsCyclic.exists_monoid_generator (α := (B ⧸ Q)ˣ)).choose_spec | ||
|
||
variable [Fintype (B ≃ₐ[A] B)] [DecidableEq (Ideal B)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You can also use Finite
here. It breaks something later, but you can always make Fintype.ofFinite
a local instance (sooner or later Finite
will replace Fintype
where it makes sense to do so).
|
||
open scoped Polynomial | ||
|
||
variable [Fintype (A⧸P)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same here.
|
||
/-- An auxiliary arithmetic Frobenius element, in the automorphism group of the integer ring | ||
rather than the global field itself. -/ | ||
noncomputable abbrev Frob := (exists_Frob Q isGalois P).choose |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The full name is ArithmeticFrobenius.Abstract.Frob
. I understand you want to make it clear we are talking about the arithmetic one, but Abstract
seems useless.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
But we will never use this Frob, as it is an element of Aut(B/A), not Gal(L/K), and one of its inputs is some weird hypothesis about everything in B which is Aut-stable being in A. Everything in the Abstract namespace is useless! Actual Frobenius elements are the next PR, which uses this abstract stuff, fills in hypotheses in the number field and function field case (e.g. finiteness hypotheses), and moves from automorphisms of rings to automorphisms of fields. As far as I am concerned, this definition could be private!
This is an attempt to minimise code duplication whilst not being entirely clear about the generality in which people want Frobenius elements.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I see, no problem then!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How about I call the namespace Aux?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This seems a good idea!
Joel Riou has pointed out here that this argument generalizes to prove a cleaner statement (no finiteness assumptions) so I will modify this PR to prove the even more general thing (apparently it's useful for the etale fundamental group; the argument is very similar to what is here, but uses integrality more). |
Closed in favour of #17717 |
This PR will be closed because it's not in the right generality; the current approach is outlined here.
We develop the "abstract" theory Frobenius elements. The set-up is a commutative ring A, a commutative A-algebra B, and maximal ideals P of A under Q of B. Assuming that the fixed points of Aut_{A-alg}(B) are A, and that B/Q and A/P are finite, we prove the existence of a Frobenius element in Aut_{A-alg}(B). This is the "guts" of the construction; applications to number fields and function fields will come later.
Sorry that this PR is long, although note that the first 100 lines are mostly docstrings.