Skip to content
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

Closed
wants to merge 29 commits into from
Closed

Conversation

kbuzzard
Copy link
Member

@kbuzzard kbuzzard commented Jun 26, 2024

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.


Open in Gitpod

Sorry that this PR is long, although note that the first 100 lines are mostly docstrings.

@kbuzzard kbuzzard added the WIP Work in progress label Jun 26, 2024
Copy link

github-actions bot commented Jun 26, 2024

PR summary 8d55945d70

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.NumberTheory.Frobenius.Basic 1189

Declarations diff

+ F.descent
+ F.mod_Q_y_pow_q_eq_zero'
+ F.smul_eq_self
+ F.y_eq_zero
+ F_spec
+ Frob_Q
+ Frob_eq_pow_card
+ Frob_spec
+ Quotient.cast_eq_cast_iff_sub_mem
+ _root_.Polynomial.coe_monomial'
+ aeval_finset_prod
+ aeval_pow_card
+ coe_def
+ exists_Frob
+ exists_y
+ g_spec
+ m.mod_P_y_pow_q_eq_zero'
+ m.y_mod_P_eq_zero
+ m_spec
+ m_spec'
+ y_mod_Q
+ y_mod_Q'
+ y_not_in_Q
+ y_spec

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 26, 2024
@kbuzzard kbuzzard added awaiting-review t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebra Algebra (groups, rings, fields, etc) and removed WIP Work in progress labels Jun 29, 2024
@kbuzzard kbuzzard changed the title Abstract Frobenius elements feat: Abstract Frobenius elements Jun 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 2, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@riccardobrasca riccardobrasca self-assigned this Jul 2, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 2, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 2, 2024
Mathlib/NumberTheory/Frobenius/Basic.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/Frobenius/Basic.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/Frobenius/Basic.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/Frobenius/Basic.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/Frobenius/Basic.lean Outdated Show resolved Hide resolved
@@ -418,6 +418,10 @@ end Semiring

section CommSemiring

lemma aeval_finset_prod {R S ι : Type*}
Copy link
Member

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.
Copy link
Member

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)]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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)]
Copy link
Member

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)]
Copy link
Member

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
Copy link
Member

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.

Copy link
Member Author

@kbuzzard kbuzzard Jul 3, 2024

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.

Copy link
Member

@riccardobrasca riccardobrasca Jul 3, 2024

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!

Copy link
Member Author

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?

Copy link
Member

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!

@kbuzzard kbuzzard added awaiting-author A reviewer has asked the author a question or requested changes WIP Work in progress and removed awaiting-review awaiting-author A reviewer has asked the author a question or requested changes labels Jul 3, 2024
@kbuzzard
Copy link
Member Author

kbuzzard commented Jul 3, 2024

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).

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 11, 2024
@kbuzzard kbuzzard added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 22, 2024
@kbuzzard
Copy link
Member Author

kbuzzard commented Nov 7, 2024

Closed in favour of #17717

@kbuzzard kbuzzard closed this Nov 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize) WIP Work in progress
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants