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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(Algebra/CharP/{Basic|ExpChar}): add sum_pow_{char|expChar}_pow #9799

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(Algebra/CharP/{Basic|ExpChar}): add sum_pow_{char|expChar}_pow #9799

wants to merge 3 commits into from

Conversation

acmepjz
Copy link
Collaborator

@acmepjz acmepjz commented Jan 17, 2024

Open in Gitpod

@acmepjz acmepjz added awaiting-review The author would like community review of the PR awaiting-CI t-algebra Algebra (groups, rings, fields etc) labels Jan 17, 2024
@acmepjz acmepjz mentioned this pull request Jan 17, 2024
Closed
11 tasks
riccardobrasca
riccardobrasca approved these changes Jan 17, 2024
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

Mathlib/Algebra/CharP/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/CharP/ExpChar.lean Outdated Show resolved Hide resolved
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 17, 2024

✌️ acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Jan 17, 2024
@acmepjz
Copy link
Collaborator Author

acmepjz commented Jan 17, 2024

I changed the newly added code to use induction and cases, but the existing code is unchanged.

@acmepjz
Copy link
Collaborator Author

acmepjz commented Jan 17, 2024

bors r+

@mathlib-bors
Copy link

mathlib-bors bot commented Jan 17, 2024

Canceled.

alreadydone
alreadydone reviewed Jan 17, 2024
View reviewed changes
Copy link
Contributor

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

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

I think we should probably construct iterateFrobenius as a RingHom (or make a general construction that allows to iterate an arbitrary ring endomorphism), so the proofs will just become map_(list/multiset_)sum etc. For the case of expChar, we'd need to intrduce RingHoms frobenius' (or expFrobenius?) and iterateFrobenius' (maybe we could even promote them to the "official" Frobenii).

@acmepjz
Copy link
Collaborator Author

acmepjz commented Jan 17, 2024 •
edited

I think we should probably construct iterateFrobenius as a RingHom (or make a general construction that allows to iterate an arbitrary ring endomorphism), so the proofs will just become map_(list/multiset_)sum etc.

I think you are right. Probably we also need that iterateFrobenius p n x is defeq to x ^ p ^ n or just rw [iterate_frobenius].

or make a general construction that allows to iterate an arbitrary ring endomorphism

You also need iterate of group (or add group, or algebra) endomorphisms, probably also iterate of group (or add group, etc etc) automorphisms with negative n.

For the case of expChar, we'd need to intrduce RingHoms frobenius' (or expFrobenius?) and iterateFrobenius' (maybe we could even promote them to the "official" Frobenii).

I was thinking of protected def ExpChar.frobenius but maybe it's also good to change the original frobenius to use ExpChar.

@alreadydone
Copy link
Contributor

Probably we also need that iterateFrobenius p n x is defeq to x ^ p ^ n.

Yeah, even though we have RingHom.comp, frobenius.comp frobenius won't be defeq to (· ^ p ^ 2) ... I guess you can't achieve the defeq with the general construction, so we should satisfy ourselves with the special case of Frobenius.

@acmepjz
Copy link
Collaborator Author

acmepjz commented Jan 18, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 18, 2024
@acmepjz
feat(Algebra/CharP/{Basic|ExpChar}): add sum_pow_{char|expChar}_pow (…
1e74fcf 
…#9799)
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/CharP/{Basic|ExpChar}): add sum_pow_{char|expChar}_pow [Merged by Bors] - feat(Algebra/CharP/{Basic|ExpChar}): add sum_pow_{char|expChar}_pow Jan 18, 2024
@mathlib-bors mathlib-bors bot closed this Jan 18, 2024
@mathlib-bors mathlib-bors bot deleted the acmepjz_sum_pow_char_pow branch January 18, 2024 01:57
alreadydone added a commit that referenced this pull request Jan 26, 2024
@alreadydone
generalize frobenius to ExpChar; add (semi)LinearMap.frobenius; remove …
a74887e 
…#9799 lemmas
mathlib-bors bot pushed a commit that referenced this pull request Feb 2, 2024
@alreadydone @acmepjz
refactor: generalize CharP+Prime to ExpChar in frobenius (#10016)
96a6d29 
Consequently, the part about `frobenius` in Algebra/CharP/Basic is moved to CharP/ExpChar, and imports are adjusted as necessary.

+ Add instances from `CharP+Fact(Nat.Prime)` and `CharZero` to `ExpChar`, to allow lemmas generalized to ExpChar still apply to CharP.

+ Remove lemmas in Algebra/CharP/ExpChar from [#9799](1e74fcf) because they coincide with the generalized lemmas, and golf the other lemmas (in Algebra/CharP/Basic).

+ Define the RingHom `iterateFrobenius` and the semilinear map `LinearMap.(iterate)Frobenius` for an algebra. When the characteristic is zero (ExpChar is 1), these are all equal to the identity map (· ^ 1). Also define `iterateFrobeniusEquiv` for perfect rings.

+ Fix and/or generalize other files.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: acmepjz <acme_pjz@hotmail.com>
atarnoam pushed a commit that referenced this pull request Feb 9, 2024
@alreadydone @acmepjz @atarnoam
refactor: generalize CharP+Prime to ExpChar in frobenius (#10016)
415b862 
Consequently, the part about `frobenius` in Algebra/CharP/Basic is moved to CharP/ExpChar, and imports are adjusted as necessary.

+ Add instances from `CharP+Fact(Nat.Prime)` and `CharZero` to `ExpChar`, to allow lemmas generalized to ExpChar still apply to CharP.

+ Remove lemmas in Algebra/CharP/ExpChar from [#9799](1e74fcf) because they coincide with the generalized lemmas, and golf the other lemmas (in Algebra/CharP/Basic).

+ Define the RingHom `iterateFrobenius` and the semilinear map `LinearMap.(iterate)Frobenius` for an algebra. When the characteristic is zero (ExpChar is 1), these are all equal to the identity map (· ^ 1). Also define `iterateFrobeniusEquiv` for perfect rings.

+ Fix and/or generalize other files.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: acmepjz <acme_pjz@hotmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone left review comments

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Assignees
No one assigned
Labels
delegated t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@acmepjz @alreadydone @riccardobrasca @leanprover-community-mathlib4-bot